[opentheory-users] the Unwanted namespace

[Ramana Kumar]

Actually it seems that one Unwanted.id remained. It shows up in an
Axiom in the lazy-list package I just uploaded
http://opentheory.gilith.com/opentheory/packages/lazy-list-0.1/lazy-list-0.1.html.

On Sat, Dec 3, 2011 at 12:33 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> 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