The traditional notion of recursion over the natural numbers is a way of defining a function out of by specifying the image of (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 an endofunctor, a morphism of the form determines a collection of constructors and the recursion principle is the statement that there is a (unique) morphism from the initial such structure . This 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 recursively in terms of the successor operation as follows:
The definition above is taken as axiomatic in Peano arithmetic. More generally, given a (parametrizable) natural numbers object , its universal property guarantees that there is a unique (!) map with the above properties.
Let , , and be sets, and suppose is a well-founded relation on . Let be a given function. Then, there is a unique function satisfying
for all in , where
By the principle of well-founded induction. (Details to be added.)
Let be a (parametrizable) natural numbers object in a category with finite products, with zero and successor . For any morphisms and , there is a unique morphism such that
and
where is the first projection and is the second projection.
Recall that the universal property for states that for data , , there is a unique morphism such that and . We take , , and , where , , and are the obvious projections. The we seek is then obtained as , where is the second projection.
Dually, there is a notion of corecursion on a coinductive structure.
Revision on August 12, 2013 at 10:21:20 by Urs Schreiber See the history of this page for a list of all contributions to it.