## Tuesday, May 16, 2006

### 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 . xlet 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 FALSElet BoolOr = lambda x y. x TRUE ylet 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`

• 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