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.

A (Very) Brief Introduction to Lambda Calculus

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

  1. Defining anonymous functions.
  2. 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:

  1. The only objects of lambda calculus are functions.
  2. Lambda calculus has no notion of assignment to variables.
  3. 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.