In a so-called optimal implementation of a term rewriting system, only needed redexes are contracted and all redex-patterns in a term which have the same history along the reduction, are kept shared in the graph implementation of the term. Such an implementation crucially relies on the notion of `being the same along a reduction' of redex-patterns in particular, and of parts of terms in general.
Lévy gave three ways to characterize this notion of sameness, in the case of the lambda-calculus. Via:
We conclude by presenting an extension of the lambda-calculus with an end-of-scope operator, which came up naturally, while extending the optimal first-order setting to higher-order. The rough idea is that a role of the lambda is to open a scope and it is only natural to introduce an explicit operator to end a scope. The nice thing is that (an extension of) beta-reduction can be defined which is confluent without alpha-reduction. Alpha reduction is only needed when removing end-of-scopes. (This calculus is halfway toward an optimal implementation of the lambda calculus: for that also the explicit operators for (un)sharing, the so-called fan-in and fan-out, need to be introduced.)
The first part of the talk is based on Chapter 8, joint work with Roel de Vrijer, of the forthcoming book on Term Rewriting Systems, by Terese. The second part of the talk on the lambda calculus with scopes, is based on joint work (in progress) with Dimitri Hendriks who's also working on a formalization in Coq. The extension to higher-order is joint work-in-progress with Sander Bruggink.