On strong normalisation of explicit substitution calculi - LARA - Libre accès aux rapports scientifiques et techniques Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1999

On strong normalisation of explicit substitution calculi

Résumé

In this paper, we present an attempt to build a calculus of explicit substitution expected to be confluent on open terms, to preserve strong normalisation and to simulate one step `b-reduction. We show why our attempt failed and we explain how we found a counter-example to the strong normalisation or termination of the substitution calculus. As a consequence, we provide also a counter-example to the strong normalisation of another calculus, namely~`t (the substitution calculus of `l`t) of Riòs, for which the problem was open.
Dans cet article, nous rendons compte d'une tentative pour construire un calcul de substitutions explicite sensé être confluent sur les termes ouverts, préserver la forte normalisation et simuler la `b-r\'eduction en une seule étape. Nous montrons pourquoi notre tentative a échoué et nous expliquons comment nous avons trouvé un contrexemple à la terminaison du calcul de substitutions. Comme conséquence nous exhibons un contrexemple à la forte normalisation d'un autre calcul à savoir le calcul `t (le calcul de substitution de `l`t) de Riòs, pour lequel le problème était ouvert.
Fichier principal
Vignette du fichier
RR1999-37.pdf (230.59 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-02101760 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02101760 , version 1

Citer

Frédéric Lang, Pierre Lescanne. On strong normalisation of explicit substitution calculi. [Research Report] LIP RR-1999-37, Laboratoire de l'informatique du parallélisme. 1999, 2+11p. ⟨hal-02101760⟩
19 Consultations
23 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More