Natural Numbers

Posted on 2014-05-01 by nbloomf

\(\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}\) \(\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}\) \(\newcommand{\a}{a}\) \(\newcommand{\b}{b}\) \(\newcommand{\c}{c}\) \(\newcommand{\p}{p}\) \(\newcommand{\q}{q}\) \(\newcommand{\r}{r}\) \(\newcommand{\s}{s}\) \(\newcommand{\x}{x}\) \(\newcommand{\y}{y}\) \(\newcommand{\z}{z}\) \(\newcommand{\bool}{\mathbb{B}}\) \(\newcommand{\btrue}{\mathsf{true}}\) \(\newcommand{\bfalse}{\mathsf{false}}\) \(\newcommand{\bnot}{\mathsf{not}}\) \(\newcommand{\band}{\mathbin{\mathsf{and}}}\) \(\newcommand{\bor}{\mathbin{\mathsf{or}}}\) \(\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}\) \(\newcommand{\beq}{\mathsf{eq}}\) \(\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}\) \(\newcommand{\id}{\mathsf{id}}\) \(\newcommand{\compose}{\mathsf{compose}}\) \(\newcommand{\const}{\mathsf{const}}\) \(\newcommand{\apply}{\mathsf{apply}}\) \(\newcommand{\flip}{\mathsf{flip}}\) \(\newcommand{\flipB}{\mathsf{flip2}}\) \(\newcommand{\flipC}{\mathsf{flip3}}\) \(\newcommand{\flipD}{\mathsf{flip4}}\) \(\newcommand{\flipE}{\mathsf{flip5}}\) \(\newcommand{\clone}{\mathsf{clone}}\) \(\newcommand{\cloneC}{\mathsf{clone3}}\) \(\newcommand{\composeAonB}{\mathsf{compose1on2}}\) \(\newcommand{\composeAonC}{\mathsf{compose1on3}}\) \(\newcommand{\composeAonD}{\mathsf{compose1on4}}\) \(\newcommand{\composeBonA}{\mathsf{compose2on1}}\) \(\newcommand{\composeBonB}{\mathsf{compose2on2}}\) \(\newcommand{\composeConA}{\mathsf{compose3on1}}\) \(\newcommand{\ptrue}{\mathsf{ptrue}}\) \(\newcommand{\pfalse}{\mathsf{pfalse}}\) \(\newcommand{\pnot}{\mathsf{pnot}}\) \(\newcommand{\pand}{\mathbin{\mathsf{pand}}}\) \(\newcommand{\por}{\mathbin{\mathsf{por}}}\) \(\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}\) \(\newcommand{\fst}{\mathsf{first}}\) \(\newcommand{\snd}{\mathsf{second}}\) \(\newcommand{\dup}{\mathsf{dup}}\) \(\newcommand{\tup}{\mathsf{tup}}\) \(\newcommand{\tSwap}{\mathsf{swap}_{\times}}\) \(\newcommand{\tPair}{\mathsf{pair}_{\times}}\) \(\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}\) \(\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}\) \(\newcommand{\tupL}{\mathsf{tupL}}\) \(\newcommand{\tupR}{\mathsf{tupR}}\) \(\newcommand{\uncurry}{\mathsf{uncurry}}\) \(\newcommand{\curry}{\mathsf{curry}}\) \(\newcommand{\lft}{\mathsf{left}}\) \(\newcommand{\rgt}{\mathsf{right}}\) \(\newcommand{\either}{\mathsf{either}}\) \(\newcommand{\uSwap}{\mathsf{swap}_{+}}\) \(\newcommand{\uPair}{\mathsf{pair}_{+}}\) \(\newcommand{\uAssocL}{\mathsf{assocL}_{+}}\) \(\newcommand{\uAssocR}{\mathsf{assocR}_{+}}\) \(\newcommand{\isLft}{\mathsf{isLeft}}\) \(\newcommand{\isRgt}{\mathsf{isRight}}\) \(\newcommand{\nats}{\mathbb{N}}\) \(\newcommand{\zero}{\mathsf{0}}\) \(\newcommand{\next}{\mathsf{next}}\) \(\newcommand{\unnext}{\mathsf{unnext}}\) \(\newcommand{\iszero}{\mathsf{isZero}}\) \(\newcommand{\prev}{\mathsf{prev}}\) \(\newcommand{\natrec}{\mathsf{natrec}}\) \(\newcommand{\simprec}{\mathsf{simprec}}\) \(\newcommand{\bailrec}{\mathsf{bailrec}}\) \(\newcommand{\mutrec}{\mathsf{mutrec}}\) \(\newcommand{\dnatrec}{\mathsf{dnatrec}}\) \(\newcommand{\normrec}{\mathsf{normrec}}\) \(\newcommand{\findsmallest}{\mathsf{findsmallest}}\) \(\newcommand{\mnormrec}{\mathsf{mnormrec}}\) \(\newcommand{\nequal}{\mathsf{eq}}\) \(\newcommand{\nplus}{\mathsf{plus}}\) \(\newcommand{\ntimes}{\mathsf{times}}\) \(\newcommand{\nleq}{\mathsf{leq}}\) \(\newcommand{\ngeq}{\mathsf{geq}}\) \(\newcommand{\nminus}{\mathsf{minus}}\) \(\newcommand{\nmax}{\mathsf{max}}\) \(\newcommand{\nmin}{\mathsf{min}}\) \(\newcommand{\ndivalg}{\mathsf{divalg}}\) \(\newcommand{\nquo}{\mathsf{quo}}\) \(\newcommand{\nrem}{\mathsf{rem}}\) \(\newcommand{\ndiv}{\mathsf{div}}\) \(\newcommand{\ngcd}{\mathsf{gcd}}\) \(\newcommand{\ncoprime}{\mathsf{coprime}}\) \(\newcommand{\nlcm}{\mathsf{lcm}}\) \(\newcommand{\nmindiv}{\mathsf{mindiv}}\) \(\newcommand{\nisprime}{\mathsf{isPrime}}\) \(\newcommand{\npower}{\mathsf{power}}\) \(\newcommand{\nchoose}{\mathsf{choose}}\) \(\newcommand{\dom}{\mathsf{dom}}\) \(\newcommand{\cod}{\mathsf{cod}}\) \(\newcommand{\lists}[1]{\mathsf{List}(#1)}\) \(\newcommand{\nil}{\mathsf{nil}}\) \(\newcommand{\cons}{\mathsf{cons}}\) \(\newcommand{\uncons}{\mathsf{uncons}}\) \(\newcommand{\isnil}{\mathsf{isNil}}\) \(\newcommand{\tail}{\mathsf{tail}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\foldr}{\mathsf{foldr}}\) \(\newcommand{\foldl}{\mathsf{foldl}}\) \(\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}\) \(\newcommand{\unfoldN}{\mathsf{unfoldN}}\) \(\newcommand{\dfoldr}{\mathsf{dfoldr}}\) \(\newcommand{\cfoldr}{\mathsf{cfoldr}}\) \(\newcommand{\bfoldr}{\mathsf{bfoldr}}\) \(\newcommand{\dbfoldr}{\mathsf{dbfoldr}}\) \(\newcommand{\lfoldr}{\mathsf{lfoldr}}\) \(\newcommand{\snoc}{\mathsf{snoc}}\) \(\newcommand{\revcat}{\mathsf{revcat}}\) \(\newcommand{\rev}{\mathsf{rev}}\) \(\newcommand{\last}{\mathsf{last}}\) \(\newcommand{\cat}{\mathsf{cat}}\) \(\newcommand{\addlength}{\mathsf{addlength}}\) \(\newcommand{\length}{\mathsf{length}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\at}{\mathsf{at}}\) \(\newcommand{\map}{\mathsf{map}}\) \(\newcommand{\range}{\mathsf{range}}\) \(\newcommand{\zip}{\mathsf{zip}}\) \(\newcommand{\zipPad}{\mathsf{zipPad}}\) \(\newcommand{\unzip}{\mathsf{unzip}}\) \(\newcommand{\prefix}{\mathsf{prefix}}\) \(\newcommand{\suffix}{\mathsf{suffix}}\) \(\newcommand{\lcp}{\mathsf{lcp}}\) \(\newcommand{\lcs}{\mathsf{lcs}}\) \(\newcommand{\all}{\mathsf{all}}\) \(\newcommand{\any}{\mathsf{any}}\) \(\newcommand{\tails}{\mathsf{tails}}\) \(\newcommand{\inits}{\mathsf{inits}}\) \(\newcommand{\filter}{\mathsf{filter}}\) \(\newcommand{\elt}{\mathsf{elt}}\) \(\newcommand{\addcount}{\mathsf{addcount}}\) \(\newcommand{\count}{\mathsf{count}}\) \(\newcommand{\repeat}{\mathsf{repeat}}\) \(\newcommand{\sublist}{\mathsf{sublist}}\) \(\newcommand{\infix}{\mathsf{infix}}\) \(\newcommand{\select}{\mathsf{select}}\) \(\newcommand{\unique}{\mathsf{unique}}\) \(\newcommand{\delete}{\mathsf{delete}}\) \(\newcommand{\dedupeL}{\mathsf{dedupeL}}\) \(\newcommand{\dedupeR}{\mathsf{dedupeR}}\) \(\newcommand{\common}{\mathsf{common}}\) \(\newcommand{\disjoint}{\mathsf{disjoint}}\) \(\newcommand{\sublists}{\mathsf{sublists}}\) \(\newcommand{\take}{\mathsf{take}}\) \(\newcommand{\drop}{\mathsf{drop}}\) \(\newcommand{\takeBut}{\mathsf{takeBut}}\) \(\newcommand{\dropBut}{\mathsf{dropBut}}\) \(\newcommand{\takeWhile}{\mathsf{takeWhile}}\) \(\newcommand{\dropWhile}{\mathsf{dropWhile}}\)

This page is part of a series on Arithmetic Made Difficult.

We all developed an intuitive understanding of the counting numbers back in kindergarten. But what exactly are they? Mathematics depends on having precise definitions, and we need one for the natural numbers.

Typically, the natural numbers are developed using the Peano axioms: these axioms assert the existence of a set \(N\) with an element 0 and a function \(S : N \rightarrow N\) which satisfy the following.

\(0 = S(n)\) does not have a solution \(n \in N\).
If \(S(n) = S(m)\), then \(n = m\).
If \(B\) is a set such that \(0 \in B\) and whenever \(n \in B\) we also have \(S(n) \in B\), then in fact \(N \subseteq B\).

There is another approach we can take, which as far as I know was introduced by William Lawvere. This approach characterizes the natural numbers explicitly as an initial object in an appropriate category. It turns out that thinking in this abstractly nonsensical fashion can be given a very concrete interpretation, essentially allowing us to derive executable programs and prove things about them.

Iterative Sets

The basic setup of the Peano axioms – the element 0 and the function \(S\) – form a kind of structure on \(N\), which we give a name.

A set \(A\) with a distinguished element \(e\) and a distinguished function \(\varphi : A \rightarrow A\) is called an iterative set.

We can think of an iterative set as a very primitive kind of algebra. There’s not much we can do with one, though, except construct a list of successive values: \[e, \quad \varphi(e), \quad \varphi(\varphi(e)), \quad \varphi(\varphi(\varphi(e))), \quad \ldots.\] Not all of these successive values have to be distinct. For instance we can define a set \(\bool = \{ \btrue, \bfalse \}\) and a function \(\bnot : \bool \rightarrow \bool\) by \(\bnot(\btrue) = \bfalse\) and \(\bnot(\bfalse) = \btrue\). Now \((\bool, \btrue, \bnot)\) is an iterative set, but the sequence of values generated by \(\bnot\) repeats: \[\begin{eqnarray*} \btrue & = & \btrue, \\ \bnot(\btrue) & = & \bfalse, \\ \bnot(\bnot(\btrue)) & = & \btrue, \\ \bnot(\bnot(\bnot(\btrue))) & = & \bfalse, \\ & \vdots & \end{eqnarray*}\]

As a kind of algebra, the iterative sets come with a corresponding class of structure-preserving maps. In this case, the only structure to be preserved is the distinguished element and the distinguished function.

Suppose \((A,e,\varphi)\) and \((B,f,\psi)\) are iterative sets. A mapping \(\theta : A \rightarrow B\) is called an iterative homomorphism if \(\theta(e) = f\) and \(\theta(\varphi(x)) = \psi(\theta(x))\) for all \(x \in A\).

That is, \(\theta\) is a homomorphism if it makes the following diagrams commute.

\[\require{AMScd} \begin{CD} 1 @= 1\\ @V{e}VV @VV{f}V \\ A @>>{\theta}> B \end{CD} \quad\quad\quad \begin{CD} A @>{\theta}>> B\\ @V{\varphi}VV @VV{\psi}V \\ A @>>{\theta}> B \end{CD}\]

It is straightforward to show that the identity function \(\id\) is always an iterative homomorphism and that the composite of two homomorphisms is a homomorphism. So the iterative sets form a category (if you’re into that).

Natural Numbers

As an axiom, we define the natural numbers to be a special iterative set.

There is a special inductive set \((\nats,\zero,\next)\) which has the following universal property: if \((A,e,\varphi)\) is an iterative set, then there is a unique iterative homomorphism \(\Theta : \nats \rightarrow A\). This unique function \(\Theta\) will be denoted \(\natrec(e)(\varphi)\).

At first this may seem like a strange definition. By repeatedly applying the \(\next\) function to \(\zero\), we get the successive values \[\zero, \quad \next(\zero), \quad \next(\next(\zero)), \quad \next(\next(\next(\zero))), \quad \ldots\] which (assuming they are all distinct!) resemble the Peano numbers. But what sets \(\nats\) apart from the other iterative sets is the special function \(\natrec\): given any other iterative set \(A\), there is exactly one iterative homomorphism from \(\nats\) to \(A\).

Applying this function to the sequence of elements above, we see that \(\natrec(e)(\varphi)(\zero) = e\) (of course), and then \[\natrec(e)(\varphi)(\next(\zero)) = \varphi(\natrec(e)(\varphi)(\zero)) = \varphi(e),\] \[\natrec(e)(\varphi)(\next(\next(\zero))) = \varphi(\natrec(e)(\varphi)(\next(\zero))) = \varphi(\varphi(e)),\] \[\natrec(e)(\varphi)(\next(\next(\next(\zero)))) = \varphi(\natrec(e)(\varphi)(\next(\next(\zero)))) = \varphi(\varphi(\varphi(e))),\] and so on.

The \(\natrec\) function captures the basic pattern of recursion on the natural numbers, as we will see. Importantly, it does so in a well-behaved way; reasoning about recursive functions defined using \(\natrec\) can be very easy.

We will eventually show that these natural numbers satisfy the more traditional Peano axioms, but we need a little more machinery first. In the meantime the following version of induction will come in handy.

(Induction Principle.) Suppose \(f : \nats \rightarrow A\) is a map and that \(B \subseteq A\) is a subset satisfying the following.

\(f(\zero) \in B\)
Whenever \(f(n) \in B\), we also have \(f(\next(n)) \in B\).

Then we have \(f(n) \in B\) for all natural numbers \(n\).

Define a subset \(T \subseteq \nats\) by \[T = \{n \in \nats \mid f(n) \in B \}.\] By hypothesis, we have \(\zero \in T\). Also, if \(n \in T\), then \(\next(n) \in T\); in particular, the restriction of \(\next\) to \(T\) is in fact a function \(T \rightarrow T\). That is, \((T,\zero,\next)\) is an iterative set. Let \(\Theta = \natrec(\zero)(\next)\) be the unique homomorphism \(\nats \rightarrow T\).

Now let \(\iota : T \rightarrow \nats\) denote the inclusion map; in fact \(\iota\) is an iterative homomorphism, since we have \(\iota(\zero) = \zero\) and \[\iota(\next(n)) = \next(n) = \next(\iota(n))\] for all \(n \in T\).

The composite map \(\iota \circ \Theta : \nats \rightarrow \nats\) is again an iterative homomorphism, and by uniqueness, in fact we have \(\iota \circ \Theta = \id\). If \(n\) is a natural number, we have \[n = \id(n) = \iota(\Theta(n)) = \Theta(n),\] and in particular, \(n \in T\). That is, if \(n\) is any natural number, we have \(f(n) \in B\).

The traditional induction principle follows as a corollary where \(A = \nats\) and \(\varphi\) is the inclusion map.

(Induction on \(f\).) Let \(f : A \rightarrow \nats\) be a map. Suppose \(B \subseteq A\) is a set satisfying the following.

If \(f(a) = \zero\), then \(a \in B\).
If we have \(n \in \nats\) such that if \(f(a) = n\), then \(a \in B\), then if \(f(a) = \next(n)\), then \(a \in B\).

Then we have \(B = A\).

Suppose \(B \subseteq A\) satisfies these properties, and define \(T \subseteq \nats\) by \[T = \{n \in \nats \mid \forall a \in A, \mathrm{if}\ f(a) = n\ \mathrm{then} a \in B \}.\] We will show that \(T = \nats\) by induction.

For the base case, suppose we have \(a \in A\) such that \(f(a) = \zero\). By condition (1) we have \(a \in B\); so \(\zero \in T\) as needed.

For the inductive step, suppose we have \(n \in T\). That is, if \(f(a) = n\), then \(a \in B\). Now let \(a \in A\), and suppose \(f(a) = \next(n)\). By condition (2), we have \(a \in B\); so we have \(\next(n) \in T\).

Thus by induction \(T = \nats\). Now if \(a \in A\), we have \(f(a) = n\) for some \(n \in \nats\), and thus \(a \in B\).

This result says that if we can map a set \(A\) to the natural numbers, we can recover a version of the induction principle. This induction doesn’t necessarily reflect any structure that may exist on \(A\), but at times it can be useful anyway. When using this theorem, we will say we are inducting “on \(f(a)\)”. The function \(f\) acts like a measurement of “size” in some sense; and if all the elements of \(A\) have “finite size” (whatever that means) we can induct. Whenever we see things like finite dimension, finitely generated, finite length, et cetera, odds are good the reason why is so we can invoke this induction principle.

But Why?

As we’ll see, the function \(\natrec\) essentially characterizes the natural numbers just like the Peano axioms do, albeit in a slightly goofy and hard-to-get-used-to way. So if \(\natrec\) and Peano are equivalent, why bother with the added abstraction? Well, if we define our arithmetic purely in terms of \(\natrec\), and then find a concrete representation of \(\natrec\) in software, then suddenly all of our proofs become executable. And by wrapping up recursion behind a small number of “recursion patterns”, those proofs can be easier to find and reason about.

But wait, there’s more! The “uniqueness” part of natural recursion is also handy. To be a little more explicit, it says the following.

Let \((A,e,\varphi)\) be an inductive set. Then \(\natrec(e)(\varphi)\) is the unique solution \(f : \nats \rightarrow A\) to the following system of functional equations for all \(k \in \nats\): \[\left\{\begin{array}{l} f(\zero) = e \\ f(\next(k)) = \varphi(f(k)) \end{array}\right.\]

This is a nice pre-packaged proof that two functions are equal. We can use it, for instance, to show that an obviously correct but slow program is equivalent to a fast but not obviously correct one.