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 `l`t) of Riòs, for which the problem was open.
Document type :
Reports
Complete list of metadatas

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, May 22, 2019 - 1:32:16 AM

File

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

Identifiers

  • HAL Id : hal-02101760, version 1

Collections

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⟩

Share

Metrics

Record views

17

Files downloads

7