An explicit $$Eta$$ rewrite rule.(English)Zbl 1063.68552

Dezani-Ciancaglini, Mariangiola (ed.) et al., Typed lambda calculi and applications. 2nd international conference, TLCA ’95, Edinburgh, GB, April 10-12, 1995. Proceedings. Berlin: Springer-Verlag (ISBN 3-540-59048-X). Lect. Notes Comput. Sci. 902, 94-108 (1995).
Summary: In this paper, we extend $$\lambda$$-calculi of explicit substitutions by an $$Eta$$ rule. The previous definition of $$Eta$$ is due to Hardin (1992) and Ríos (1993). Their definition is a conditional rewrite rule and does not stick fully to the philosophy of explicit substitutions. Our main result is making the $$\eta$$-contraction explicit by means of an unconditional, generic $$Eta$$ rewrite rule and of an extension of the substitution calculus. We do this in the framework of $$\lambda \upsilon$$, a calculus introduced by Lescanne (1994). We prove the correction, confluence and strong normalization (on typed terms) of $$\lambda \upsilon\eta$$. We also show how this explicit $$Eta$$ leads to $$\eta'$$, a very general alternative to the classical $$\eta$$, that allows confluent contractions not captured by $$\eta$$.
For the entire collection see [Zbl 0813.68040].

MSC:

 68N18 Functional programming and lambda calculus 03B40 Combinatory logic and lambda calculus 68Q42 Grammars and rewriting systems