[Prev][Next][Index][Thread]
Re: Church-Rosser for typed systems
The point of the example is this. It is often claimed that
CR for typed lambda calculus follows immediately from CR
for untyped lambda calculus, because every typed term (in
the usual formulation) looks just like an untyped term.
However, that argument applies equally well to the term
\x.(\y.y)x, where x and y have different types. But since
confluence fails from this term (assuming beta, eta), the
reasoning that led you to conclude CR for typed lambda calculus
is flawed. Have I clarified it for you?
John