An explicit Eta rewrite rule

Abstract

In this paper, we extend λ-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 η-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 λυ, a calculus introduced by Lescanne (1994). We prove the correction, confluence and strong normalization (on typed terms) of λυη. We also show how this explicit Eta leads to η′, a very general alternative to the classical η, that allows confluent contractions not captured by η.