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.

[pdf file]

© 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