# implementation of xnor with lambda

i dont know how to ask my question but here it is...

i have implementation of "NOT" and "True" and "false",but if i want to have "xnor" according to the example beneath:

(true) T--->λx.λy.x

(false) F----> λx.λy.y

(true) Q =((TQ)P) => ((λX.λY.X Q)P= (λY.Q)P=Q (false) P =((FQ)P) => ((λX.λY.Y Q)P= (λY.Y)P=P

Not ---> λx.((xF)T)

Not T ---> λx.((xF)T) T = ((TF)T=F

Not F ---> λx.((xF)T) F = ((FF)T=T

what "xnor" will be according to these examples? i have "not" ,"true" and "false",how i can get "xnor" or "or" or "and" ?(cause i can get to the Xnor with at least "or" and "and" )

-
Have you seen this? –  Matt N. Jan 6 '12 at 18:33
thank you so much –  sam Jan 6 '12 at 18:37

The reason we define $$T = \lambda x. \lambda y. x$$ $$F = \lambda x. \lambda y. y$$ is so that you can easily define an "if" function $Q$ satisfying $$QTxy = x$$ $$QFxy = y$$ by $Qxyz = xyz$ (so $Q = \lambda x. \lambda y. \lambda z. x y z$).
Now it's easy to write things like an "and" function $A$ satisfying $$ATT = T$$ $$ATF = F$$ $$AFy = F$$ by $Axy = Qx(QyTF)F$ so $A = \lambda x. \lambda y. Qx(QyTF)F$. You could unfold the definition of $Q$ inside $A$ and beta reduce it a bit, but that will just give a slightly more compresses lambda term.