Idea
A definition is recursive when the object being defined is specified in terms of itself, often on smaller or simpler inputs. For functions this usually means that the value at an input is computed by reducing the problem to values at arguments that are earlier in a well-founded relation.
Recursion is central in computability theory, type theory, and functional programming. It is the basic mechanism for defining functions on inductive data, but unrestricted recursion may lead to non-termination. For this reason one often distinguishes total forms of recursion, such as structural or well-founded recursion, from general recursion, which may define only partial functions.
Definition
A recursive definition gives the value of a function by finitely many base cases together with clauses reducing more complex cases to simpler ones.
Mutual recursion is the variant in which several functions are defined simultaneously and may call one another.
Structural Recursion
In type theory, a function is structurally recursive when each recursive call is made on an immediate subterm of an inductive type. This is the standard way to define total functions on natural numbers, lists, trees, and syntax.
For example, recursion on the natural numbers is given by a base case at and a step reducing the value at to the value at . Proof assistants such as Agda usually accept such definitions because termination is evident from the decreasing structure.
Primitive Recursion
Primitive recursion is the classical numerical form of structural recursion. A function on is defined by a base value and a step function:
f(0, \vec{x}) &= g(\vec{x}) \\ f(n + 1, \vec{x}) &= h(n, f(n, \vec{x}), \vec{x}). \end{aligned}$$ Primitive recursive definitions always terminate. In [[computability theory]] they form an important subclass of the total computable functions. ## Well-Founded Recursion Structural recursion can be generalized from inductive structure to any [[Well-founded Relation|well-founded relation]]. A definition of $f(x)$ is well-founded recursive when recursive calls are only made at arguments $y$ with $y < x$. This is the recursion principle corresponding to [[Induction|well-founded induction]]. It is often used when the relevant notion of size is not literally given by the shape of the data. ## General Recursion General recursion drops the requirement that recursive calls be visibly decreasing. This is common in programming language semantics and in untyped or effectful programming, where recursive definitions are often understood via [[Fixed Point|fixed points]]. General recursion is expressive, but it may fail to terminate. In constructive settings one therefore often separates total recursion from partial or potentially divergent computation. ## In Computability Theory In classical recursion theory, recursive functions are studied extensionally as functions on the natural numbers. The basic operations are usually composition, primitive recursion, and minimization. Allowing minimization leads from primitive recursive functions to partial recursive functions, which capture the ordinary notion of computable numerical function. From this point of view, recursion is not merely a programming technique but one of the standard mathematical presentations of effective computation, alongside [[Turing Machine|Turing machines]] and other equivalent models. ## Relation to Induction Recursion and [[Induction]] are closely related. Recursion defines functions out of an inductive object, while induction proves propositions about its elements. In dependent type theory, recursion is the non-dependent special case of induction. ## Related Concepts - [[Induction]] - [[Inductive Type]] - [[Well-founded Relation]] - [[Fixed Point]] - [[Computability Theory]]