The past decade has seen an explosion of work on calculi of explicit substitutions. Numerous works have illustrated the usefulness of these calculi for practical notions like the implementation of typed functional programming languages and higher order proof assistants. It has also been shown that eta-reduction is useful for adapting substitution calculi for practical problems like higher order unification. This paper concentrates on rewrite rules for eta-reduction in three different styles of explicit substitution calculi: λσ, λse and the suspension calculus. (...) Both λσ and λse when extended with eta-reduction rules, have proved useful for solving higher order unification. We enlarge the suspension calculus with an adequate eta-reduction rule which we show to preserve termination and confluence of the associated substitution calculus and to correspond to the eta rules of the other two calculi. We prove that λσ and λse as well as λσ and the suspension calculus are non-comparable while λse is more adequate than the suspension calculus in simulating one-step beta-reduction. After defining the eta-reduction rule in the suspension calculus, and after comparing these three calculi of explicit substitutions , we then concentrate on the implementation of the rewrite rules of eta-reduction in these calculi. We note that it is usual practice when implementing the eta rule for substitution calculi, to mix isolated applications of eta-reduction with the application of other rules of the corresponding substitution calculi. The main disadvantage of this practice is that the eta rewrite rules so obtained are unclean because they have an operational semantics different from that of the eta-reduction of the λ-calculus. For the three calculi in question enlarged with adequate eta rules we show how to implement these eta rules. For the λse we build a clean implementation of the eta rule and we prove that it is not possible to follow the same approach for the λσ and λsusp. (shrink)

We present the system SUBSEXPL used for simulating and comparing explicit substitutions calculi. The system allows the manipulation of expressions of the λ-calculus and of three different styles of explicit substitutions: the λσ, the λse and the suspension calculus. A variation of the suspension calculus, which allows for combination of steps of β-contraction is included too. Implementations of the η-reduction are provided for each style. Other explicit substitutions calculi can be easily incorporated into the system due to its modular structure. (...) The uses of the system include: the visualization of the contractions of the λ-calculus in de Bruijn notation, and of guided one-step reductions as well as normalization via each of the associated substitution calculi. Many useful facilities are included: reductions can be easily recorded as text files, LATEX outputs can be generated and several examples for dealing with arithmetic operations and computational operators such as conditionals and repetitions in the λ-calculus are available. The system can be executed over Emacs using the x-symbol mode in such a way that λ-terms and terms of the explicit substitutions calculi are represented in its natural syntax avoiding the necessity of repeatedly generating LATEX outputs. The system has been of great help for systematically comparing explicit substitutions calculi, as well as for understanding properties of explicit substitutions such as the Preservation of Strong Normalization. In addition, it has been used for teaching basic properties of the λ-calculus such as: computational adequacy, the usefulness of de Bruijn's notation and of making explicit substitutions in real implementations. (shrink)