Explicit substitutions à la de Bruijn: The local and global way

Fairouz Kamareddine, Alejandro Ríos

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


Kamareddine and Nederpelt, resp. Kamareddine and Ríos [11] gave two calculi of explicit of substitutions highly influenced by de Bruijn's notation of the ?-calculus. These calculi added to the explosive pool of work on explicit substitution in the past 15 years. As far as we know, calculi of explicit substitutions: a) are unable to handle local substitutions, and b) have answered (positively or negatively) the question of the termination of the underlying calculus of substitutions. The exception to a) is the calculus of [9] where substitution is handled both locally and globally. However, the calculus of [9] does not satisfy properties like confluence and termination. The exception to b) is the ?se-calculus of [11] for which termination of the se-calculus, the underlying calculus of substitutions, remains unsolved. This paper has two aims:(i) To provide a calculus à la de Bruijn which deals with local substitution and whose underlying calculus of substitutions is terminating and confluent.(ii) To pose the problem of the termination of the substitution calculus of [11] in the hope that it can generate interest as a termination problem which at least for curiosity, needs to be settled. The answer here can go either way. On the one hand, although the ?s-calculus [1] does not preserve termination, the s-calculus itself terminates. On the other hand, could the non-preservation of termination in the ?se-calculus imply the non-termination of the se-calculus? ©2003 Published by Elsevier Science B. V.

Original languageEnglish
Pages (from-to)91-110
Number of pages20
JournalElectronic Notes in Theoretical Computer Science
Issue number7
Publication statusPublished - Sept 2003


Dive into the research topics of 'Explicit substitutions à la de Bruijn: The local and global way'. Together they form a unique fingerprint.

Cite this