# On strong normalisation of explicit substitution calculi

Abstract : 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 lt) of Riòs, for which the problem was open.
Mots-clés :
Document type :
Reports
Domain :

https://hal-lara.archives-ouvertes.fr/hal-02101760
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:05:32 AM
Last modification on : Wednesday, November 20, 2019 - 2:50:25 AM

### File

RR1999-37.pdf
Files produced by the author(s)

### Identifiers

• HAL Id : hal-02101760, version 1

### Citation

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⟩

Record views