Direct proofs of strong normalisation in calculi of explicit substitutions

Abstract : This paper is part of a general programme of treating explicit substitutions as the primary $\lambda$-calculi from the point of view of foundations as well as applications. Here we investigate the property of strong normalization. To date all the proofs of strong normalization of typed calculi of explicit substitutions use a reduction to the strong normalization of classical $\lambda$-calculus via the so-called ``preservation of strong normalization'' property. This paper develops a new approach, namely a direct proof that the strongly normalizing terms are precisely those typable under the intersection-types discipline. We also define an effective perpetual strategy for the general calculus, give an inductive definition of the strongly normalizing terms, and furthermore show that normalization properties are essentially unaffected by the inclusion of a rule for garbage collection. A key role is played by a certain general combinatorial lemma relating the reduction properties of two interacting abstract reductions, which we feel is of interest in its own right.
Document type :
Reports
Complete list of metadatas

https://hal-lara.archives-ouvertes.fr/hal-02101884
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:08:57 AM
Last modification on : Friday, May 17, 2019 - 1:39:22 AM

File

RR2000-05.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101884, version 1

Collections

Citation

Daniel Dougherty, Pierre Lescanne. Direct proofs of strong normalisation in calculi of explicit substitutions. [Research Report] LIP RR-2000-05, Laboratoire de l'informatique du parallélisme. 2000, 2+20p. ⟨hal-02101884⟩

Share

Metrics

Record views

3

Files downloads

8