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.