*To*: András Kovács <puttamalac at gmail.com>*Subject*: Re: [isabelle] [Agda] [Coq-Club] Prior work on proof assistant performance / optimization*From*: Wolfram Kahl <kahl at cas.mcmaster.ca>*Date*: Tue, 12 May 2020 16:35:22 -0400*Cc*: coq-club <coq-club at inria.fr>, Coq Discourse <coq+miscellaneous at discoursemail.com>, cl-isabelle-users at lists.cam.ac.uk, Stefan Monnier <monnier at iro.umontreal.ca>, lean-user <lean-user at googlegroups.com>, agda-list <agda at lists.chalmers.se>*In-reply-to*: <CAA3CDBa8sLdn37CXxZLPwS4hEMrbUTSvstTnmsxphHT9Wwtm5Q@mail.gmail.com>*References*: <CAKObCaqa5NZvJvU_ZpZek+OnVEOQETiYpisbgJXhPchMn6PLcQ@mail.gmail.com> <CAKObCar-44SM0gMLi0jMbkqU1hJ+AvoWQ_wJyhbr=DAQL3qcCQ@mail.gmail.com> <CAA3CDBZt4CyJPapH6jLZudJuC3vjn3+cuCLAdHifp-3P-PhnDg@mail.gmail.com> <jwv1rnp2q29.fsf-monnier+types@gnu.org> <CAA3CDBa8sLdn37CXxZLPwS4hEMrbUTSvstTnmsxphHT9Wwtm5Q@mail.gmail.com>

On Tue, May 12, 2020 at 05:15:17PM +0200, András Kovács wrote: > Stefan Monnier <monnier at iro.umontreal.ca> ezt írta (időpont: 2020. máj. > 12., K, 16:30): > > > > Could you elaborate on this "sharing loss from beta-redexes"? > > We may have a huge Peano numeral which is represented by a small term, > because we can use iteration/recursion to give short descriptions of large > numerals. Then, we can beta-reduce from a small term to a large numeral, > but we cannot go from a large numeral to a small term. In particular, Peano > numerals are incompressible by hash consing. Hash consing only does > "delta-contraction", i.e. contracting terms by maximally introducing > let-definitions, but it is intractable to invent small terms which beta > reduce to a given term (related: Kolmogorov complexity). So technically, the lost sharing is the second-order sharing that is preserved in ``optimal reduction'' of lambda calculi [Levy-1980, Lamping-1990, Asperti-Laneve-1992], while hash consing normally is directly usable only for first-order sharing. Wolfram

**References**:**[isabelle] Prior work on proof assistant performance / optimization***From:*Jason Gross

- Previous by Date: Re: [isabelle] Bug in the algebra method for ideal membership
- Next by Date: [isabelle] new in the AFP: Recursion Theorem in ZF
- Previous by Thread: Re: [isabelle] Prior work on proof assistant performance / optimization
- Next by Thread: Re: [isabelle] [Agda] Prior work on proof assistant performance / optimization
- Cl-isabelle-users May 2020 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list