Sciweavers

ENTCS
2002

Comparing Calculi of Explicit Substitutions with Eta-reduction

13 years 3 months ago
Comparing Calculi of Explicit Substitutions with Eta-reduction
The past decade has seen an explosion of work on calculi of explicit substitutions. Numerous work has illustrated the usefulness of these calculi for practical notions like the implementation of typed functional programming languages and higher order proof assistants. Three styles of explicit substitutions are treated in this paper: the and the se which have proved useful for solving practical problems like higher order unification, and the suspension calculus related to the implementation of the language Prolog. We enlarge the suspension calculus with an adequate etareduction which we show to preserve termination and confluence of the associated substitution calculus and to correspond to the eta-reductions of the other two calculi. Additionally, we prove that and se as well as and the suspension calculus are non comparable while se is more adequate than the suspension calculus.
Mauricio Ayala-Rincón, Flávio L. C.
Added 21 Dec 2010
Updated 21 Dec 2010
Type Journal
Year 2002
Where ENTCS
Authors Mauricio Ayala-Rincón, Flávio L. C. de Moura, Fairouz Kamareddine
Comments (0)