Booleans and Choice in Lambda Calculus

Now that we have numbers in our Lambda calculus, there are only two things missing before we can express arbitrary computations: a way of expressing choice, and a way of expressing repetition. In this post, I'll talk about booleans and choice; and then next post I'll explain repetition and recursion.

We'd like to be able to write choices as if/then/else expressions, like we have in most programming languages. Following the basic pattern of the church numerals, where a number is expressed as a function that adds itself to another number, we'll express true and false values as functions that perform an if-then-else operation on their parameters:

let TRUE = lambda x y . x
let FALSE = lambda x y . y

So, now we can write an "if" function, whose first parameter is a condition expression, second parameter is the expression to evaluate if the condition was true, and third parameter is the expression to evaluate if the condition is false.

let IfThenElse = lambda cond true_expr false_expr . cond true_expr false_expr

For the boolean values to be useful, we also need to be able to do the usual logical operations:

let BoolAnd = lambda x y .x y FALSE
let BoolOr = lambda x y. x TRUE y
let BoolNot = lambda x . x FALSE TRUE

Now, let's just walk through those a bit. Let's first takea look at BoolAnd:

BoolAnd TRUE FALSE
Expand the TRUE and FALSE definitions: BoolAnd (lambda x y . x) (lambda x y . y)
Alpha the true and false: BoolAnd (lambda xt yt . xt) (lambda xf yf . yf)
Now, expand BoolAnd: (lambda x y. x y FALSE) (lambda xt yt . xt) (lambda xf yf . yf)
And beta: (lambda xt yt.xt) (lambda xf yf. yf) FALSE
Beta again: (lambda xf yf . yf)

And we have the result: BoolAnd TRUE FALSE = FALSE. Now let's look at "BoolAnd FALSE TRUE":
BoolAnd (lambda x y . y) (lambda x y .x)
Alpha: BoolAnd (lambda xf yf . yf) (lambda xt yt . xt)
Expand BoolAnd: (lambda x y .x y FALSE) (lambda xf yf . yf) (lambda xt yt . xt)
Beta: (lambda xf yf . yf) (lambda xt yt . xt) FALSE
Beta again: FALSE
So BoolAnd FALSE TRUE = FALSE

Finally, BoolAnd TRUE TRUE:
Expand the two trues: BoolAnd (lambda x y . x) (lambda x y . x)
Alpha: BoolAnd (lambda xa ya . xa) (lambda xb yb . xb)
Expand BoolAnd: (lambda x y . x y FALSE) (lambda xa ya . xa) (lambda xb yb . xb)
Beta: (lambda xa ya . xa) (lambda xb yb . xb) FALSE
Beta: (lambda xb yb .xb)
So BoolAnd TRUE TRUE = TRUE