 |
HAL-LARA Libre accès aux rapports scientifiques et techniques |
 |
Reports
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.
https://hal-lara.archives-ouvertes.fr/hal-02101760
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:05:32 AM
Last modification on : Saturday, September 11, 2021 - 3:19:21 AM
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:05:32 AM
Last modification on : Saturday, September 11, 2021 - 3:19:21 AM
File
RR1999-37.pdf
Files produced by the author(s)
