I am trying to understand xor in context on lambda calculus. I understand xor (Exclusive or) as boolean logic operation in https://en.wikipedia.org/wiki/Exclusive_or and the truth table of xor.
But how why is it true as a xor b=(a)((b)(false)(true))(b) from http://safalra.com/lambda-calculus/boolean-logic/ it is indeed what what expect in lambda calculus. When I saw true=λab.a false=λab.b I kinda have to see the true and false as a lambda calc true and false since it returns the first element in case of true. But is it correct to understand that the xor here is also a name but not the same as xor in boolean logic?
Intuitively, we can think of A XOR B as
.... or in some pseudocode:
func xor (a,b)
if a then
return not b
else
return b
Let's get lambda calculusing
true := λa.λb.a
false := λa.λb.b
true a b
// a
false a b
// b
next we'll do not
not := λp.p false true
not true a b
// b
not false a b
// a
we can do if next (note, that this is sort of silly since true and false already behave like if)
if := λp.λa.λb.p a b
if true a b
// a
if false a b
// b
Ok, lastly write xor
xor := λa.λb.if a (not b) b
(xor true true) a b
// b
(xor true false) a b
// a
(xor false true) a b
// a
(xor false false) a b
// b
Remember if is kind of dumb here, we can just remove it
xor := λa.λb.a (not b) b
Now if we want to write it all with pure lambda, just replace the not with its definition
xor := λa.λb.a (not b) b
->β [ not := λp.p false true ]
xor := λa.λb.a ((λp.p false true) b) b
->β [ p := b ]
xor := λa.λb.a (b false true) b
At this point, you can see we have the definition from your question
a xor b = (a)((b)(false)(true))(b)
But of course that introduced additional free variables false and true – you can replace those with a couple additional beta reductions
xor := λa.λb.a (b false true) b
->β [ false := (λa.λb.b) ]
xor := λa.λb.a (b (λa.λb.b) true) b
->β [ true := (λa.λb.a) ]
// pure lambda definition
xor := λa.λb.a (b (λa.λb.b) (λa.λb.a)) b