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

Question

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

Answer 1

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.

Answer 2

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.

Answer 3

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.