2022-09-29

One of the first things one learns about when studying lambda calculus are the Church numerals. This is the Church encoding for natural numbers.

It is a pretty cleverly designed unary number encoding with simple non-recursive arithmetic functions. However, because of its originality, it may be difficult to understand, creating an obstacle at the beginning of one’s journey into the world of lambda calculus.

Fortunately neither students nor teachers of lambda calculus have to go through these difficulties: there are more straightforward encodings for numbers in lambda calculus.

Here I will show a few such unary encodings and how they compare to the original. Specifically, we will look at the fundamentals: the definitions of zero as well as the successor, and predecessor functions.

When using the lambda calculus notation, I mark arguments which are
ignored with the underscore `_`

.

When using the pseudo lambda calculus notation, I wrap the “pseudo”
parts in square brackets `[]`

.

Originally formulated by Alonzo Church, the creator of lambda calculus.

Lambda calculus

`0 = λ_.λx. x`

`0 = LL T`

This is a very convenient definition of `0`

, as it is
identical to the definition of the Church
boolean `false`

and to a defintion of the
`nil`

value, which is a handy terminator of lists.
It is also the function used to select the second component of a Church
pair or the tail of a list.

Since the Church boolean `true`

is defined symmetrically
as:

Lambda calculus

`0 = λx.λ_. x`

LAST

`true = LL ST`

an expression which reduces to a boolean (a predicate) can behave like an if-expression:

Pseudo lambda calculus

`([predicate] [consequent] [alternative])`

If the `predicate`

reduces to `true`

, then the
result is the `consequent`

, whereas if it reduces to
`false`

, the result is the `alternative`

.

The successor function in the Church encoding is pretty simple.

Lambda calculus

`succ = λn. λf.λx. f (n f x)`

LAST

`succ = L LL AST AASST ST T`

By invoking `n f x`

we do
$n$
applications of `f`

to `x`

. By calling
`f`

on the result of that, we add one more application,
bringing the total to
$n+1$.

This function is notoriously difficult to explain and comprehend.

Supposedly Church himself almost gave up on lambda calculus, struggling to come up with a working definition of the predecessor. Finally his student Stephen Kleene cracked the problem while under the influence of nitrous oxide at his dentist.

Since then, a few simpler (but still rather involved) formulations have been devised. Perhaps the most concise one is this:

Lambda calculus

`pred = λn. λf.λx. n (λg.λh. h (g f)) (λ_.x) (λu.u)`

LAST

`pred = L LL AAASST LL AT AST SSST LST LT`

I will leave that without explanation, as that can be found elsewhere (e.g. on Wikipedia or in The predecessor function for Church Numerals in the Lambda Calculus by Greg Johnson).

What we will do instead is examine alternative encodings for natural numbers which have much simpler definitions of both the successor and the predecessor.

Before that, I’ll just state in mathematical terms what the predecessor function is supposed to do:

$\operatorname{pred}(n) = \begin{cases} 0 & \operatorname{if\ }n=0, \\ n-1 & \operatorname{otherwise.}\end{cases}$

Note that since we’re dealing with natural numbers, we define
`0`

to be the predecessor of `0`

itself.

To get rid of subtraction and constants, we can state the same definition as:

$\operatorname{pred}(n) = \begin{cases} n & \operatorname{if\ }n=0, \\ m & \operatorname{otherwise.}\end{cases}$

Where

$S(m) = n.$

This is an original encoding, discovered during my research which led to the creation of LAST. Turns out their definition is analogous to that of Zermelo ordinals, hence the name.

The Zermelo definition of `0`

is the empty set, i.e.

$0 = \{\}$

The Church zero is the same function as `nil`

, which can
be used to represent an empty list.

The analogy is then between the empty set and the empty list.

The successor function in this encoding is remarkably simple.

Lambda calculus

`succ = λn. λf. (f n)`

LAST

`succ = L L AT ST`

The Zermelo definition of the successor function is:

$S(a) = \{a\}$

i.e. the successor of $a$ is a singleton set which contains $a$.

To see the analogy between `succ`

and
$S$,
let’s recall the definition of the Church pair constructor function:

Lambda calculus

`makePair = λx.λy. λf. (f x y)`

and observe that a Church pair is analogous to a set of 2 elements.

If we get rid of the second element of the pair, we get a constructor function for singleton sets:

Lambda calculus

`makeSingleton = λx. λf. (f x)`

LAST

`makeSingleton = L L AT ST`

This is identical to `succ`

and so the analogy with the
Zermelo
$S$
holds.

Lambda calculus

`pred = λn. (n λm.λ_.m n)`

LAST

`pred = L AAT LL ST T`

This is dramatically simpler than the Church predecessor.

Since by definition, a non-zero number contains its predecessor, all we need to do is unpack it.

There is one small wrinkle.

Our unpacking function here is:

Lambda calculus

`λm.λ_.m`

LAST

`LL ST`

which is identical to `true`

in the Church encoding. The
same function is used to select the first element of a Church pair or
the head of a list.

Even though in our encoding non-zero numbers are singletons rather than pairs, using the identity function would not be correct, since we have to account for the zero case.

