Direct proofs of strong normalisation in calculi of explicit substitutions
Résumé
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.
Cet article fait partie d'un programme plus général visant à traiter les substitutions explicites comme le sont en général les lambda-calculs aussi bien dans la théorie fondamentale que dans les applications. Ici nous analysons, de ce point de vue, la propriété de normalisation forte. Jusqu'à présent, toutes les preuves de normalisation forte des calculs typés de substitutions explicites s'appuyaient sur une réduction à la normalisation forte du lambda-calcul à travers la propriété dite de ``préservation de la normalisation forte''. Cet article, quant à lui, développe une approche nouvelle, à savoir une preuve directe que les termes fortement normalisables sont précisément les termes qui sont typables par un système de types avec intersection. Mais dans cet article, nous définissons aussi une stratégie perpétuelle effective pour un calcul général de substitutions explicites, nous donnons une définition inductive des termes fortement normalisables et enfin nous montrons que les propriétés de normalisation ne sont pas essentiellement affectées par l'adjonction d'une règle de glanage de cellules. Dans ces démonstrations, un lemme combinatoire général relie deux réductions abstraites qui interagissent et joue un rôle clé dans la preuve de normalisation forte ; nous pensons que ce lemme a un intérêt par lui-même.
Origine : Fichiers produits par l'(les) auteur(s)