In computer science, corecursion is a type of operation that is dual to (structural) recursion. Whereas recursion consumes a data structure by first handling the topmost layer before descending into its inner parts, corecursion produces a data structure by first defining the topmost layer before defining its inner parts. Corecursion is a particularly important in total languages, as it allows encoding potentially non-terminating computations in a context where every function must terminate. It is supported by theorem provers Agda and Rocq.
Both corecursion and recursion can be thought of as operating on trees, which include data structures like lists and streams as special cases. Since recursion must terminate, it only works on trees that are well-founded, i.e. not infinitely deep, which are called data or initial data types; on the other hand, corecursion produces codata or final data types, which includes infinitely deep trees. Codata cannot be represented in memory directly, so is often implemented using self-referential data structures or lazy evaluation.
In total programming languages, the natural numbers may be defined as follows (using Haskell syntax):
This states that every natural number is either zero or the successor of an existing natural number. For example, the number one is represented as <code>Succ Zero</code>, two as <code>Succ (Succ Zero)</code>, three as <code>Succ (Succ (Succ Zero))</code> and so on.
If we interpret the above declaration in an inductive way, then all natural numbers are generated like this, and we get our familiar set of natural numbers. Importantly, we can do recursion on this set: for example, we can use it to make a list that repeats a value <code>n</code> times:
Note that the use of <code>recursive n</code> is crucialâÂÂwe could not have written <code>recursive (Succ n)</code>, because that is the function we are trying to define, and therefore it would loop forever. More specifically, the input must get smallerâÂÂor rather deeper, if seen as a data structureâÂÂeach time we recurse.
The declaration may also be interpreted in a coinductive way, which may be denoted as:
<code>CoNat</code> has all the natural numbers that <code>Nat</code> has automatically. But because codata can be infinitely deep, it has an extra term <code>Succ (Succ (Succ (Succ â¦)))</code> that continues on indefinitelyâÂÂoften denoted âÂÂ. This is unique to the conatural numbers, so it can only be constructed using corecursion:
While recursion requires that the input of the recursive call must get smaller each time, corecursion requires that the output of the recursive call must get larger each time. This is why we must write <code>Succ infinity</code>; just <code>infinity = infinity</code> would be disallowed as it loops forever.
To illustrate the duality between recursion and corecursion, we can encapsulate them in two functions, <code>rec</code> and <code>corec</code>. These functions' existence, together with the regular two constructors of <code>Nat</code> and <code>CoNat</code>, uniquely identify their respective types, and therefore allow rewriting all forms of recursion and corecursion in terms of them.
Conceptually, <code>CoNat</code> can be thought of as a state machine, where <code>c</code> is a type encapsulating the "current state". The function <code>c -> Maybe c</code> is a state transition function that either results in termination with <code>Zero</code> or continuation with <code>Succ</code>. We can rewrite the examples above using the functions:
A more complex example of codata is that of binary trees, where each node is either a leaf node, holding some data, or is a branch node that has exactly two children:
This example has many more infinitely deep terms that can only be constructed by corecursion. For example, it can be infinitely deep only on the left-hand side, or on both sides, or alternating left and right:
Again, corecursion on binary trees has a more general form based on a "state machine"-like constructor:
In a dependently-typed setting, codata can be encoded using M-types, which are dual to W-types. Given a type A and an A-indexed family of types B, one can form the M-type , representing the type of trees whose nodes are labelled with elements of A and who child nodes are indexed by the set B(a). In pseudocode, M-types (and their corecursion principle) may be defined as:As an example, the natural and conatural numbers may be constructed as W- and M-types of the same function:M-types can be proven to exist in many elementary topoi, and their existence follows from the existence of W-types.
The above section showed that there is an intimate link between natural and conatural numbers and <code>Maybe c</code>, and similarly between binary trees and <code>Either a (c, c)</code>. This link is made precise by showing that <code>Nat</code> is in bijection with <code>Maybe Nat</code>, and <code>CoNat</code> with <code>Maybe CoNat</code>; explicitly, this bjiection associates <code>Zero</code> with <code>Nothing</code> and <code>Succ n</code> with <code>Just n</code>. In other words, <code>Nat</code> and <code>CoNat</code> are fixed points (up to isomorphism) of the map .
The difference between data and codata is that data is the least such fixed point, while codata is the greatest. In this way, recursion can be summarized as the statement that "every element of the type was generated only by the given constructors (<code>Zero</code> and <code>Succ</code> in the case of <code>Nat</code>/<code>CoNat</code>)", while corecursion states that "every value that can be analysed using the constructors as cases exists".
From a category-theoretic perspective, <code>CoNat</code> can be precisely defined as the final coalgebra of the endofunctor. Unfolding this definition, we have that:
<code>Maybe c</code> can be replaced with any other functor in the above description to obtain the definition of any other coinductive type.
Not all functors have final coalgebras. For example, Cantor's theorem tells us that no set can be in bijection with its powerset, and therefore the powerset functor <code>a -> Bool</code> has no final coalgebra. However, in the case of polynomial functors or quotient polynomial functors, final coalgebras always exist; polynomial functors are functors that can be expressed in the form for a type ñ and ñ-indexed type family ò(a). The M-type is exactly the construction of this final coalgebra.
While one can reason about coinductive data types using the uniqueness of <code>corec</code> directly, it is often more convenient to use coinduction, which can prove equalities of codata. Given a final coalgebra A of a polynomial functor FâÂÂi.e. 'â we say that a relation is a bisimulation if, for all , and for all . Here, and refer to the maps:
The principle of coinduction states that for all bisimulations R on A and , .
More generally, for a coalgebra map , a relation R on A is a bisimulation if there exists a function satisfying, for all ,
where ÃÂâ and ÃÂâ are the first and second projection maps . It can be seen this equivalent to the polynomial case by setting . The required equalities can also be expressed as a commutative diagram:
Coinduction is easy to prove from the uniqueness of <code>corec</code>: ÃÂâ and ÃÂâ both satisfy the required property to be equal to <code>corec f</code>, and are therefore equal to each other, thus showing that .
To demonstrate the usage of coinduction, we will prove some basic properties about addition on conatural numbers. Addition can be defined identically to how it is defined for natural numbers:This definition, while valid, hides some amount of complexity. We may alternatively write:This definition makes the translation to <code>corec</code> straightforward:We can prove that by coinduction on the relation (where is the set of conatural numbers). First, it follows from the definition of addition that ; second, if we assume that is of the form for some a, we must show that is also of this form. We have: Thus , and therefore as required.
The identity may be similarly proven by coinduction on (remember the relation must necessarily include ); finally, commutativityâÂÂâÂÂresults from similar straightforward coinduction on .
If the domain of discourse is the category of sets and total functions (such as in theorem provers like Agda and Rocq), then final types (codata) may contain infinite, non-wellfounded values, whereas initial types (data) do not. On the other hand, if the domain of discourse is the category of complete partial orders and continuous functions, which corresponds roughly to the Haskell programming language, then final types coincide with initial types, and the corresponding final coalgebra and initial algebra form an isomorphism.
Corecursion, referred to as circular programming, dates at least to , who credits John Hughes and Philip Wadler; more general forms were developed in . The original motivations included producing more efficient algorithms (allowing a single pass over data in some cases, instead of requiring multiple passes) and implementing classical data structures, such as doubly linked lists and queues, in functional languages.