[opentheory-users] the Unwanted namespace

[Joe Hurd]

Hi Ramana,

The elimination procedure only knows the definition

Unwanted.id = \x. x

which it uses to reduce terms

Unwanted.id x --> x

This is the reason that an instance of Unwanted.id is not being
eliminated in your article (the elimination procedure knows nothing
about the Function.o constant), although it does instantiate the
undefined Unwanted.id constant to the definition above (which is why
it appears to be defined in the resulting article).

The solution is to ensure that every instance of Unwanted.id in theory
assumptions and theorems is fully applied. This should always be the
case for constants used to tag terms, which are the main use-case of
Unwanted.id.

Cheers,

Joe

On Tue, Dec 6, 2011 at 11:18 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> Will your scheme for eliminating Unwanted.id work in terms where it
> does not appear fully applied, but can still be eliminated?
> Specifically, when Unwanted.id is composed with another function.
>
> On Tue, Dec 6, 2011 at 6:44 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> Thanks for making it quicker :)
>>
>> Now, the only place where Unwanted.id seems not to be erased is in an
>> apparent axiom required by my article.
>> Can you confirm that the article is actually trying to define Unwanted.id?
>> I generated the article from a HOL4 theory that I don't think should
>> be defining anything mapped to Unwanted.id, so I'm a bit confused
>> about that at the moment...
>>
>> On Tue, Dec 6, 2011 at 4:58 AM, Joe Hurd <joe at gilith.com> wrote:
>>> Hi Ramana,
>>>
>>> I fixed a performance bug in the proof rewriting, and your example
>>> goes through pretty quickly now (see below). The fix is both pushed
>>> and released in the latest version of the opentheory tool.
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> ________________________________________________________________
>>>
>>> dimholt:~/dev/opentheory$ gzcat ~/Desktop/ll.art.gz | time
>>> bin/mlton/opentheory info --inference article:-
>>> WARNING: 38 objects left on the stack by -
>>> WARNING: 473,658 objects left in the dictionary by -
>>> Primitive inferences:
>>> eqMp ............ 150,377
>>> deductAntisym ... 129,584
>>> subst ............ 76,065
>>> appThm ........... 20,748
>>> assume ........... 18,086
>>> refl .............. 9,363
>>> betaConv .......... 7,461
>>> absThm ............ 4,564
>>> axiom ............... 193
>>> defineConst .......... 25
>>> defineTypeOp .......... 1
>>> Total ........... 416,467
>>>       24.40 real
>>>       15.30 user
>>>         9.07 sys
>>>
>>> dimholt:~/dev/opentheory$ time bin/mlton/opentheory info --inference
>>> foo.art Primitive inferences:
>>> eqMp ............. 68,100
>>> subst ............ 56,228
>>> deductAntisym .... 51,689
>>> appThm ........... 17,378
>>> betaConv .......... 6,866
>>> refl .............. 6,325
>>> absThm ............ 4,267
>>> assume ............ 1,608
>>> axiom ............... 190
>>> defineConst .......... 26
>>> defineTypeOp .......... 1
>>> Total ........... 212,678
>>>
>>> real    0m5.289s
>>> user    0m5.027s
>>> sys     0m0.256s
>>>
>>> _______________________________________________
>>> 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