lambda calculus xor expression by true false

Question

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?

Answer 1

Intuitively, we can think of A XOR B as

1. if A, then not B
2. otherwise, B

.... 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