[opentheory-users] the Unwanted namespace

[Ramana Kumar]

On Fri, Dec 2, 2011 at 10:25 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> I will say that the recent change I made to eliminate "Unwanted.id tm"
> terms in general, rather than simple cases, resulted in a performance
> degradation that I'm currently investigating.
>
> But this aside, when the the opentheory tool eventually terminated,
> did it successfully eliminate all Unwanted.id terms?

I think so. A glance at the summary of the article looked OK.
I am having trouble reading it back in to HOL4, but that may be an
unrelated problem.

>
> Cheers,
>
> Joe
>
> On Fri, Dec 2, 2011 at 11:53 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> OK it wasn't looping - just taking a long time.
>>
>> On Fri, Dec 2, 2011 at 7:46 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>> My lazy list article made use of Unwanted.id but didn't define it.
>>> I've been trying to process it with the new opentheory for about 10
>>> minutes and it seems like it's either really slow or caught in a loop.
>>> I put the article here cam.xrchz.net/ll.art.gz. There's also the
>>> original version from two months ago cam.xrchz.net/llist.art.gz, which
>>> I don't know why is different.
>>>
>>> Here's what I'm looking at:
>>> % opentheory info --article -o llist.art llist.art
>>> WARNING: 38 objects left on the stack by llist.art
>>> WARNING: 473,658 objects left in the dictionary by llist.art
>>>
>>> Some (maybe optional) output indicating status and progress might be nice.
>>>
>>> On Thu, Dec 1, 2011 at 10:08 PM, Joe Hurd <joe at gilith.com> wrote:
>>>> Hi Ramana,
>>>>
>>>> I just released a version of the opentheory tool that should eliminate
>>>> any occurrences of
>>>>
>>>> Unwanted.id <term>
>>>>
>>>> I wanted to test it on the article that you uploaded some time ago,
>>>> but unfortunately the new scheme requires that the Unwanted.id
>>>> constants to be eliminated are input constants (i.e., not defined by
>>>> the theory).
>>>>
>>>> Could you either (i) upload a new version of your article without the
>>>> definition of Unwanted.id or (ii) try the new version of the
>>>> opentheory tool yourself to see whether it does the right thing?
>>>>
>>>> Cheers,
>>>>
>>>> Joe
>>>>
>>>> On Mon, Oct 10, 2011 at 12:55 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>>>>> Unfortunately I can see other ways that terms like these could enter
>>>>>> the state, such as
>>>>>>
>>>>>> appThm (|- (\f. f x) = t) (|- Unwanted.id = u)
>>>>>>
>>>>>> followed by betaConv of the LHS at a later point.
>>>>>
>>>>> So we would need to consider betaConv too...
>>>>> Anything else?
>>>>>
>>>>>> I'd really like a scheme that eliminates all occurrences of the
>>>>>> Unwanted.id constant from a proof, if that was possible. And by this I
>>>>>> mean that grepping the resulting article for occurrences of the
>>>>>> "Unwanted" namespace will not turn up any results.
>>>>>
>>>>> OK.
>>>>>
>>>>> I think your current treatment of appTerm is fine - it won't fail, and
>>>>> it removes those occurrences of Unwanted.id from the article file.
>>>>>
>>>>> So let's consider appThm and betaConv.
>>>>> These are the general forms I see introducing unwanted terms:
>>>>>
>>>>> appThm (|- Unwanted.id = f) (|- x = y)
>>>>> appThm (|- f = Unwanted.id) (|- x = y)
>>>>> betaConv (|- (\f. t[f x]) Unwanted.id)
>>>>>
>>>>> What happens if you just change the semantics of all of these commands
>>>>> to replace any resulting (Unwanted.id t) terms by (t), and also
>>>>> prevent Unwanted.id from being defined (to stop an obvious soundness
>>>>> problem)?
>>>>>
>>>>> _______________________________________________
>>>>> opentheory-users mailing list
>>>>> opentheory-users at gilith.com
>>>>> http://www.gilith.com/opentheory/mailing-list
>>>>>
>>>>
>>>> _______________________________________________
>>>> opentheory-users mailing list
>>>> opentheory-users at gilith.com
>>>> http://www.gilith.com/opentheory/mailing-list
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list