corecursion

In computer science, corecursion is a type of operation that is dual to recursion. Corecursion is typically used (in conjunction with lazy evaluation) to generate infinite data structures.

The rule for primitive corecursion on codata is the dual to that for primitive recursion on data. Instead of descending on the argument, we ascend on the result. Notice that corecursion creates (potentially infinite) codata, whereas ordinary recursion analyses (necessarily finite) data. Ordinary recursion is not applicable to the codata because it might not terminate. Conversely, corecursion is not applicable if the result type is data, because data must be finite.

Here is an example in Haskell. The following definition produces the list of Fibonacci numbers in linear time:

fibs = 0 : 1 : zipWith (+) fibs (tail fibs)

The infinite list is produced by corecursion — the latter values of the list are computed on demand starting from the initial two items 0 and 1. This kind of definition is possible only because of lazy evaluation, which allows algorithms on parts of codata to terminate; such techniques are an important part of Haskell programming.

References

• David Turner (2004-07-28). "Total Functional Programming". Journal of Universal Computer Science 10 (7): 751–768. 

See also

• Bisimulation
• Coinduction

Donate to Wikimedia