nLab
recursion

Recursion

Idea

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 00 (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 FF an endofunctor, a morphism of the form F(X)XF(X) \to X determines a collection of constructors and the recursion principle is the statement that there is a (unique) morphism f:AXf : A \to X from the initial such structure F(A)AF(A) \to A. This ff is the corresponding recursively defined function.

Viewed from just a slightly different angle, this state of affairs is the induction principle.

Examples

Example

In the theory of Peano arithmetic, we define x+yx + y recursively in terms of the successor operation ss as follows:

  1. x+0=xx + 0 = x
  2. x+s(y)=s(x+y)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 general

Theorem

Let XX, YY, and ZZ be sets, and suppose \rightsquigarrow is a well-founded relation on XX. Let h:X×Y×𝒫(Z)Zh\colon X \times Y \times \mathcal{P}(Z) \to Z be a given function. Then, there is a unique function f:XZf\colon X \to Z satisfying

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

for all yy in YY, where

S={zZ:x.(xxz=f(x,y))}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:10\colon 1 \to \mathbb{N} and successor s:s\colon \mathbb{N} \to \mathbb{N}. For any morphisms f 0:YZf_0\colon Y \to Z and h:×Y×ZZh\colon \mathbb{N} \times Y \times Z \to Z, there is a unique morphism f:×YZf\colon \mathbb{N} \times Y \to Z such that

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

and

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

where x:×Yx\colon \mathbb{N} \times Y \to \mathbb{N} is the first projection and y:×YYy\colon \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:YAg_0\colon Y \to A, k:Y×AAk\colon Y \times A \to A, there is a unique morphism u:×YAu\colon \mathbb{N} \times Y \to A such that u(0×id Y)=g 0u \circ (0 \times \mathrm{id}_Y) = g_0 and u(s×id Y)=kuu \circ (s \times \mathrm{id}_Y) = k \circ u. We take A=×ZA = \mathbb{N} \times Z, g 0=0×f 0g_0 = 0 \times f_0, and k(y,n,z)=n,h(n,y,z)k(y, n, z) = \langle n, h(n, y, z) \rangle, where n:Y××Zn\colon Y \times \mathbb{N} \times Z \to \mathbb{N}, y:Y××ZYy\colon Y \times \mathbb{N} \times Z \to Y, and z:Y××ZZz\colon Y \times \mathbb{N} \times Z \to Z are the obvious projections. The ff we seek is then obtained as p 2up_2 \circ u, where p 2:×ZZp_2 : \mathbb{N} \times Z \to Z is the second projection.

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

computability

type I computabilitytype II computability
typical domainnatural numbers \mathbb{N}Baire space of infinite sequences 𝔹= \mathbb{B} = \mathbb{N}^{\mathbb{N}}
computable functionspartial recursive functioncomputable function (analysis)
type of computable mathematicsrecursive mathematicscomputable analysis, Type Two Theory of Effectivity
type of realizabilitynumber realizabilityfunction realizability
partial combinatory algebraKleene's first partial combinatory algebraKleene's second partial combinatory algebra

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