### 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:

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.

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

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

Expand the TRUE and FALSE definitions:

Alpha the true and false:

Now, expand BoolAnd:

And beta:

Beta again: (lambda xf yf . yf)

And we have the result: BoolAnd TRUE FALSE = FALSE. Now let's look at "BoolAnd FALSE TRUE":

Alpha:

Expand BoolAnd:

Beta:

Beta again: FALSE

So

Finally, BoolAnd TRUE TRUE:

Expand the two trues:

Alpha:

Expand BoolAnd:

Beta:

Beta:

So

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`

## 3 Comments:

You defined IfThenElse and then never gave an example of using it. :)

By Anonymous, at 9:38 AM

If we're going to be pedantic, isn't there something special also about your "cond" construct that you've introduced?

I can't quite put my finger on what it is...

By Anonymous, at 3:23 PM

Sorry, but I don't understand what you mean about the conditional construct.

Perhaps it's evaluation order? In lambda calc, you can select different orders in which to perform the betas; I'm mostly using the lazy (head-normal) order. In that case, in the cond construct, only the selected branch is ever evaluated; if you use eager evaluation, then you'd evaluate both the true and false branches, but only return one. That would become important once we add recursion, because the Y combinator form that I use will expand forever if you do eager evaluation.

Is that it? If not, you'll have to try to explain what you're getting at a bit more.

By MarkCC, at 3:57 PM

Post a Comment

<< Home