On strong normalisation of explicit substitution calculi

Frédéric Lang (1) , Pierre Lescanne (1)

1 LIP - Laboratoire de l'Informatique du Parallélisme

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.

Mots clés: Explicit Substitution; Lambda Calculus; Strong Normalisation; Termination

Mots clés: Confluence; Lambda Calcul; Normalisation Forte; Substitution Explicite; Terminaison

Domaines: Informatique [cs]

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⟩