# Why does predecessor(zero) need to be zero in Church numerals?

My question may be similar to: Why naturals instead of integers?, but it is more specific.

I am trying to learn lambda calculus. All the books make a big deal about how it was necessary that predecessor(zero) == zero and it was very tricky to get it right.

Why was that necessary? Can someone point me to some literature, or, better yet, give me a 30 sec explanation?

The only thing I can figure out is that this resulted in the naturals being closed under subtraction, but at a cost of having subtraction being a non one-to-one mapping from the natural numbers to themselves.

Thanks,

Charlie

• I think the answer is that this is the only natural definition for predecessor. It must be defined to be some natural number, but any other number seems ridiculous. – Dave Clarke Nov 20 '11 at 13:38
• “All the books make a big deal about how it was necessary that predecessor(zero) == zero and it was very tricky to get it right.” Is that true? I thought that it is trivial to define predecessor(zero) as any term you want (even a term which is not a Church numeral), and it is defined as zero just because it is slightly more natural than other choices. – Tsuyoshi Ito Nov 20 '11 at 15:29

## 3 Answers

The other reason (than the one already stated) for pred 0 = 0 are the (all too often unstated) requirements that

1. pred be a total function from nat to nat
2. pred succ n = n be true.
3. pred be as close to injective as possible.
4. pred be as close to a monotone decreasing function as possible.

It is that last requirement which really 'seals the deal' in forcing pred 0 = 0, since that is the choice which minimizes the distance to not being monotone decreasing.

Here's the thirty second explanation for why subtraction "should be" saturating. First, suppose that we have $a, b, s \in \mathbb{N}$.

1. The subtraction $a - b$, when it exists, is the solution $s$ to the equation $s + b = a$.

2. Truncated subtraction is the supremum of the set of solutions to the equation $s + b \leq a$.

3. That is, when $b > a$, no solutions $s + b = a$ exist, and the supremum of an empty set of natural numbers is 0. Otherwise the supremum will just be the subtraction.

4. So saturating subtraction is left adjoint to addition (i.e., $a - b \leq s \iff a \leq s + b$), and is hence a natural definition.

5. Predecessor is just subtracting 1, so it should be saturating too.

I learned about this from Martin Escardo, who also recommended Lawvere's Metric spaces, generalized logic and closed categories as a nice exposition of this and related ideas.

I should add that this adjunction is nice when doing interactive theorem proving. Proofs involving subtraction typically require case distinctions (i.e., you need to case on whether $b > a$ when proving someting about $a - b$), and furthermore subtraction does not have good associativity or commutativity properties.

In contrast, addition on the natural numbers behaves much better, and you can often use this adjunction to massage a proof obligation into a form which is easier to work with.

In typed $\lambda$-calculus with sums the most natural type for the predecessor function would be (in Haskell parlance)

pred :: Nat -> Maybe Nat


so that it can return Nothing when applied to 0 and Just n when applied to the successor of n. In untyped $\lambda$-calculus we could just ignore the types, but would still have to invent some way of encoding members of the type Maybe Nat, which would just complicate matters. It is easier to "fudge it" and define predecessor so that it maps numerals to numerals.

• Nitpicking: In Haskell, type names must be capitalized. – Tsuyoshi Ito Nov 22 '11 at 18:07
• @Tsuyoshi: Duly noted. – Andrej Bauer Nov 22 '11 at 22:23