** Next:** Axiomatic Rewriting Systems
**Up:** Foundational models and abstract
** Previous:** Foundational models and abstract

The theory of optimal sharing in -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 -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 -steps
is polynomial. More precisely, it is polynomial in the size of some
-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)
-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
-reduction is not elementary recursive*.
Proc. of the twenty-fifth Annual ACM SIGACT-SIGPLAN Symposium
on Principles of Programming Languages (POPL'98).