The recursor for natural numbers
Before we define recursors, let's first introduce the idea of an inductive type. We'll do this by examining how lean defines natural numbers.
inductive Nat where
| zero : Nat
| succ (n : Nat) : Nat
The idea here being that we can construct natural numbers by either using the constructor zero to get 0, or by applying the constructor succ to an existing natural number to get its successor. For example, we can construct 3 as follows:
def three : Nat := Nat.succ (Nat.succ (Nat.succ Nat.zero))
We can equivalently express this definition using the type formation and term introduction rules:
While this explanation for inductive types usually gives most people I think enough intuition to understand the basic notions of how to use them to construct something like natural numbers, I think it kind of misses the deeper idea of what an inductive type and by extension a recursor really is. To attempt to explain this we'll take a look into some categorical semantics behind inductive types.
While at first this definition seems a bit needlessly abstract, it actually captures what the inductive type of natural numbers really is. The basic thing to recognize is that the two morphisms (just think of them as functions for now) in reality don't have anything to do with natural numbers directly. Instead, they act as a kind of blueprint for how we can use the properties or constraints of natural numbers to make anything. Here on a high level we can describe the two functions / constructors as follows:
- \(0 : 1 \to \mathbb {N}\) - The represents the abstract idea of having some starting point or base case. Within natural numbers this is represented by
0, but in reality it denotes an abstract concept of having a starting point.
- \(s : \mathbb {N} \to \mathbb {N}\) - This represents the abstract idea of being able to build upon existing things to create new things. Within natural numbers this is represented by the successor function.
Now this might quite fairly still seem a bit confusing and abstract. How can we use properties to make anything?. To describe this more formally lets constrain ourselves to the category of sets, \(\mathbf {Set}\). If you are unfamiliar with category theory it's sufficient to think of this as just a collection of all kinds of sets and functions between them.
So in plain English what this is saying is that given any set \(X\) where we have some starting point \(x \in X\) and some way of building upon existing elements of \(X\) (the function \(f : X \to X\)), we can use the properties of natural numbers to create a unique function \(u : \mathbb {N} \to X\) that maps natural numbers to elements of \(X\) in a way that respects our starting point and building function. A natural next question to have might be
But what does it mean to respect the starting point and building function?
Here I'd fast say intuitively you can just imagine construct which has some notion of a start and some way of building upon existing things. For example let's imagine the following graph:
\[
a \to b \to c \to d \to e \to \ldots
\]
Clearly here with have:
- Starting point: Our start here is the node \(a\).
- Building function: Our building function i.e. successor mechanism here is just following the arrows to the next node.
So our two morphisms then are:
Creating a minimal replica of this in Lean we could do something like:
inductive Node where
| start : Node -- this will play the role of “a”
| next : Node → Node
def succNode (v : Node) : Node :=
Node. next v
def natToNode : ℕ → Node
| 0 => Node.start
| n + 1 => succNode (natToNode n)
So we can see our function \(u : \mathbb {N} \to X\) here is represented by natToNode. Where the function maps 0 to a and each successor natural number to the next node along the arrow.
Something you might notice here is that if our natToNode function is replaced by just an identity, i.e.:
def natToNat : ℕ → ℕ
| 0 => 0
| n + 1 => n + 1
Then we get just the natural numbers themselves as defined by their properties. This is precisely what's expressed by the earlier commutative diagram we say. The two arrows:
\[
1 \xrightarrow {0} \mathbb {N}
\quad \text { and } \quad \mathbb {N} \xrightarrow {s} \mathbb {N}
\]
Are just the natural numbers defined by their properties. So in a sense the natural numbers are the most basic instantiation of their own properties. So now a fair thing to wonder is:
So what does this have to do with recursers?
Well the key insight here is that our functions natToNat and natToNode both are our recursers for the natural numbers. A recursor is just a function that allows us to define functions out of an inductive type by specifying how to handle each constructor of the inductive type. So equivalently we can express our recursor for natural numbers as:
def recNat {C : Type} (z : C) (s : C → C) : ℕ → C
| 0 => z
| n + 1 => s (recNat z s n)
If we examine the actual type signature generated by #check Nat.rec we have:
«Nat».rec.{u}
{motive : ℕ → Sort u}
(zero : motive «Nat».zero)
(succ : (n : ℕ)
→ motive n
→ motive n.succ)
(t : ℕ) : motive t
In our examples above we can see that the motive is just the type we are mapping to (either \(\mathbb {N}\) or \(X\)), the zero is our starting point (either 0 or a) and the succ is our building function (either the successor function or following the arrows). So using the recursor we can rewrite our earlier natToNat and natToNode functions as:
def natToNat : ℕ → ℕ :=
Nat.rec
0 -- | 0 => 0
(fun n => n + 1) -- | n + 1 => n + 1
def natToNode : ℕ → Node :=
Nat.rec
Node.start -- | 0 => Node.start
(fun n => succNode n) -- | n + 1 => succNode (natToNode n)