The traditional notion of recursion over the natural numbers $\mathbb{N}$ is a way of defining a function out of $\mathbb{N}$ by specifying the image of $0$ (the “initial value”) along with a way to obtain each successive value from the previous one(s).
The study of functions on the natural numbers which can or cannot be defined using only recursion – recursive functions – is the topic of computability theory and has deep connections with the formal logic of Peano arithmetic.
More generally, recursion is a way of defining a function on any mathematical object which is “defined inductively” (in a way analogous to how the natural numbers are characterized by zero and successor). In place of the “initial value” and “successor step”, a general definition by recursion consists of giving one “clause” for each “constructor” of the inductively defined object.
Recursion is formalized in type theory by the notion of inductive type (and the corresponding elimination rule) and, equivalently, in category theory by the notion of initial algebra of an endofunctor. For $F$ an endofunctor, a morphism of the form $F(X) \to X$ determines a collection of constructors and the recursion principle is the statement that there is a (unique) morphism $f : A \to X$ from the initial such structure $F(A) \to A$. This $f$ is the corresponding recursively defined function.
Viewed from just a slightly different angle, this state of affairs is the induction principle on non-dependent types.
In the theory of Peano arithmetic, we define $x + y$ recursively in terms of the successor operation $s$ as follows:
$x + 0 = x$
$x + s(y) = s(x + y)$
The definition above is taken as an axiom in Peano arithmetic.
More generally, given a (parametrizable) natural numbers object $\mathbb{N}$, its universal property guarantees that there is a unique (!) map $\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ with the above properties.
Let $X$, $Y$, and $Z$ be sets, and suppose $\rightsquigarrow$ is a well-founded relation on $X$. Let $h\colon X \times Y \times \mathcal{P}(Z) \to Z$ be a given function. Then, there is a unique function $f\colon X \to Z$ satisfying
for all $y$ in $Y$, where
By the principle of well-founded induction. (Details to be added.)
Let $\mathbb{N}$ be a (parametrizable) natural numbers object in a category with finite products, with zero $0\colon 1 \to \mathbb{N}$ and successor $s\colon \mathbb{N} \to \mathbb{N}$. For any morphisms $f_0\colon Y \to Z$ and $h\colon \mathbb{N} \times Y \times Z \to Z$, there is a unique morphism $f\colon \mathbb{N} \times Y \to Z$ such that
and
where $x\colon \mathbb{N} \times Y \to \mathbb{N}$ is the first projection and $y\colon \mathbb{N} \times Y \to Y$ is the second projection.
Recall that the universal property for $\mathbb{N}$ states that for data $g_0\colon Y \to A$, $k\colon Y \times A \to A$, there is a unique morphism $u\colon \mathbb{N} \times Y \to A$ such that $u \circ (0 \times \mathrm{id}_Y) = g_0$ and $u \circ (s \times \mathrm{id}_Y) = k \circ u$. We take $A = \mathbb{N} \times Z$, $g_0 = 0 \times f_0$, and $k(y, n, z) = \langle n, h(n, y, z) \rangle$, where $n\colon Y \times \mathbb{N} \times Z \to \mathbb{N}$, $y\colon Y \times \mathbb{N} \times Z \to Y$, and $z\colon Y \times \mathbb{N} \times Z \to Z$ are the obvious projections. The $f$ we seek is then obtained as $p_2 \circ u$, where $p_2 : \mathbb{N} \times Z \to Z$ is the second projection.
Dually, there is a notion of corecursion on a coinductive structure.
type I computability | type II computability | |
---|---|---|
typical domain | natural numbers $\mathbb{N}$ | Baire space of infinite sequences $\mathbb{B} = \mathbb{N}^{\mathbb{N}}$ |
computable functions | partial recursive function | computable function (analysis) |
type of computable mathematics | recursive mathematics | computable analysis, Type Two Theory of Effectivity |
type of realizability | number realizability | function realizability |
partial combinatory algebra | Kleene's first partial combinatory algebra | Kleene's second partial combinatory algebra |
See also:
Discussion in type theory:
and in view of homotopy type theory:
Last revised on December 31, 2022 at 11:14:02. See the history of this page for a list of all contributions to it.