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)

A unification method based on the λse-style of explicit substitution is proposed. This method together with appropriate translations, provide a Higher Order Unification procedure for the pure λ-calculus. Our method is influenced by the treatment introduced by Dowek, Hardin and Kirchner using the λσ-style of explicit substitution. Correctness and completeness properties of the proposed λse-unification method are shown and its advantages, inherited from the qualities of the λse-calculus, are pointed out. Our method needs only one sort of objects: terms. And (...) in contrast to the HOU approach based on the λσ-calculus, it avoids the use of substitution objects. This makes our method closer to the syntax of the λ-calculus. Furthermore, detection of redices depends on the search for solutions of simple arithmetic constraints which makes our method more operational than the one based on the λσ-style of explicit substitution. (shrink)