If
$n$
is `0`

then our unpacking function will be ignored and the
final
$n$
(= `0`

) will be returned.

Pseudo lambda calculus

`pred 0 = (λn. (n λm.λ_.m n)) [0] = [0] λm.λ_.m [0] = [0]`

If however $n$ is non-zero then our unpacking function will receive the unpacked predecessor $m$, but also the final $n$ which we must ignore before returning $m$ as the result. For example:

Pseudo lambda calculus

```
pred 3 = (λn. (n λm.λ_.m n)) [3]
= [3] λm.λ_.m [3]
= (λf. (f [2])) λm.λ_.m [3]
= (λm.λ_.m [2]) [3]
= (λ_.[2]) [3]
= [2]
```

This is because in the zero case, $n$ is a function of 2 arguments whereas in the non-zero case $n$ is a function of 1 argument.

The problem is general: when working with Zermelo-like numerals we
have to always take care of providing the proper unpacking function. For
example when defining the `isZero`

predicate:

Pseudo lambda calculus

`isZero = λn. (n λm.λ_.[false] [true])`

we also need to remember to include the dummy argument
`_`

.

Introduced by Ben Lynn, hence the name. Described as the Scott encoding for Peano numbers.

I found this encoding after having discovered the Zermelo-like numerals and it gave me an idea on how to modify them to achieve a simpler predecessor function and simplify unpacking, resulting in the formulation of Zermelo-Lynn numerals.

Lambda calculus

`0 = λx.λ_. x`

LAST

`0 = LL ST`

The encoding effectively defines zero as identical to
`true`

in the Church encoding.

This is a problem, because it may lead to confusion and makes this less convenient than other encodings which leverage the versatile Church false.

Lambda calculus

`succ = λn. λ_.λf. (f n)`

LAST

`succ = L LL AT SST`

The important difference between the Zermelo-like successor and this is the addition
of the dummy argument `_`

.

In exchange for that we get a simpler predecessor and streamlined unpacking.

This is the crucial ingredient that, incorporated into Zermelo-like numerals, led me to Zermelo-Lynn numerals which, I think, provide the best of both worlds.

Compared to the Church predecessor this one is beautifully simple.

Lambda calculus

`pred = λn. (n n λm.m)`

LAST

`pred = L AAT T LT`

If $n$ is zero, we return it, otherwise we simply unpack and return the predecessor. That’s it!

The unpacking function here is simply the identity function.

Lambda calculus

`λm.m`

LAST

`LT`

This is thanks to the fact that a non-zero number in this encoding is, like zero, a function of 2 arguments, which ignores its first argument (whereas zero in this encoding ignores its second argument).

So if `n`

is zero, the unpacking function is ignored,
returning `n`

itself (= `0`

).

If `n`

is non-zero then `n`

is ignored,
returning the unpacked predecessor.

This encoding would be perfect, if it weren’t for the fact that it
defines zero as identical to the Church `true`

. This would
make sense if we also redefined the booleans and all the functions of
the Church encoding which use them.

But the value of this effort would be questionable because, in Ben Lynn’s own words:

[L]ong before computers were commonplace, Alonzo Church devised this particular encoding of booleans, which subsequently became standard. We bow down to this convention to avoid confusion.

Fortunately, there is an easier way: enter Zermelo-Lynn numerals.

The Zermelo-Lynn numerals can be viewed as a variant of the Lynn numerals where the order of the two cases of the Scott encoding is reversed.

Alternatively, taking the angle from which I arrived at their definition, they can be viewed as a variant of the Zermelo-like numerals, where all numbers are 2-argument functions, with one dummy argument, for convenient unpacking.

Lambda calculus

`succ = λn. λf.λ_. (f n)`

LAST

`succ = L LL AST SST`

which S-optimizes to:

LAST

`succ = L LL SAT ST`

The definition is the same as for the Lynn successor, except here the
dummy argument `_`

goes second rather than first.

Lambda calculus

`pred = λn. (n λm.m n)`

LAST

`pred = L AAT LT T`

The definition is the same as for the Lynn predecessor, except here
the unpacking function goes first and the case for zero (`n`

)
goes second – they are swapped.

Since zero in this encoding is the same as `false`

in the
Church encoding, it remains compatible. No need to redefine anything.
Problem solved!

We have discussed three unary encodings for natural numbers in lambda calculus which provide alternatives to the original Church encoding with much simpler definitions of the fundamental successor and predecessor functions.

If you ask me, the simplest, most beautiful, and most convenient of them all are the Zermelo-Lynn numerals.

Particularly striking is the simplicity of its predecessor function:

Lambda calculus

`pred = λn. (n λm.m n)`

LAST

`pred = L AAT LT T`

Compared to the infamous Church predecessor:

Lambda calculus

`pred = λn. λf.λx. n (λg.λh. h (g f)) (λ_.x) (λu.u)`

LAST

`pred = L LL AAASST LL AT AST SSST LST LT`

If you were to learn or teach lambda calculus, which would you prefer?

- SK numerals by John Tromp – yet another interesting unary encoding for numbers in lambda calculus based on the SKI combinator calculus