[opentheory-users] the Unwanted namespace

[Ramana Kumar]

On Dec 6, 2011 11:02 PM, "Michael Norrish" <Michael.Norrish at nicta.com.au>
wrote:
>
> I think the mistake here is mapping the Abbrev constant to Unwanted.  I'd
say it was probably worth preserving.

Why? What does it mean outside of HOL4?

>
> Michael
>
> On 07/12/11 09:35, Joe Hurd wrote:
> > Hi Ramana,
> >
> > Good job digging up a counter-example to my claim about how tags are
> > used, but I think it's probably not worth the effort to handle exotic
> > cases. Perhaps the theorem you found could be deduced from a form with
> > a fully applied tag?
> >
> > Cheers,
> >
> > Joe
> >
> > On Tue, Dec 6, 2011 at 11:53 AM, Ramana Kumar <ramana.kumar at gmail.com>
wrote:
> >> On Tue, Dec 6, 2011 at 7:36 PM, Joe Hurd <joe at gilith.com> wrote:
> >>> 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.
> >>
> >> I'm not so sure about that. This theorem is from the HOL4 library
> >> (combinTheory.literal_case_FORALL_ELIM):
> >>
> >> |- literal_case f v ⇔ (!) (S ((==>) o Abbrev o C (=) v) f)
> >>
> >> The "Abbrev" constant in the middle there is a tag for abbreviations
> >> (which I map to Unwanted.id).
> >> (This is where, I believe, my axiom in the lazy list theory was coming
from.)
> >>
> >> I'm not sure why this theorem has the form it does, but it could be an
> >> example of a useful not-fully-applied tag.
> >> Perhaps someone who knows more about that theorem could clarify...
> >>
> >>>
> >>> 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
> >>>
> >>> _______________________________________________
> >>> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20111207/ad0795fd/attachment-0001.htm>