Good Math/Bad Math

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 . 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 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 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 Blogger MarkCC, at 3:57 PM  

Post a Comment

Links to this post:

Create a Link

<< Home