Where recursion may not terminate, never reaching a base state, corecursion starts from a base state, and thus produces subsequent steps deterministically, though it may proceed indefinitely (and thus not terminate under strict evaluation), or it may consume more than it produces and thus become non-productive.
In these examples local variables are used, and assigned values imperatively (destructively), though these are not necessary in corecursion in pure functional programming.
The assignments simply express this in the imperative paradigm and explicitly specify where the computations happen, which serves to clarify the exposition.
This stack unwinding can be explicated, defining the factorial corecursively, as an iterator, where one starts with the case of
via: If we're only interested in a certain factorial, just the last value can be taken, or we can fuse the production and the access into one function, As can be readily seen here, this is practically equivalent (just by substituting return for the only yield there) to the accumulator argument technique for tail recursion, unwound into an explicit loop.
Thus it can be said that the concept of corecursion is an explication of the embodiment of iterative computation processes by recursive definitions, where applicable.
The root node's value is handled separately, whether before the first child is traversed (resulting in pre-order traversal), after the first is finished and before the second (in-order), or after the second child node is finished (post-order) — assuming the tree is binary, for simplicity of exposition.
To have it actually performed in the intended left-to-right order the sequencing would need to be enforced by some extraneous means, or it would be automatically achieved if the output were to be built in the top-down fashion, i.e. corecursively.
As in the factorial example above, where the auxiliary information of the index (which step one was at, n) was pushed forward, in addition to the actual output of n!, in this case the auxiliary information of the remaining subtrees is pushed forward, in addition to the actual output.
This shows the usefulness of corecursion rather than recursion for dealing with infinite data structures.
One caveat still remains for trees with the infinite branching factor, which need a more attentive interlacing to explore the space better.
The breadth-first corecursive generator can be defined as:[g] This can then be called to print the values of the nodes of the tree in breadth-first order: Initial data types can be defined as being the least fixpoint (up to isomorphism) of some type equation; the isomorphism is then given by an initial algebra.
[1][2] 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.
[5] The examples used in this article predate the attempts to define corecursion and explain what it is.
Thus corecursion creates (potentially infinite) codata, whereas ordinary recursion analyses (necessarily finite) data.
Following the above notation, the sequence of primes (with a throwaway 0 prefixed to it) and numbers streams being progressively sieved, can be represented as or in Haskell, The authors discuss how the definition of sieve is not guaranteed always to be productive, and could become stuck e.g. if called with [5,10..] as the initial stream.
The following definition produces the list of Fibonacci numbers in linear time: This infinite list depends on lazy evaluation; elements are computed on an as-needed basis, and only finite prefixes are ever explicitly represented in memory.
This can be done in Python as well:[7] The definition of zipWith can be inlined, leading to this: This example employs a self-referential data structure.
The following definition produces a breadth-first traversal of a binary tree in the top-down manner, in linear time (already incorporating the flattening mentioned above): This definition takes a tree and produces a list of its sub-trees (nodes and leaves).
The length of the queue must be explicitly tracked in order to ensure termination; this can safely be elided if this definition is applied only to infinite trees.
This Haskell code uses self-referential data structure, but does not essentially depend on lazy evaluation.
For that, Prolog has tail recursion modulo cons (i.e. open ended lists).
using linked lists with mutable tail sentinel pointer: Another particular example gives a solution to the problem of breadth-first labeling.
This solution employs a self-referential data structure, and the binary tree can be finite or infinite.
The Coq proof assistant supports corecursion and coinduction using the CoFixpoint command.
Corecursion, referred to as circular programming, dates at least to (Bird 1984), who credits John Hughes and Philip Wadler; more general forms were developed in (Allison 1989).
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.