[FOM] Simply Typed Lambda Calculus

[Chad E Brown]

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