One area of math that I’ve always been enamored with is the proof of numbers. The simplicity of the starting assumptions exudes a certain elegance. More startling is how much structure can be created from such simple initial states. Not so different from Conway’s game of Life or the board game go, both of which have simple rues yet produce voluminous complexity. The set theoretic approach to proving the natural numbers struck this chord with me. As a quick review, in this approach you start with the assumption that nothing exists. From here you define a set that contains nothing and call this set . You then define another set that contains the set that contains nothing and call this set . Continuing you define another set that is the union of the set that contains nothing and the set that contains the set that contains nothing and call this . From here it is easy to see that this is an inductive process where you can assume that exists and create a new set that is the union of and a set that contains , which is .

The Church Numerals work in a similar fashion except that the starting assumption is different. This yields a very different procedure for defining the natural numbers, but the overall encoding and inductive process is similar. Instead of sets, Church Numerals use lambda terms for counting. The starting assumption is that lambda abstraction is valid. From here you define a lambda term that takes two arguments f and x and returns x.

These numerals are encoded by an n-fold function composition. Since functions in R are first-class, it is easy to define them.

C0 <- function(f) function(x) x
C1 <- function(f) function(x) f(x)
C2 <- function(f) function(x) f(f(x))
C3 <- function(f) function(x) f(f(f(x)))

Performing operations on these numbers requires yet more functions. For example let’s define a function to increment a number and also define addition.

SUCC <- function(n) function(f) function(x) f(n(f)(x))
PLUS <- function(m) function(n) m(SUCC)(n)

Now it is possible to perform addition, say as

> PLUS(C2)(C3)
function(f) function(x) f(n(f)(x))
<environment: 0x29d0be8>

Easy, right? Okay so the tricky part is knowing whether this value is correct! It’s particularly difficult since n hides part of the chain of function composition. I scratched my head for a while until it dawned on me that these are functions. So a simple way to verify the calculation is to write a function that maps the Church numerals to the more traditional natural numbers. This function just needs to have the same property as the Church numerals: namely that function composition yields addition, or

TO_NAT <- function(x) x + 1

Now we can pass this function along with the identity for addition (i.e. ) to any Church numeral to get the corresponding natural number.

> C3(TO_NAT)(0)
[1] 3
> PLUS(C2)(C3)(TO_NAT)(0)
[1] 5

Continuing with this process it is possible to define the other arithmetic operations. What I like about this approach is how much easier it is to visualize and understand the behavior of the Church numerals. This in turn shows how foundational theories such as the lambda calculus can provide the basis for mathematics itself. In a separate post I will provide an example of the Church booleans as well.