[opentheory-users] the Unwanted namespace

[Ramana Kumar]

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