HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

An explicit $Eta$ rewrite rule

Abstract : 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$.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 2:52:35 PM
Last modification on : Friday, February 4, 2022 - 3:24:47 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:33:31 PM


  • HAL Id : inria-00074258, version 1



Daniel Briaud. An explicit $Eta$ rewrite rule. [Research Report] RR-2417, INRIA. 1994. ⟨inria-00074258⟩



Record views


Files downloads