This post explores Church Encoding, a method of representing natural numbers as lambda calculus terms.

**Assumed Knowledge:**

This post assumes that you're already familiar with a few concepts. You may still enjoy the post if you're not familiar with these ideas, but if you start to feel lost, these might be good topics to brush up on before continuing.

- I assume you can read Python code.
- I assume that you're comfortable with the idea of functions that return other functions as results.
- I assume you know what the Natural Numbers are.

### A (Very) Brief Introduction to Lambda Calculus

Lambda calculus is a theoretical model for computing in which the only allowed operations are:

- Defining anonymous functions.
- Applying functions to arguments.

There are many excellent resources online that describe lambda calculus and explain why it's important in the history and theory of computer science. For the purposes of this post, the important features of the lambda calculus are:

- The only objects of lambda calculus are functions.
- Lambda calculus has no notion of assignment to variables.
- The only way to introduce a new name in lambda calculus is as a parameter to a function.

Despite these limitations, lambda calculus turns out to be a surprisingly powerful model of computing. It's so powerful, in fact, that we have reason to believe that lambda calculus can express every computable function!

If this is your first time hearing about lambda calculus, that last sentence probably raised a few
questions. How can lambda calculus express every computable function when it only operates on
functions? What about functions defined on integers like "add one" or "double"? Are they not
computable? What does it even **mean** to "compute" using only functions?

It would take much more than a blog post to answer all of these questions completely. The remainder of this post will attempt to answer just one part of one of those questions: How can lambda calculus define functions that compute on natural numbers, using only functions?

### Encoding Numbers as Functions

In the previous section, I said that we can define **every computable function** in lambda calculus,
even though the only objects in lambda calculus are functions that accept functions as inputs and
return new functions as outputs. This might seem like a strange assertion when almost all of the
computable functions we care about (e.g. "add" or "multiply") are defined over sets like the
integers or the natural numbers. How can we define these functions in lambda calculus?

The first step toward defining lambda calculus functions that compute on natural numbers is to
define a **mapping** that associates every natural number N with a unique lambda calculus function,
which we call the "encoding" of N. Given such an mapping, we can build lambda calculus functions
that "compute on natural numbers" by accepting encoded numbers as inputs and producing encoded
numbers as outputs. For example, a lambda calculus definition of "add one" would take the
**encoding** of the number `N`

and return the **encoding** of the number `N + 1`

.

What encoding can we use to map natural numbers to functions that use only operations that are allowed in lambda calculus?

Well, in a world where we only have functions, we know at least the following:

`encode(N)`

will be a function.- The input to
`encode(N)`

will be a function. - The output of
`encode(N)`

will be a function.

In other words, we know our encoding operation will have to look something like this:

encode(0) == lambda f: lambda x: ??? encode(1) == lambda f: lambda x: ??? ... encode(N) == lambda f: lambda x: ???

What options do we have for filling in the question marks? Well, the only variables we have in scope
are `f`

and `x`

, and the only thing we can do with functions is apply them to arguments, so our
options are limited to expressions composed of repeated applications of `f`

and `x`

, e.g. `f(x)`

,
`f(f(x))`

, `f(f)(x)`

.

The trick to building a useful encoding from these tools is to notice that we can use the **number
of repeated applications of f** to encode the natural number N. So,

`encode(1)`

applies `f`

to `x`

one time, `encode(2)`

applies `f`

to `x`

two times, `encode(3)`

applies `f`

three times, and so on.encode(0) == lambda f: lambda x: x encode(1) == lambda f: lambda x: f(x) encode(2) == lambda f: lambda x: f(f(x)) encode(3) == lambda f: lambda x: f(f(f(x))) ...

This encoding of the natural numbers as lambda expressions is called the Church Encoding, after its inventor Alonzo Church, who also invented lambda calculus. The functions produced by Church Encoding are often referred to as "Church numerals".

We can write a Python function that converts an integer into a Church numeral using the
`eval`

function:

