If we define true and false with the following combinators (in Python):

TRUE = lambda a: lambda b: (a) FALSE = lambda a: lambda b: (b)

then if-then-else can be implemented simply by applying a predicate to two arguments: the then/true case and the else/false case.

For example:

(TRUE)(True)(False) == True (FALSE)(True)(False) == False

Now if we define:

AND = lambda a: lambda b: (a)(b)(a) OR = lambda a: lambda b: (a)(a)(b) NOT = lambda a: lambda b: lambda c: (a)(c)(b)

we can do boolean logic with only reference to function application.

For example:

(AND)(TRUE)(FALSE) == (FALSE)

This is a little hard to verify in Python so we can use our if-then-else trick:

(AND)(TRUE)(FALSE)(True)(False) == False

Our definition of `TRUE` and `FALSE` is known as the **Church encoding** of the booleans.

We can also Church-encode a pair, or `cons`, and define `car` and `cdr` appropriately:

CONS = lambda a: lambda b: lambda c: (c)(a)(b) CAR = lambda a: (a)(TRUE) CDR = lambda a: (a)(FALSE)

If the definitions of `CAR` and `CDR` seem odd, note that the magic is really in `CONS`.

(CAR)((CONS)(1)(2)) == 1 (CDR)((CONS)(1)(2)) == 2

But this means `CONS` makes a nice way of deferring our `(True)(False)` trick to "unchurch" Church-encoded booleans into Python booleans:

UNCHURCH_BOOLEAN = (CONS)(True)(False)

Now we can say:

(UNCHURCH_BOOLEAN)((NOT)(TRUE)) == False (UNCHURCH_BOOLEAN)((OR)(TRUE)(FALSE)) == True

The natural numbers can also be Church-encoded:

ZERO = FALSE SUCC = lambda a: lambda b: lambda c: (b)((a)(b)(c))

We can then define:

ONE = (SUCC)(ZERO) TWO = (SUCC)(ONE) THREE = (SUCC)(TWO) FOUR = (SUCC)(THREE)

and so on. Here's a little Python function for "churching" numbers:

def church_number(n): return SUCC(church_number(n - 1)) if n else FALSE

We can define addition, multiplication and exponentiation as follows:

PLUS = lambda a: lambda b: lambda c: lambda d: (a)(c)((b)(c)(d)) MULT = lambda a: lambda b: lambda c: (b)((a)(c)) EXP = lambda a: lambda b: (b)(a)

Of course, what would be nice is if we had an easy way to unchurch our Church-encoded numbers so we could see if these work. Well, it turns out that's easy to do:

UNCHURCH_NUMBER = lambda a: (a)(lambda b: b + 1)(0)

So

(UNCHURCH_NUMBER)(ZERO) == 0 (UNCHURCH_NUMBER)(ONE) == 1 (UNCHURCH_NUMBER)(TWO) == 2

and so on.

(UNCHURCH_NUMBER)((PLUS)(THREE)(TWO)) == 5 (UNCHURCH_NUMBER)((MULT)(THREE)(TWO)) == 6 (UNCHURCH_NUMBER)((EXP)(THREE)(TWO)) == 9

Tweet

The original post was in the categories: python combinatory_python but I'm still in the process of migrating categories over.

The original post had **14 comments** I'm in the process of migrating over.