Query on Booleans in Lambda Calculus

Question

This is the lambda calculus representation for the AND operator:

lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b

Can anyone help me in understanding this representation?

Parted

Answer 1

To understand how to represent Booleans in lambda calculus, it helps to think about an IF expression, "if a then b else c". This is an expression which chooses the first branch, b, if it is true, and the second, c, if it is false. Lambda expressions can do that very easily:

lambda(x).lambda(y).x

will give you the first of its arguments, and

lambda(x).lambda(y).y

gives you the second. So if a is one of those expressions, then

a b c

gives either b or c, which is just what we want the IF to do. So define

 true = lambda(x).lambda(y).x
false = lambda(x).lambda(y).y

and a b c will behave like if a then b else c.

Looking inside your expression at (n a b), that means if n then a else b. Then m (n a b) b means

if m then (if n then a else b) else b

This expression evaluates to a if both m and n are true, and to b otherwise. Since a is the first argument of your function and b is the second, and true has been defined as a function that gives the first of its two arguments, then if m and n are both true, so is the whole expression. Otherwise it is false. And that's just the definition of and!

All this was invented by Alonzo Church, who invented the lambda calculus.

Ulrich

Thank you so very much !!! I am finding Lambda Calculus really difficult to understand and such explanations make my life a lot easier !! Thank you again. – Parted

@Peter: Just another help needed, if you can: I am reading Church Booleans on wikipedia: en.wikipedia.org/wiki/Church_encoding#Church_booleans I am not able to understand how the examples are inferred i.e. AND TRUE FALSE. Can you help me understand them? – Parted

The way to understand those long expressions is just to remember the rules and evaluate them one step at a time, left to right. So in the expression (λm.λn. m n m) (λa.λb. a) (λa.λb. b) the first part in parentheses is a function, and the second and third parts get substituted for m and n:(λa.λb. a) (λa.λb. b) (λa.λb. a). Then do the same thing again, remembering that the a and b in each parenthesis are completely independent of each other. The first part, (λa.λb. a), returns the first of its two arguments. So it returns (λa.λb. b), which is the Church representation of false. – Ulrich

Great Peter !!! Thank you very much. Did you learn Lambda Calculus in school or you read any documentation to get this level of understanding? Also, another question I have is: (lambda (a) (lambda (b) ((lambda (c) c) b))) In this case, is the outer 'c' of "(lambda (c) c)" a free variable or a bounded variable ?? – Parted

I think I first saw lambdas in a book on Lisp, then a book on Denotational Semantics. I don't recall where Booleans came into it, but I did have great fun reconstructing how they worked after I had forgotten! Enjoying it is the secret to understanding it. For your question, the outer "c" is bound, because it's named in the "lambda (c)" part. – Ulrich

Woww !! That's really great that you still remember ... Thanks a lot for your help Peter !! – Parted

Answer 2

In the lambda calculus, a Boolean is represented by a function that takes two arguments, one for success and one for failure. The arguments are called continuations, because they continue with the rest of the computation; the boolean True calls the success continuation and the Boolean False calls the failure continuation. This coding is called the Church encoding, and the idea is that a Boolean is very much like an "if-then-else function".

So we can say

true  = \s.\f.s
false = \s.\f.f

where s stands for success, f stands for failure, and the backslash is an ASCII lambda.

Now I hope you can see where this is going. How do we code and? Well, in C we could expand it to

n && m = n ? m : false

Only these are functions, so

(n && m) s f = (n ? m : false) s f = n ? (m s f) : (false s f) = n ? (m s f) : f

BUT, the ternary construct, when coded in the lambda calculus, is just function application, so we have

(n && m) s f = (n m false) s f = n (m s f) (false s f) = n (m s f) f

So finally we arrive at

&& = \n . \m . \s . \f . n (m s f) f

And if we rename the success and failure continuations to a and b we return to your original

&& = \n . \m . \a . \b . n (m a b) b

As with other computations in lambda calculus, especially when using Church encodings, it is often easier to work things out with algebraic laws and equational reasoning, then convert to lambdas at the end.

Prestissimo

Answer 3

Actually it's a little more than just the AND operator. It's the lambda calculus' version of if m and n then a else b. Here's the explanation:

In lambda calculus true is represented as a function taking two arguments* and returning the first. False is represented as function taking two arguments* and returning the second.

The function you showed above takes four arguments*. From the looks of it m and n are supposed to be booleans and a and b some other values. If m is true, it will evaluate to its first argument which is n a b. This in turn will evaluate to a if n is true and b if n is false. If m is false, it will evaluate to its second argument b.

So basically the function returns a if both m and n are true and b otherwise.

(*) Where "taking two arguments" means "taking an argument and returning a function taking another argument".

Edit in response to your comment:

and true false as seen on the wiki page works like this:

The first step is simply to replace each identifier with its definition, i.e. (λm.λn. m n m) (λa.λb. a) (λa.λb. b). Now the function (λm.λn. m n m) is applied. This means that every occurrence of m in m n m is replaced with the first argument ((λa.λb. a)) and every occurrence of n is replaced with the second argument ((λa.λb. b)). So we get (λa.λb. a) (λa.λb. b) (λa.λb. a). Now we simply apply the function (λa.λb. a). Since the body of this function is simply a, i.e. the first argument, this evaluates to (λa.λb. b), i.e. false (as λx.λy. y means false).

Ane

@sepp: Can you help me out, if you can with the 2nd comment posted by me below to Peter? – Parted