recursion

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). There is a rich theory regarding the functions which can or cannot be defined using only recursion: this is computability theory and has deep connections with the 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*.

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 axiomatic 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

$f (x', y) = h (x', y, S)$

for all $y$ in $Y$, where

$S = \{ z \in Z : \exists x . \, ( x \rightsquigarrow x' \wedge z = f (x, y) ) \}$

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

$f(0, -) = f_0$

and

$f(s(x), y) = h(s(x), y, f(x, y))$

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 |

Revised on March 1, 2014 05:15:17
by Urs Schreiber
(82.113.121.15)