[opentheory-users] the Unwanted namespace

[Ramana Kumar]

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