An explicit $Eta$ rewrite rule
Résumé
In this report, we extend $\la$-calculi of explicit substitutions by an $Eta$ rule. We do this in the framework of $\la\ups$, a $\la$-calculus of explicit substitutions introduced in~\citeLescannePOPL94 and thoroughly studied in~\citeLescanneR94. The main feature of such a calculus is that the classical $\beta$-contraction is expressed by a first-order term rewriting system. Our main result is the explicitation of the $\eta$-contraction by means of an unconditional, \it generic $Eta$ rewrite rule and of an extension of the substitution calculus, $\upsilon$. %Similar results Previous definitions of $Eta$ are due to~\citeHardin92 and~\citeRiosTHESE in the framework of $\la\sigma$-calculi. The principal difference between $\la\upsilon$ and $\la\sigma$-calculi concerns confluence and strong normalization\,: $\la\upsilon$ is ground confluent and its simply typed version is terminating, whenever $\la\sigma_\Lift$\ -calculus is confluent on open terms but non terminating on typed terms. In~\citeHardin92 and~\citeRiosTHESE, $Eta$ rule is presented as an extension of $\eta$-contraction. Hardin and R\'\ios present their extension as a conditional rewrite rule and do not stick fully to the philosophy of explicit substitutions. In our approach, the $Eta$-rule is a first order rewrite rule which uses an explicit substitution calculus. For that, one needs to introduce a new constant $\bot$ that denotes an unspecified term. Its behaviour is described by a rewrite rule. This report shows, in the one hand, how the $Eta$-rule associated with $\la\ups$ and the rule for $\bot$ provides a correct implementation of the $\eta$-reduction and studies other properties of the $\la\ups\eta$-calculus namely confluenceon ground terms and strong normalisation on typed terms. On the other hand, this explicit $Eta$ leads to $\eta'$ a very general alternative to the classical $\eta$. Indeed, we prove that $\eta'$ allows confluent contractions which are not captured by classical $\eta$.