def church(N): """Church-encode the natural number N. """ signature = "lambda f: lambda x:" return_val = "f(" * N + "x" + ")" * N return eval(signature + return_val)

### Testing Our Church Encoding

Let's confirm that our church-encoded numerals work as expected:

`church(N)`

should produce a function that, when applied to a function `f`

, returns a function that
will feed its input through `f`

`N`

times.

If we call `church(3)`

on "increment by one", we should get back "increment by three":

>>> church(3)(lambda x: x + 1)(2) 5

`church(4)`

called on "double" should give us back "double four times", i.e. "multiply by 16":

>>> church(4)(lambda x: x * 2)(3) 48

Note that `church(N)`

doesn't know about or depend in any way on numbers. We got "add three" and
"multiply by 16" in the examples above because we applied our church numerals to functions that
operated on integers, but we can apply our numerals to any function that can applied iteratively to
its own output.

For example, if we call `church(2)`

on a function that gets the first element of a sequence, we end
up with "get the first element of the first element of a sequence":

>>> church(2)(lambda x: x[0])(['foo', 'bar']) 'f'

### Decoding Numerals

We can convert an encoded numeral back into an integer by applying the numeral to "increment by one" and then calling the result on zero.

def unchurch(f): """Convert a Church Numeral to a Python integer. """ return f(lambda x: x + 1)(0)

For any integer N, `unchurch(church(N))`

should give us back `N`

:

>>> unchurch(church(3)) 3 >>> unchurch(church(10)) 10

### Arithmetic

Now that we have a suitable representation of numbers as lambda expressions, we can turn our attention to implementing arithmetic on Church-encoded values.

#### Increment

The simplest operation we can implement on an Church-encoded integer is "increment by one". Here's one w

def increment(M): """Add one to M. """ return lambda f: lambda x: f(M(f)(x))

The key observation here is that `M(f)`

is a function that calls `f`

some number of times on `x`

,
and we need to produce a function that calls `f`

one time more than `M`

. We can implement that
function by applying `M(f)`

to `x`

and then feeding the result into `f`

one final time.

>>> unchurch(increment(church(3))) 4

#### Addition

Addition is implemented similarly to `increment`

.

def add(M, N): """Add two church numerals. """ return lambda f: lambda x: M(f)(N(f)(x))

To understand why the above definition works, recall that `M(f)(x)`

evaluates to:

f(f(... m times ...f(x)))

Similarly `N(f)(x)`

evaluates to:

f(f(... n times ...f(x)))

If we apply `M(f)`

to the result of `N(f)(x)`

, then we get:

f(f(... m times ...f(f(... n times... f(x)))))

Which is just:

f(f(... (m + n) times ...f(x)))

Which is exactly what we want `add(M, N)`

to produce!

unchurch(add(church(3), church(4))) 7 >>> unchurch(add(church(10), church(5))) 15

#### Multiplication

The definition of multiplication is even simpler than the definition of addition:

def multiply(M, N): """Multiply two church numerals. """ return lambda f: M(N(f))

To see why this works, notice that `N(f)`

is a function which, when applied to an input `x`

, will
produce:

