[Prev][Next][Index][Thread]
Church-Rosser for typed systems
A year or two ago, Furio Honsell pointed out to me that
beta,eta-reduction on terms that look like typed lambda
terms, but are not well-typed, is not Church-Rosser.
The example he showed me was from van Dalen's thesis,
and also mentioned earlier by Nederpelt, so certainly
well-known to the Automath group. A simple example is
\x:A. (\ y:B. y) x
which beta-reduces to \x:A.x, and eta-reduces to \y:B.y.
These are not alpha equivalent (assuming A and B are different).
In particular, this example shows that C-R FOR TYPED LAMBDA
CALCULUS DOES NOT FOLLOW FROM C-R FOR UNTYPED LAMBDA CALCULU,
at least not immediately, and not in any other way I can see.
Any proof of C-R must take the typing rules into account.
(NOTE: I am only speaking about beta, eta-reduction. The
situation is different for beta only.)
I would also like to emphasize that this has nothing to do with
the fact that types are written explicitly using \x:A notation,
instead of the somewhat more common practice of giving each
variable a fixed type. In the alternate presentation,
alpha-conversion must be restricted so that we only replace
one bound variable by another with the same type. With this
restriction, the above example still applies, since \x.x
and \y.y are not alpha-convertible as typed terms when the
types of x and y differ.