[FOM] Simply Typed Lambda Calculus
Chad E Brown
cebrown2323 at yahoo.com
Wed Jan 16 20:44:24 EST 2008
Steven,
I suspect this is an example proving you cannot forget the types
without introducing new equations.
Let o be a base type, T and F be constants of type o,
Q be a constant of type ooo, and
N, C, and D be constants of type oo.
The following axioms are well typed, the left hand sides
are linear patterns, and the right hand sides only contain
free variables contained on the left:
(1) C x = Q x x
(2) D x = Q (N x) x
(3) C x = T
(4) D x = F
In the typed calculus, we cannot prove T = F.
(Consider the interpretation in which Q is equivalence and N is negation.)
Using untyped terms, we can prove T = F.
Let Y = (W W) where W = (\z.(N (z z))) so that Y = (N Y).
Then
T = C Y = Q Y Y = Q (N Y) Y = D Y = F.
Does this answer your question?
Chad
---------------------------------
Looking for last minute shopping deals? Find them fast with Yahoo! Search.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: /pipermail/fom/attachments/20080116/87a699bf/attachment-0001.html
More information about the FOM
mailing list