<p>The other reason (than the one already stated) for <code>pred 0 = 0</code> are the (all too often unstated) <em>requirements</em> that</p>

<ol>
<li><code>pred</code> be a total function from <code>nat</code> to <code>nat</code></li>
<li><code>pred succ n = n</code> be true.</li>
<li><code>pred</code> be as close to injective as possible.</li>
<li><code>pred</code> be as close to a monotone decreasing function as possible.</li>
</ol>

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

CC BY-SA 3.0
2011-11-20T14:57:59.970Z
2011-11-20T14:57:59.970Z
Jacques Carette
<p>Here's the thirty second explanation for why subtraction "should be" saturating. First, suppose that we have $a, b, s \in \mathbb{N}$. </p>

<ol>
<li><p>The subtraction $a - b$, when it exists, is the solution $s$ to the equation $s + b = a$. </p></li>
<li><p>Truncated subtraction is the supremum of the set of solutions to the equation $s + b \leq a$. </p></li>
<li><p>That is, when $b &gt; 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. </p></li>
<li><p>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.</p></li>
<li><p>Predecessor is just subtracting 1, so it should be saturating too. </p></li>
</ol>

<p>I learned about this from Martin Escardo, who also recommended Lawvere's <a href="http://tac.mta.ca/tac/reprints/articles/1/tr1.pdf"><em>Metric spaces, generalized logic and closed categories</em></a> as a nice exposition of this and related ideas. </p>

<p>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 &gt; a$ when proving someting about $a - b$), and furthermore subtraction does not have good associativity or commutativity properties. </p>

<p>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. </p>

CC BY-SA 3.0
2011-11-22T05:54:30.493Z
2011-11-22T07:27:03.633Z
2011-11-22T07:27:03.633Z
Neel Krishnaswami
<p>In typed $\lambda$-calculus with sums the most natural type for the predecessor function would be (in Haskell parlance)</p>

<pre><code>pred :: Nat -&gt; Maybe Nat
</code></pre>

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

CC BY-SA 3.0
2011-11-22T18:07:14.157Z
Nitpicking: In Haskell, type names must be capitalized.
Tsuyoshi Ito
CC BY-SA 3.0
2011-11-22T22:23:13.880Z
@Tsuyoshi: Duly noted.
Andrej Bauer
CC BY-SA 3.0
2011-11-20T14:32:12.333Z
2011-11-22T22:22:54.723Z
2011-11-22T22:22:54.723Z
Andrej Bauer
<p>My question may be similar to: <a href="https://cstheory.stackexchange.com/questions/3772/why-naturals-instead-of-integers">Why naturals instead of integers?</a>, but it is more specific.</p>

<p>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.</p>

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

<p>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.</p>

<p>Thanks,</p>

<p>Charlie</p>

CC BY-SA 3.0
2011-11-20T13:38:19.973Z
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
CC BY-SA 3.0
2011-11-20T15:29:12.883Z
“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
<lo.logic><lambda-calculus>
Why does predecessor(zero) need to be zero in Church numerals?
Charles R
# Why does predecessor(zero) need to be zero in Church numerals?

(Asked by: username_0 on 2011-11-20)

My question may be similar to: [Why naturals instead of integers?](https://cstheory.stackexchange.com/questions/3772/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

**Tags:** lo.logic, lambda-calculus
> **Comments:**
> **username_1**: 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.  
> **username_2**: “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.  

---

## 3 answers

### Answer by username_3 on 2011-11-20. Score: 10

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 by username_4 on 2011-11-22. Score: 7

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*](http://tac.mta.ca/tac/reprints/articles/1/tr1.pdf) 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 by username_5 on 2011-11-20. Score: 6

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.

> **Comments:**
> **username_2**: Nitpicking: In Haskell, type names must be capitalized.  
> **username_5**: @Tsuyoshi: Duly noted.  

---

