Encodings for numbers in lambda calculus

Darius J Chuck

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.

Notation

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 [].

Church numerals

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

Zero

Lambda calculus

0 = λ_.λx. x

LAST

0 = LL T

Properties

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.

Successor

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$ .

Predecessor

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.$

Zermelo-like numerals

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.

Zero

Identical to Church zero.

Analogy to Zermelo ordinals

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.

Successor

The successor function in this encoding is remarkably simple.

Lambda calculus

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

LAST

succ = L L AT ST

Analogy to Zermelo ordinals

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.

Predecessor

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.

Problem with unpacking

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 _.

Lynn numerals

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.

Zero

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.

Successor

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.

Predecessor

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!

No problem with unpacking

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.

Problem of incompatbility with Church encoding

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.

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.

Zero

Identical to Church zero.

Successor

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.

Predecessor

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.

No problem of incompatbility

Since zero in this encoding is the same as false in the Church encoding, it remains compatible. No need to redefine anything. Problem solved!

Summary

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?

Support TAO

If you like, you can support my work with a small donation.

Thank you!

— Darius J Chuck

Notation

Church numerals

Zero

Properties

Successor

Predecessor

Zermelo-like numerals

Zero

Analogy to Zermelo ordinals

Successor

Analogy to Zermelo ordinals

Predecessor

Problem with unpacking

Lynn numerals

Zero

Successor

Predecessor

No problem with unpacking

Problem of incompatbility with Church encoding

Zermelo-Lynn numerals

Zero

Successor

Predecessor

No problem of incompatbility

Summary

See also

Support TAO