0
$\begingroup$

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" )

  • 0
    Have you seen [this](http://en.wikipedia.org/wiki/Lambda_calculus#Logic_and_predicates)?2012-01-06

1 Answers 1

1

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.

You can easily define the other boolean combinators using the same idea.