Encoding natural numbers (part 1)

The classic inductive definition of natural numbers is well known: zero is a natural number, and the successor of a natural number is a natural number. In a language that supports inductive types, it can be written somewhat like this:

data Nat :: * where
  Zero :: Nat
  Succ :: Nat -> Nat
  
zero :: Nat
zero = Zero

one :: Nat
one = Succ Zero

two :: Nat
two = Succ (Succ Zero)

add :: Nat -> Nat -> Nat
add n Zero     = n
add n (Succ k) = Succ (add n k)

mul :: Nat -> Nat -> Nat
mul n Zero     = Zero
mul n (Succ k) = add m (mul n k)

pred :: Nat -> Nat
pred Zero     = Zero
pred (Succ k) = k

minus :: Nat -> Nat -> Nat
minus Zero     m        = Zero
minus n        Zero     = n
minus (Succ k) (Succ l) = minus k l

The simplest way to encode such numbers in the untyped lambda calculus is Church encoding, which seems to have no direct connection to the intuitive inductive type:

\begin{align*} 0 &= \lambda s z. z\\ 1 &= \lambda s z. sz\\ 2 &= \lambda s z. s(sz)\\ &\ldots\\ n &= \lambda s z. s^nz\\ \end{align*}

Here, exponent notation is used as syntactic sugar for the following definition:

\begin{align*} F^0(X) &= X\\ F^N(X) &= F^{N-1}(F(X)) \end{align*}

Despite the strange appearance of these terms, we can find an analogy: z in the lambda terms represents zero, while a number of s terms preceding it represent incrementing that zero several times. To make the analogy stronger still, let us introduce a succ function:

succ = \lambda n s z.s (n s z)

Indeed, using this term produces the expected behaviour:

\begin{align*} succ \; n &= (\lambda \color{red}n \color{black} s z.s (\color{red}n \color{black} s z)) \color{blue} (\lambda s z. s^n z) \color{black} = \\ &= (\lambda s z.s (\color{green} (\lambda \color{red} s \color{green} z. \color{red} s \color{green} ^n z) \color{blue} s \color{black} z)) = \\ &= (\lambda s z.s (\color{green} (\lambda \color{red} z \color{green}. s^n \color{red} z \color{green}) \color{blue} z \color{black})) = \\ &= (\lambda s z.s (s^n z)) = (\lambda s z.s^{n+1} z) \end{align*}

The simplest arithmetic operations are also available to us; they can be checked in exactly the same way as the succ function above:

\begin{align*} add &= \lambda m n. m \; succ \; n\\ mul &= \lambda m n. m \; add \; n\\ pow &= \lambda m n. m \; mul \; n \end{align*}

These functions reveal an important property of Church-encoded natural numbers. Applying the term representing the $n$ th natural number to terms f and x causes f to be applied to x exactly $n$ times:

n f x = (\lambda s z.s^n z) f x = f^n x

Subtraction and division are somewhat more difficult and use primitive recursion. To build them, we will need several auxiliary constructions. First, let us introduce two-element pairs. The inductive definition of a pair looks like this:

data Pair :: * -> * -> * where
  MkPair :: a -> b -> Pair a b
  
fst :: Pair a b -> a
fst (Pair x y) = x

snd :: Pair a b -> b
snd (Pair x y) = y

Once again, however, we must encode them using the lambda calculus:

pair = \lambda a b c.c a b

Indeed, any pair of elements can be written this way, because $pair X Y = \lambda c. c X Y$ . Moreover, we have two projections that return the first and second elements of the pair:

\begin{align*} fst &= \lambda p. p \; K \\ snd &= \lambda p. p \; K* \end{align*}

Here, $K$ and $K*$ are the combinators $\lambda x y.x$ and $\lambda x y. y$ , respectively. Indeed:

\begin{align*} fst (pair X Y) &= (\lambda p.p \; K) \; ((\lambda a b c.c a b) X Y) = \\ &= (\lambda p.p \; K) \; (\lambda c.c X Y) = (\lambda c.c X Y) K = \\ &= K X Y = (\lambda x y.x) X Y = (\lambda y.X) Y = X \end{align*}

How can we use this construction to obtain the preceding number? Let us define a pair whose first argument is some number and whose second argument is its successor. It is easy to construct:

pair \; n \; (succ \; n)

In particular, the first several pairs will be as follows, assuming that zero's predecessor is zero:

\begin{aligned} pair \; 0 \; 0\\ pair \; 0 \; 1\\ pair \; 1 \; 2\\ \ldots \end{aligned}

Instead of writing out every pair, can we simply invent a term that produces the next pair from the previous one? Easily!

