Strong Normalization of $\overline{\lambda}\mu\widetilde{\mu}$ -Calculus with Explicit Substitutions

Since Melliès showed that λσ (a calculus of explicit substitutions) does not preserve the strong normalization of the β-reduction, it has become a challenge to find a calculus satisfying the following properties: step-by-step simulation of the β-reduction, confluence on terms with metavariables, strong normalization of the calculus of substitutions and preservation of the strong normalization of the λ-calculus. We present here such a calculus. The main novelty of this calculus (given with de Bruijn indices) is the use of labels that represent updating functions and correspond to explicit weakening. A typed version is also presented.

Download Full-text

Strong normalization of explicit substitutions via cut elimination in proof nets

Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science ◽

10.1109/lics.1997.614927 ◽

2002 ◽

Cited By ~ 10

Author(s):

R. Di Cosmo ◽

D. Kesner

Keyword(s):

Cut Elimination ◽

Strong Normalization ◽

Explicit Substitutions ◽

Proof Nets

Download Full-text

λCalculi with Explicit Substitutions Preserving Strong Normalization

Applicable Algebra in Engineering Communication and Computing ◽

10.1007/s002000050110 ◽

1999 ◽

Vol 9 (4) ◽

pp. 333-371 ◽

Cited By ~ 2

Author(s):

Maria C. F. Ferreira ◽

Delia Kesner ◽

Laurence Puel

Keyword(s):

Strong Normalization ◽

Explicit Substitutions

Download Full-text

Perpetuality in a named lambda calculus with explicit substitutions

Mathematical Structures in Computer Science ◽

10.1017/s0960129500003248 ◽

2001 ◽

Vol 11 (1) ◽

pp. 47-90 ◽

Cited By ~ 8

Author(s):

EDUARDO BONELLI

Keyword(s):

Lambda Calculus ◽

Strong Normalization ◽

Reduction Strategies ◽

Explicit Substitutions ◽

Type Substitution

We study perpetuality in the calculus of explicit substitutions λx. A reduction is called perpetual if it preserves the possibility of infinite reduction sequences. We then take a look at applications of this study: an inductive characterization of the λx-strongly normalizing terms, two perpetual reduction strategies for λx and finally a proof of strong normalization of a polymorphic lambda calculus with explicit substitutions Fes. To complete the study of Fes, the property of subject reduction is shown to hold by extending type assignments of the typing rules to allow non-pure types (types with possible occurrences of the type substitution operator).

Download Full-text