[opentheory-users] the Unwanted namespace

[Ramana Kumar]

ugh apparently it's also a "defined constant". I don't know why my
theory would be defining Unwanted.id ...

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