1.9 The natural numbers
The rules we have introduced so far do not allow us to construct any infinite types. The simplest infinite type we can think of (and one which is of course also extremely useful) is the type of natural numbers. The elements of are constructed using and the successor operation . When denoting natural numbers, we adopt the usual decimal notation , , , ….
The essential property of the natural numbers is that we can define functions by recursion and perform proofs by induction — where now the words “recursion” and “induction” have a more familiar meaning. To construct a non-dependent function out of the natural numbers by recursion, it is enough to provide a starting point and a “next step” function . This gives rise to with the defining equations
We say that is defined by primitive recursion.
As an example, we look at how to define a function on natural numbers which doubles its argument. In this case we have . We first need to supply the value of , which is easy: we put . Next, to compute the value of for a natural number , we first compute the value of and then perform the successor operation twice. This is captured by the recurrence . Note that the second argument of stands for the result of the recursive call .
Defining by primitive recursion in this way, therefore, we obtain the defining equations:
This indeed has the correct computational behavior: for example, we have
We can define multi-variable functions by primitive recursion as well, by currying and allowing to be a function type. For example, we define addition with and the following “starting point” and “next step” data:
We thus obtain satisfying the definitional equalities
As usual, we write as . The reader is invited to verify that .
As in previous cases, we can package the principle of primitive recursion into a recursor:
with the defining equations
Using we can present and as follows:
Of course, all functions definable only using the primitive recursion principle will be computable. (The presence of higher function types — that is, functions with other functions as arguments — does, however, mean we can define more than the usual primitive recursive functions; see e.g. http://planetmath.org/node/87563Exercise 1.10.) This is appropriate in constructive mathematics; in §3.4 (http://planetmath.org/34classicalvsintuitionisticlogic),§3.8 (http://planetmath.org/38theaxiomofchoice) we will see how to augment type theory so that we can define more general mathematical functions.
We now follow the same approach as for other types, generalizing primitive recursion to dependent functions to obtain an induction principle. Thus, assume as given a family , an element , and a function ; then we can construct with the defining equations:
We can also package this into a single function
with the defining equations
Here we finally see the connection to the classical notion of proof by induction. Recall that in type theory we represent propositions by types, and proving a proposition by inhabiting the corresponding type. In particular, a property of natural numbers is represented by a family of types . From this point of view, the above induction principle says that if we can prove , and if for any we can prove assuming , then we have for all . This is, of course, exactly the usual principle of proof by induction on natural numbers.
As an example, consider how we might represent an explicit proof that is associative. (We will not actually write out proofs in this style, but it serves as a useful example for understanding how induction is represented formally in type theory.) To derive
it is sufficient to supply
To derive , recall that , and hence . Hence we can just set
For , recall that the definition of gives , and hence
Thus, the output type of is equivalently . But its input (the “inductive hypothesis”) yields , so it suffices to invoke the fact that if two natural numbers are equal, then so are their successors. (We will prove this obvious fact in Lemma 1 (http://planetmath.org/22functionsarefunctors#Thmlem1), using the induction principle of identity types.) We call this latter fact , so we can define
Putting these together with , we obtain a proof of associativity.
|Title||1.9 The natural numbers|