Corecursion

From Wikipedia, the free encyclopedia

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 a definition is an instance of lazy evaluation and an important part of Haskell programming.

[edit] See also

• bisimulation
• coinduction