# Church Encoding in Python

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
```

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.