This post is part of the Lambda Calculus series.

Having now seen the building blocks of the Lambda Calculus, we must ask ourselves whether this is actually a useful system or if, as it may first appear, it is capable of nothing more than shuffling symbols around on a page. To begin to construct any useful algorithm using this system, we first need a way to represent the data that the algorithm requires. While it is certainly debatable, I would suggest the natural numbers are a sensible place to start. To achieve this, we will use the scheme of Church numerals.

This scheme is remarkably simple and starts by representing the number 0 as \( \lambda fx . x \). We then represent 1 as \( \lambda fx . fx \), 2 as \( \lambda fx . f ( fx ) \), 3 as \( \lambda fx . f ( f ( fx )) \), and so on. The number \( n \) is represented as a lambda function that takes two arguments, \( f \) and \( x \), and repeatedly applies \( f \) to \( x \) a total of \( n \) times! For convenience, I will write \( [n] \) as a shorthand for the Church numeral representing the number \( n \), so \( [0] = \lambda fx . x \) and so on.

You may notice that \( \beta \)-substitution doesn’t allow a lambda function to inspect its arguments at all. As a result, this idea of blurring the lines between functions and data is necessary to represent anything meaningfully within the Lambda Calculus.

Arithmetic With Church Numerals

If you have read the ‘What is Maths’ series, you will know that if we are armed with the ability to add 1 and to describe recursive definitions, we will be able to reconstruct both addition and multiplication. If you haven’t read that series, then fear not; we will go over the details we need here as well.

Before we start, we should think about how we want our algorithms for these arithmetic operations to look. I will claim that, in the example of adding by 1, we want to find some term \( S \) such that \( S [n] =_\beta [n + 1] \) for any natural number \( n \). Similarly, for addition, we want to find some term \( A \) such that \( A [n] [m] =_\beta [n + m] \) for any natural numbers \( n \) and \( m \).

Firstly, let’s think about how we can implement addition by one in the Lambda Calculus. As the only fundamental operation we can perform is substitution, we should think about what sort of substitutions we can make that might achieve this. If we replace \( x \) with \( fx \) in any Church numeral, we will have succeeded in adding one! This naturally results in thinking about some term like \( [n] f ( fx ) \)—this will be the Church numeral \( [n] \), but substituting \( f \) into \( f \) and \( fx \) into \( x \). This is clearly not in the form we want, but it’s a good start.

Next, to make this \( \beta \)-equivalent to a Church number, we have to wrap it in a lambda abstraction, so we need to instead think about \( \lambda fx . [n] f ( fx ) \). If we are concerned about \( f \) and \( x \) being the subject of lambda abstraction both at the top level of this term and hidden away in \( [n] \), which we should be, we can simply appeal to \( \alpha \)-equivalence. The final step is to pull out \( [n] \), allowing us to separate this into two terms, one we shall call \( S \) and \( [n] \). This ends up looking like \( ( \lambda afx . a f (fx) ) [n] \) and so we can write \( S = \lambda afx . a f (fx) \). In order to convince ourselves that this works, let’s look at an example:

\begin{align*} S [3] &= ( \lambda afx . a f (fx) ) [3] \\ &= ( \lambda afx . a f (fx) ) ( \lambda fx . f ( f ( fx ))) \\ &=_\alpha ( \lambda afx . a f (fx) ) ( \lambda g y . g ( g ( g y ))) \\ &\to_\beta \lambda fx . ( \lambda g y . g ( g ( g y ))) f (fx) \\ &\to_\beta \lambda fx . ( \lambda y . f ( f ( f y ))) (fx) \\ &\to_\beta \lambda fx . f ( f ( f ( fx ))) \\ &= [4] \end{align*}

Now that we have addition by one, we are well on our way to general addition. By noticing that \( n + m = n + 1 + 1 + \cdots + 1 \) where there are \( m \) ones, we develop our plan. Recalling our earlier observation that the Church numeral \( [m] \) is also a function that applies some other function \( m \) times, we can see that \( [m] S [n] \) produces a result by applying \( S \) (addition by one) to \( [n] \) a total of \( m \) times. We can again pull out the numbers \( [m] \) and \( [n] \), suggesting the term \( A = \lambda ab . a S b \) is a suitable candidate for addition. For clarity and conciseness, I am reusing \( S \) from above; if we want, we can instead write this out in full, \( A = \lambda ab . a ( \lambda a^\prime fx . a^\prime f ( fx )) b \). Now, let’s check our work with an example:

\begin{align*} A [3] [2] &= ( \lambda ab . a S b ) [3] [2] \\ &\to_\beta ( \lambda b . [3] S b ) [2] \\ &\to_\beta [3] S [2] \\ &= ( \lambda fx . f ( f ( fx ))) S [2] \\ &\to_\beta ( \lambda x . S ( S ( S x ))) [2] \\ &\to_\beta S ( S ( S [2] )) \\ &=_\beta S ( S [3] ) \\ &=_\beta S [4] \\ &=_\beta [5] \end{align*}

We can reuse this same idea again for multiplication. By noting that \( n \times m = n + \cdots + n + 0 \) where \( n \) is repeated \( m \) times, we see that \( [n \times m] \) can be obtained by applying addition by \( n \) to \( [0] \) a total of \( m \) times. This gives us the term \( M = \lambda ab . a X [0] \) where \( X \) is some term that needs to be filled in and should represent addition by \( n \) (assuming that \( b = [n] \)). While we could revisit our work on addition to try and devise some new term that achieves this, it would be easier to simply reuse \( A \)—it turns out that \( X = Ab \) does exactly what we need!

This may be surprising if we think of \( A \) as a two-argument function. However, we can equally think of \( A \) a single-argument function that produces a new single-argument function. With this second interpretation, we can recover the two-argument behaviour, apply \( A \) to the first argument and the resulting function to the second argument. In fact, if you return to the definition of the Lambda Calculus, you will see that there are no ‘true’ two-argument functions; syntax such as \( \lambda ab . \cdots \) is really just a shorthand for \( ( \lambda a . ( \lambda b . \cdots )) \)!

This means that we can neatly say \( M = \lambda ab. a (Ab) [0] \); although it is only neat because of all the shorthands we’re using! I will also leave the example of this multiplication for you to test! It is worth saying that our descriptions of addition and multiplication are not necessarily unique. For example, an alternative (and much more concise) way to implement multiplication in the Lambda Calculus is \( M = \lambda abfx . a (bf) x \). Similarly, we could have implemented addition as \( A = \lambda abfx . a f ( b f x ) \).

While being able to perform basic arithmetic is an essential part of describing algorithms, we will be very limited without some way to ‘inspect’ numbers and make decisions based on our calculations. In the next part, we will explore how we can do just that.