Mathematics, Logic and Computation
A Satellite workshop of ICALP03
In honour of N.G. de Bruijn's 85th anniversary
4-5 July 2003
Eindhoven, the Netherlands
http://www.cedar-forest.org/forest/events/Bruijn03/
Explicit Substitutions a la de Bruijn: the local and global way
Fairouz Kamareddine and Alejandro Rios
Abstract
Kamareddine and Nederpelt, respectively Kamareddine and
Rios gave two calculi of explicit of substitutions
highly influenced by de Bruijn's notation of the
lambda-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
-
have answered (positively or negatively) the
question of the termination of the underlying calculus of
substitutions.
The exception to 1. is the calculus of Kamareddine and Nederpelt
where substitution is handled both locally and globally. However, the
calculus of Kamareddine and Nederpelt does not satisfy properties like confluence and
termination. The exception to 2. is the lambda se-calculus of Kamareddine and
Rios
for which termination of the se-calculus, the underlying calculus
of substitutions, remains unsolved. This paper has two aims:
-
To provide a calculus a la de Bruijn which deals with local substitution and
whose underlying calculus of
substitutions is terminating and confluent.
-
To pose the problem of the termination of the substitution calculus
of Kamareddine and
Rios
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
lambda sigma-calculus
does not preserve termination, the
sigma-calculus itself terminates. On the other hand, could the
non-preservation of termination in the lambda se-calculus imply the
non-termination of the se-calculus?