Lecture
Corecursion — in category theory and computer science, a type of operation dual to recursion. Corecursion is typically used (together with lazy evaluation) to generate infinite data structures.
While recursion works analytically, starting from data further from the base case and breaking it down into smaller data, repeating until the base case is reached, corecursion works synthetically, starting from the base case and building it up, iteratively producing data further removed from the base case. Put simply, corecursive algorithms use the data they themselves produce, bit by bit, as it becomes available and needed, to generate further bits of data. A similar but distinct concept is generative recursion, in which a definite «direction» inherent to corecursion and recursion may be absent.
Where recursion lets programs operate on arbitrarily complex data, provided it can be reduced to simple data (base cases), corecursion lets programs build arbitrarily complex and potentially infinite data structures, such as streams, provided they can be built up from simple data (base cases) in a sequence of finite steps. Where recursion may fail to terminate, never reaching a base case, corecursion starts from a base case and thus deterministically produces subsequent steps, though it may continue indefinitely (and therefore fail to terminate under strict evaluation), or it may consume more than it produces, thereby becoming non-productive. Many functions traditionally analyzed as recursive can alternatively, and perhaps more naturally, be interpreted as corecursive functions that terminate at a given stage, such as recurrence relations like the factorial.
Corecursion can produce both finite and infinite data structures as results and may use self-referential data structures. Corecursion is often used together with lazy evaluation to produce only a finite subset of a potentially infinite structure (rather than attempting to produce the entire infinite structure at once). Corecursion is an especially important concept in functional programming, where corecursion and codata allow languages to work with infinite data structures at all.
Corecursion, called circular programming, dates back at least to (Bird 1984), which cites John Hughes and Philip Wadler; more general forms were developed in (Allison 1989). The original motivation was to produce more efficient algorithms (in some cases allowing data to be passed through instead of requiring multiple passes) and to implement classical data structures, such as doubly linked lists and queues, in functional languages.
The rule for using corecursion on codata is dual to the rule for applying recursion on data. Instead of folding a data structure using a result recursively derived from a value for the base case, corecursion unfolds a result starting from an initial value. Note that corecursion produces potentially infinite data structures, whereas ordinary recursion analyzes (deconstructs) finite data structures as needed. Ordinary recursion is not applicable to codata, since the analysis process might never terminate. Correspondingly, corecursion cannot fully produce data, since data is always finite; but every partial result of a productive corecursion is finite and can be interpreted as data.
Corecursion can be understood by contrast with recursion, which is more familiar. Although corecursion is primarily of interest in functional programming, it can be illustrated using imperative programming, done below with a generator facility in Python. These examples use local variables and assign values to them imperatively (destructively), although in pure functional programming this is not necessary for corecursion. In pure functional programming, instead of being assigned to local variables, these computed values form an immutable sequence, and access to previous values happens through self-reference (later values in the sequence refer to earlier values in the sequence being computed). The assignments simply express this within the imperative paradigm and explicitly show where the computations happen, which helps clarify the presentation.
An example of using the corecursion mechanism in Haskell (computing an infinite list of Fibonacci numbers):
Another example is computing an infinite list of prime numbers:
This function (inefficiently) implements the «trial division» algorithm.
The Haskell examples given are not entirely accurate, since the language has no codata idiom. In these examples, codata is only emulated using an unboundedly-defined («infinite») list.
Comments