[Agda] [Coq-Club] Prior work on proof assistant performance / optimization

[Wolfram Kahl]

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