### A terminating and confluent linear lambda calculus.

Yo Ohta and Masahito Hasegawa
In
*Proc. 17th
International Conference on Rewriting Techniques and Applications
(RTA'06), Seattle*.

Springer
LNCS 4098, pages 166-180, August 2006.

© Springer-Verlag 2006
### Correction (November 2006)

The paper in the conference proceedings contains various small
technical flows, and a very serious one -
there is a missing rewrite rule:
\z.(let !y be M in let !x be L in N) > let !x be L in \z.(let !y be M in N)

where z is *free* in M.
Without this rule, the system is not locally confluent/coherent
modulo the equivalence relation \sim^*.
In particular, Lemma 1 in the paper fails. For example, consider
M = \z.(let !x be L in let !y be M in N)
M1 = \z.(let !y be M in let !x be L in N)
M2 = let !x be L in \z.(let !y be M in N)

where x is not free in M, and z is free in M.
Then M \sim M1 and M > M2 (via the rule com3), but in general
M1 and M2 are not joinable modulo \sim^*, due to the side condition
on com3.
After adding this rule, all the results in the paper are indeed valid.

Back to Hassei's
Research Page / Home Page