sp = \lambda p. pair \; (snd \; p) (snd \; (succ \; p))

The first element of the new pair is the second element of the previous pair, and the second is the next number. Applying this function to the pair $(pair \; 0 \; 0)$ exactly n times gives us a pair whose second element is n and whose first element is n - 1. That is precisely what we need. Putting everything together gives us the predecessor function for natural numbers:

pred \; n = \lambda n.fst \; (n \; sp \; (pair \; 0 \; 0))

The same reasoning gives us subtraction:

minus = \lambda n m. m \; pred \; n

An important observation here is that pred takes $O(n)$ time, while minus takes no less than $O(n^2)$ ! This is an obvious problem with Church encoding for natural numbers.

Integer division can also be obtained by recalling its recursive expression in terms of subtraction:

\left[ \frac{n}{m} \right] = \begin{cases} 1 + \left[ \frac{n - m}{m} \right] & n \ge m \\ 0 & n < m \end{cases}

To write this expression, we need one more data type: Boolean, which will express the condition according to which we either return zero or follow the recursive branch. The classic definition of Boolean is trivial: it is a type inhabited by two concrete values.

data Bool :: * where
  True  :: Bool
  False :: Bool
  
ifThenElse :: Bool -> a -> a -> a
ifThenElse True  x y = x
ifThenElse False x y = y

Its representation in the untyped lambda calculus is not particularly complicated either:

\begin{align*} true &= \lambda t f.t \\ false &= \lambda t f.f \end{align*}

The if operator for this encoding is entirely trivial:

if = \lambda c x y.c x y

We can verify this directly:

\begin{align*} if \; true \; X \; Y &= (\lambda c x y.c x y) \; true \; X \; Y = \\ &= (\lambda x y.true \; x \; y) \; X \; Y = \\ &= (\lambda y.true \; X \; y) \; Y = true \; X \; Y = \\ &= (\lambda t f.t) \; X \; Y = (\lambda f.X) \; Y = \\ &= X\\ if \; false \; X \; Y &= (\lambda c x y.c x y) \; false \; X \; Y = \\ &= (\lambda x y.false \; x \; y) \; X \; Y = \\ &= (\lambda y.false \; X \; y) \; Y = false \; X \; Y = \\ &= (\lambda t f.f) \; X \; Y = (\lambda f.f) \; Y = \\ &= Y \end{align*}

To obtain our division formula, we must also work out how to compare two numbers. The simplest method is to subtract one from the other and compare the result with zero. We already know how to subtract, but comparison with zero is a new point of contact between two worlds: natural numbers and Boolean values. Nevertheless, the comparison is easy to implement. Observe that zero looks exactly like false, while a non-zero number applies some function to zero n times. This allows us to write an iszero function by analogy with if:

iszero = \lambda n.n \; (\lambda x.false) \; true

We can now write the recursive form of division:

div = \lambda n m. if \; (iszero \; (minus \; m \; (add \; n \; 1))) \; 0 \; (add \; 1 \; (div \; (minus \; n \; m) \; m))

Excellent! With one exception: we do not yet know how to work with recursive terms. But that is easy to fix. First, let us abstract over the occurrence of div in our term:

div = (\lambda \color{red} d \color{black} n m. if \; (iszero \; (minus \; m \; (add \; n \; 1))) \; 0 \; (add \; 1 \; (\color{red} d \color{black} \; (minus \; n \; m) \; m))) \; \color{red} div \color{black}

Our term now has the form $X = F \; X$ . In other words, div is a fixed point of the term:

\lambda d n m. if \; (iszero \; (minus \; m \; (add \; n \; 1))) \; 0 \; (add \; 1 \; (d \; (minus \; n \; m) \; m))

According to the fixed-point combinator theorem, every term has such a point, which can be found simply by applying a fixed-point combinator to the term:

Y = \lambda f.(\lambda x.f (xx))(\lambda x.f (xx))

The final non-recursive expression for division is therefore:

div = Y (\lambda d n m. if \; (iszero \; (minus \; m \; (add \; n \; 1))) \; 0 \; (add \; 1 \; (d \; (minus \; n \; m) \; m)))

Let us summarise. We have seen simple and intuitive definitions of data types such as natural numbers, pairs, and Boolean values. We have also defined a set of functions for working with each of them. The next step was the seemingly magical appearance of lambda terms that reproduce the behaviour of these constructions. Combining them with primitive recursion and expressing recursive terms through the Y combinator gave us the same set of functions. The question we will try to answer next time is this: is there an algorithm that translates intuitive inductive constructions into lambda terms?