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].


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