Optimal reductions in the $\lambda$-calculus

The theory of optimal sharing in $\beta$-reduction had many significant improvements recently (see the results of Asperti, Gonthier, Laneve, and Lévy in BRA Confer-1). In 1977, Lévy designed the notion of so-called family-complete reductions, optimal in the number of $\beta$-steps. Each of the elementary steps had to contract a set of redexes, and these steps were unit costs. In 1988, Lamping exhibited a data structure and an algorithm, fitting these costs. He heavily used shared structures to keep a single object to contract in each of the elementary steps of family-complete reductions. However, between each of these steps, several bookkeeping operations were needed to share or unshare objects.

Asperti and Mairson (Brandeis University) showed that the number of these bookeeping steps was very large. In fact their number is not elementary recursive in the size of the original term, decorated by the type of all its subterms, whereas the number of $\beta$-steps is polynomial. More precisely, it is polynomial in the size of some $\eta$-expansion of the initial term. This means that the notion of optimal ``parallel'' reduction, as formalized by Lèvy, is not elementary recursive. It cannot have a simple implementation since, essentially, all the computational work can be done via sharing. Actually, the result is a straightforward consequence of the fact that every term of the simply typed lambda calculus can be essentially reduced in a linear number of ``parallel'' (i.e. sharable) $\beta$-reduction. [AM98]

The result should not be understood in a too negative sense. On the road to this result, many interesting and fine properties have been found in the behaviour of redexes families, which can be of use for other areas such as sequentiality or strong normalisation.

[[AM98]] A. Asperti, H.Mairson Optimal $\beta$-reduction is not elementary recursive. Proc. of the twenty-fifth Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'98).