Lambda Calculus, Logical operators

We saw that we can use the following abstractions to define True, False and If-Then-Else statement:

True  :  λxy.x
False :  λxy.y

if p then x else y : λpxy.p x y 

We are going to use these three abstractions and the reductions rules we talked about before to show how easily we can drive the logical operators in lambda calculus.

Logical AND

There are many ways we can define abstractions for logical operators, let us start with a sample for logical AND. We can define AND operator as follow:

λx.λy.x y x

To show it is correct abstraction, it must comply the truth table of logical AND operator, so if x equals to True and y equals to False we have:



(λx.λy.x y x) True False → True False True → (λxy.x) False True → False

Or when x equals to False and y equals to True:

(λx.λy.x y x) False True → False True False → (λxy.y) True False → False

Or when both x and y equal to True:

(λx.λy.x y x) True True → True True False → (λxy.x) True True → True

Or when both x and y equal to False:

(λx.λy.x y x) False False → False False False → (λxy.y) False False → False

As you see, the abstraction λx.λy.x y x completely fulfills the logical AND operator's truth table. Note that as I told before we can have other abstractions which defines logical AND operator too like:

λx.λy.x y False

Logical OR

Same as logical AND we can define logical OR as follows:

λx.λy.x x y

To proof it obeys logical OR truth table, like what we did for AND operator, we have to show in each case of the table the result of the abstraction is like logical OR truth table. Let us see what happens if we have x equal to True and y equals to False:

(λx.λy.x x y) True False → True  True False → (λxy.x) True True → True

Or when x equals to False and y equals to True we have:

(λx.λy.x x y) False True → False False True → (λxy.y) False True → True

Or when both are True:

(λx.λy.x x y) True True → True  True True → (λxy.x) True True → True

And finally, when both are False we have:

(λx.λy.x x y) False False → False  False False → (λxy.y) False False → False

We can also define logical OR abstraction as follows:

λx.λy.x true y

Logical NOT
Like we brought fro logical AND and OR operators we can define NOT as bellow, the proof is as easy as before:

λx.x False True

Logical XOR

Logical XOR may seem a little bit complicated, we can show this abstraction as follows:

λx.λy.x (not y) y

It should return False if bot x and y are False or true, let us see:

(λx.λy.x (not y) y) True True → True False True → (λxy.x) False True → False

(λx.λy.x (not y) y) False False → False True False → (λxy.y) True False → False

and should return True when one of the x or y is true and the other is false:

(λx.λy.x (not y) y) False True → False False True → (λxy.y) False True → True

(λx.λy.x (not y) y) True False → True True False  → (λxy.x) True True → True