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.
Origine | Fichiers produits par l'(les) auteur(s) |
---|