An explicit $Eta$ rewrite ruleReportar como inadecuado

An explicit $Eta$ rewrite rule - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 INRIA Lorraine

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

Mots-clés : $\lambda$-calculus explicit substitutions $\eta$-reduction

Autor: Daniel Briaud -



Documentos relacionados