Corecursion

In computer science, corecursion is a type of operation that is dual to recursion. Corecursion is often used in conjunction with lazy evaluation. Corecursion can denote both finite and infinite data structures, and may or may not employ self-referential 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 by pattern-matching on its constructors, we ascend on the result by filling-in its "destructors" (or "observers"). Notice that corecursion creates (potentially infinite) codata, whereas ordinary recursion analyses (necessarily finite) data. Ordinary recursion might not be 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)

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 feature allows algorithms on parts of codata to terminate; such techniques are an important part of Haskell programming.

This example employs a self-referential data structure. Ordinary recursion makes use of self-referential functions, but does not accommodate self-referential data. However, this is not essential to the Fibonacci example. It can be rewritten as follows:

fibs = fibs' 0 1
fibs' x y = x : fibs' y (x+y)

This rewrite employs only self-referential functions, but it is still an example of corecursion. It still produces an infinite list and depends on lazy evaluation.

This shows how it can be done in Python^[1]:

def fibonacci():
    def deferred_output():
        for i in output:
            yield i
 
    result, c1, c2 = tee(deferred_output(), 3)
    paired = imap(add, c1, islice(c2, 1, None))
    output = chain([0, 1], paired)
    return result

Corecursion need not produce an infinite object; a corecursive queue^[2] is a particularly good example of this phenomenon. The following definition produces a breadth-first traversal of a binary tree in linear time:

data Tree a b = Leaf a  |  Branch b (Tree a b) (Tree a b)
 
bftrav :: Tree a b -> [Tree a b]
bftrav tree = queue
  where
    queue = tree : trav 1 queue
 
    trav  0   q                 =         []
    trav len (Leaf   _     : q) =         trav (len-1) q
    trav len (Branch _ l r : q) = l : r : trav (len+1) q

This definition takes an initial tree and produces list of subtrees. This list serves a dual purpose as both the queue and the result. It is finite if and only if the initial tree is finite. 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. Even if the result is finite, this example depends on lazy evaluation due to the use of self-referential data structures.

Another particularly good example gives a solution to the problem of breadth-first labelling.^[3] The function label visits every node in a binary tree in a breadth first fashion, and replaces each label with an integer, each subsequent integer is bigger than the last by one. This solution employs a self-referential data structure, and the binary tree can be finite or infinite.

label :: Tree a b -> Tree Int Int 
label t = t'
    where
          (t',ns) = label' t (1:ns)
 
label' :: Tree a b    -> [Int]  -> (Tree Int Int, [Int])
label'    (Leaf   _    ) (n:ns) = (Leaf   n       , n+1 : ns  )
label'    (Branch _ l r) (n:ns) = (Branch n l' r' , n+1 : ns'')
                                where
                                  (l',ns' ) = label' l ns
                                  (r',ns'') = label' r ns'

An anamorphism is a form of corecursion in the same way that a catamorphism is a form of recursion.

The Coq proof assistant supports corecursion and coinduction using the CoFixpoint command.

See also

• Bisimulation
• Coinduction

Notes

References

• David Turner (2004-07-28). "Total Functional Programming". Journal of Universal Computer Science 10 (7): 751–768. doi:10.3217/jucs-010-07-0751. http://www.jucs.org/jucs_10_7/total_functional_programming. 
• Lloyd Allison (1989-04). "Circular Programs and Self-Referential Structures". Software Practice and Experience 19 (2): 99–109. http://www.csse.monash.edu.au/~lloyd/tildeFP/1989SPE/. 
• Leon P Smith (2009-07-29), "Lloyd Allison's Corecursive Queues: Why Continuations Matter", The Monad Reader (14): 37–68, http://themonadreader.wordpress.com/2009/07/29/issue-14/ 
• Geraint Jones and Jeremy Gibbons (1992). Linear-time breadth-first tree algorithms: An exercise in the arithmetic of folds and zips. Technical Report Dept of Computer Science, University of Auckland.
• Python Recipe 576961 by Raymond Hettinger: Technique for cyclical iteration: http://code.activestate.com/recipes/576961/