Pure Lambda Calculus - and function

Question

I am currently learning Haskell and also participating in a rather theoretical lecture about functional programming at university.

I know that this is purely theoretical/academic question, but nevertheless I am interested how to express different simple functions simply with pure lambda calculus (i.e. without any constants defined).

Some lecture materials of mine define the boolean values such as:

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

(\ denoting the lambda symbol)

If they are defined like these selector functions, the if-condition can be easily defined as:

If = \x.x

Now, I'm trying to come up with some short form for the logical "and"-function. My first guess is:

and = \xy.{(If x)[(If y) True False] False}

So basically this lambda function would receive 2 arguments u v where both have to be typed like True/False. If I do various beta-reductions with all 4 combinations of the logic table I receive the right result.

Nevertheless this function looks a little ugly and I'm thinking about making it more elegant. Any proposals here?

Answer 1

We can just do reductions on your answer to get a pithier one.

First some warm-ups. Obviously IF x ==> x, and as TRUE TRUE FALSE ==> TRUE and FALSE TRUE FALSE ==> FALSE if x is a boolean then x TRUE FALSE ==> x.

Now we reduce

\x y . (IF x) ( (IF y) TRUE FALSE ) FALSE
\x y .     x  (     y  TRUE FALSE ) FALSE  -- using IF x         ==> x
\x y .     x  (     y             ) FALSE  -- using y TRUE FALSE ==> y
\x y . x y FALSE                           -- clean up

and this expression still works with truth tables

AND TRUE  TRUE  = TRUE  TRUE  FALSE = TRUE
AND FALSE TRUE  = FALSE TRUE  FALSE = FALSE
AND TRUE  FALSE = TRUE  FALSE FALSE = FALSE
AND FALSE FALSE = FALSE FALSE FALSE = FALSE