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

Let us first write the functions in question with actual data types (but no pattern-matching: only if/then/else):

data Bool = False | True -- recall this definition
not  a   = if a then False else True
eq   a b = if a then (if b then True  else False)
                else (if b then False else True )
nand a b = if a then (if b then False else True )
                else (if b then True  else True )

If you buy these definitions -- which are quite straightforward, just listing the truth tables of the functions -- then we can start doing some reasoning. First, we can simplify the outer branches of the eq and nand functions a little bit:

eq   a b = if a then b else not b
nand a b = if a then not b else True

And now we're basically done. We just replace every False and True with their if/then/else behavior, and replace every if/then/else with function application:

type Bool a = a -> a -> a
false a b = a -- `if False then a else b` becomes `false a b`
true  a b = b -- `if True  then a else b` becomes `true  a b`

not  a   = a false true   -- from `if a then False else True`
eq   a b = a b (not b)    -- from `if a then b else not b`
nand a b = a (not b) true -- from `if a then not b else True`

These are the definitions given in your solutions, though admittedly in Haskell syntax rather than lambda calculus syntax.