f(f(... n times ...f(x)))`

If we apply `M`

to `N(f)`

, we get a function that applies `N(f)`

, `m`

times. Since `N(f)`

itself invokes `f`

`n`

times, we end up with a total of
`m * n`

applications of `f`

, which is precisely what we want for `multiply(M, N)`

.

>>> unchurch(multiply(church(2), church(3))) 6 >>> unchurch(multiply(church(3), church(5))) 15

#### Aside: Function Composition

If you're familiar with functional programming, you might notice a common structure in our
definitions of `add`

and `multiply`

. The innermost expression of both functions involved "chained"
application of a pair of functions.

In the implementation of `add`

, we chained `M(f)`

and `N(f)`

on the input `x`

:

M(f)(N(f)(x))

In the implementation of `multiply`

, we chained `M`

and `N`

on the input `f`

:

M(N(f))

Both of these expressions have the general form:

function1(function2(input))

This pattern of feeding a single input through two or more functions is common enough in functional
programming (and more generally in mathematics) that it has a special name: **function
composition**.

If we allow ourselves to cheat the lambda calculus rules a bit and make use of a `compose`

helper
function, the common structure of `add`

and `multiply`

becomes clearer:

def compose(f, g): return lambda x: f(g(x)) def add(M, N): return lambda f: compose(M(f), N(f)) def multiply(M, N): return lambda f: compose(M, N)(f)

When written this way, we can see that:

- To add two Church Numerals, you
**apply**each numeral to an input and then**compose**the results. - To multiply two Church Numerals, you
**compose**the numerals, and then**apply**the result to an input.

Of course, we don't actually need `compose`

as a named function. We can define our own anonymous
`compose`

"inline" to stay closer to the spirit of lambda calculus:

def add(M, N): # |------------- compose() -------------| return lambda f: (lambda g: lambda h: lambda x: g(h(x)))(M(f))(N(f)) def multiply(M, N): # |------------- compose() -------------| return lambda f: (lambda g: lambda h: lambda x: g(h(x)))(M)(N)(f)

These compose-based definitions still produce the expected results:

>>> unchurch(add(church(2), church(3))) 5 >>> unchurch(multiply(church(2), church(3))) 6

#### Exponentiation

The last definition I want to show in this post is exponentiation. We often think of exponentiation as being "more complex" than addition or multiplication, but the definition of exponentiation ends up being the simplest of any of the operators we've seen:

def exp(M, N): """Raise `M` to the power of `N`. """ return N(M)

The first time I saw this definition it blew my mind. Exponentiation on church numerals is just (flipped) function application!

To see why this works, we can start by expanding `N(M)`

.

Assuming `N == church(n)`

, we have:

exp(M, N) == N(M) == lambda f: M(M(... n times ...M(f)))

That still looks a pretty complicated, so let's see what this looks like in the special case where
`N`

is `church(2)`

:

exp(M, church(2)) == church(2)(M) == lambda f: M(M(f))

Wait a second, that looks familiar... `exp(M, church(2))`

expands to the same expression as
`multiply(M, M)`

!

multiply(M, N) == lambda f: M(N(f)) multiply(M, M) == lambda f: M(M(f)) == exp(M, church(2))

This shows that our definition of `exp`

preserves the expected property that `M ** 2 == M * M`

.

A bit less obviously, the expansion of `exp(M, church(3))`

can be written as follows:

exp(M, church(3)) == church(3)(M) == lambda f: M( M(M(f)) ) == lambda f: M( (lambda g: M(M(g)))(f) ) == lambda f: M( exp(M, church(2))(f) ) == multiply(M, exp(M, church(2)))

Which shows us (as expected) that `M ** 3 == M * (M ** 2)`

under our encoding.

We can modify this expansion slightly to show that `M ** (N + 1)`

expands to `M * (M ** N)`

:

exp(M, church(n + 1)) == church(n + 1)(M) == lambda f: M( ... n + 1 times ... M(f) ) == lambda f: M( M( ... n times ... M(f)) ) == lambda f: M( (lambda g: M(... n times ... M(g)))(f) ) == lambda f: M( exp(M, church(n)) )

From here it's not too hard to give an inductive proof that our encoding of exponentiation works for all cases.

### Review

In this post:

- We learned how Church Encoding associates every natural number
`n`

with a lambda calculus function that applies an input function`n`

times. - We learned how to define addition, multiplication, and exponentiation on Church numerals.
- We saw how the natural definitions of addition, multiplication and exponentiation are related to mathematical relationships between iteration, function composition, and function application.

All of this just barely scratches the surface of the rich history and theory of lambda calculus. If you're interested in learning more, there are many excellent resources on the internet where you can continue reading.. One resource that I particularly enjoy is the Lambda Calculus entry in the Stanford Encyclopedia of Philosophy, which includes links references for further reading as well as links to related articles in other areas of computing, mathematics, and philosophy.