nLab recursion (Rev #2, changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

Recursion

Idea
Examples
Recursion theorem
- In classical mathematics
- For a natural numbers object
Related concepts

Idea

To understand recursion, one must first understand recursion.

— An old joke

Joke as it may be, the quote above is very nearly the truth. The missing ingredient are conditions to guarantee that the process terminates; formally, what we need are base cases and a well-founded relation on the domain on which we are recursing.

Frequently the domain of interest is the natural numbers, or more generally an inductive structure. In the former case there is a rich theory regarding the functions which can or cannot be recursively defined: this is computability theory and has deep connections with the logic of Peano arithmetic.

Examples

Example. 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.

Recursion theorem

In classical mathematics

Theorem. Let $X$ , $Y$ , and $Z$ be sets, and suppose $\rightsquigarrow$ is a well-founded relation on $X$ . Let $h : X \times Y \times \mathcal{P}(Z) \to Z$ be a given function. Then, there is a unique function $f : X \to Z$ satisfying

Theorem

Let $X$ , $Y$ , and $Z$ be sets, and suppose $\rightsquigarrow$ is a well-founded relation on $X$ . Let $h : X \times Y \times \mathcal{P}(Z) \to Z$ be a given function. Then, there is a unique function $f : 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) ) \}

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

Proof

By the principle of well-founded induction. (Details to be added.)

~~for all $y$ in $Y$ , where~~
~~$S = \{ z \in Z : \exists x . \, ( x \rightsquigarrow x' \wedge z = f (x, y) ) \}$~~
Proof. By the principle of well-founded induction. (Details to be added.)

For a natural numbers object

Theorem. Let $\mathbb{N}$ be a (parametrizable) natural numbers object in a category with finite products, with zero $0 : 1 \to \mathbb{N}$ and successor $s : \mathbb{N} \to \mathbb{N}$ . For any morphisms $f_0 : Y \to Z$ and $h : \mathbb{N} \times Y \times Z \to Z$ , there is a unique morphism $f : \mathbb{N} \times Y \to Z$ such that

Theorem

Let $\mathbb{N}$ be a (parametrizable) natural numbers object in a category with finite products, with zero $0 : 1 \to \mathbb{N}$ and successor $s : \mathbb{N} \to \mathbb{N}$ . For any morphisms $f_0 : Y \to Z$ and $h : \mathbb{N} \times Y \times Z \to Z$ , there is a unique morphism $f : \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 : \mathbb{N} \times Y \to \mathbb{N}$ is the first projection and $y : \mathbb{N} \times Y \to Y$ is the second projection.

~~$f(0, -) = f_0$~~

Proof

Recall that the universal property for $\mathbb{N}$ states that for data $g_0 : Y \to A$ , $k : Y \times A \to A$ , there is a unique morphism $u : \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 : Y \times \mathbb{N} \times Z \to \mathbb{N}$ , $y : Y \times \mathbb{N} \times Z \to Y$ , and $z : 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. $\blacksquare$

~~and~~
~~$f(s(x), y) = h(s(x), y, f(x, y))$~~
~~where $x : \mathbb{N} \times Y \to \mathbb{N}$ is the first projection and $y : \mathbb{N} \times Y \to Y$ is the second projection.~~
Proof. Recall that the universal property for $\mathbb{N}$ states that for data $g_0 : Y \to A$ , $k : Y \times A \to A$ , there is a unique morphism $u : \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 : Y \times \mathbb{N} \times Z \to \mathbb{N}$ , $y : Y \times \mathbb{N} \times Z \to Y$ , and $z : 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. $\blacksquare$

Related concepts

Dually, there is a notion of corecursion on a coinductive structure.

Revision on August 26, 2011 at 15:10:55 by Urs Schreiber See the history of this page for a list of all contributions to it.