How to encode in lambda calculus

Question

I am learning lambda calculus in Haskell and during that, i come across to this question.

And the solution of these question is this :

But I am unable to understand how they conclude the answer. Like for eq, I don't understand how they come to this : λab.a b (b (λxy.y) (λxy.x)) and same for nand. It will be really great if someone explains it and help me to understand this question.

Thank you.

Answer 1

I'm using the Haskell convention of writing λ as \.

From the comments it looks like you are having trouble with this part specifically:

eq = \a b. a b (b (\x y. y) (\x y. x))

So I'll just focus on this.

Our encoding of booleans is as functions which take two arguments. True returns the first argument, False returns the second argument. The first paragraph gives the encoding directly:

True = \x y. x
False = \x y. y

We'll use the names instead of the lambda expressions until the very end.

We know that eq should take two arguments, the two booleans to be compared. (The encoding of booleans itself takes two arguments, but this is different -- eq should take two arguments no matter how booleans are encoded) So we know it should look like:

eq = \a b. _________________

At this point pretty much the only thing we can do is check one of the arguments to find out whether it's True or False. eq is symmetrical so it doesn't really matter which one we ask about; let's pick a for no reason. The way we ask, according to the encoding, is to pass two arguments to the thing we want to find out about.

eq = \a b. a ____ ____

Where we haven't figured out what goes in the "holes" yet. The first hole is what will be returned if a turns out to be True, the second one is what will be returned if it turns out to be False.

To figure out how to fill these holes, let's write the truth table for what we're trying to define:

a     |   b   |  eq a b
------+-------+---------
True  | True  |  True
True  | False |  False
False | True  |  False
False | False |  True

Notice that on the two rows where a is True, the a == b column is the exact same as the b column. So when a is True, we just return b. So we can fill in one of the holes:

eq = \a b. a b ____

Now notice in the table that when a is False, a == b is the opposite of the b column, so in that case we should invert b and return it.

To invert b, we want it to be False when b is True and vice versa. In the encoding, that is:

b False True

And that's what we should return when a is False, so we fill in the other hole:

eq = \a b. a b (b False True)

Now we just unroll the definitions of False and True

eq = \a b. a b (b (\x y. y) (\x y. x))

And there you have it.