Corecursion

In computer science, corecursion is a type of operation that is dual to recursion. Where recursion works backwards (analytically, deductively), working on large data (more properly, data further from a base case) by breaking it into smaller data and repeating until one reaches a base case, corecursion works forward (synthetically, inductively), starting from a base case and iteratively producing larger data (more properly, later data, further removed from a base case). Put simply, it is about algorithms using the data which they themselves produce, bit by bit, as they become available, and needed, to produce further bits of data.

Where recursion allows programs to operate on arbitrarily complex data, so long as it can be reduced to simple data (base cases), corecursion allows programs to produce arbitrarily complex and potentially infinite data structures, such as streams, so long as it can be produced from simple data (base cases). Where recursion may not terminate, never reaching a base state, corecursion starts from a base state, and thus produces subsequent steps deterministically, but the result may be infinite (and thus not terminate).

Corecursion can produce both finite and infinite data structures as result, and may employ self-referential data structures. Corecursion is often used in conjunction with lazy evaluation, to only produce a finite subset of a potentially infinite structure (rather than trying to produce an entire infinite structure at once). Corecursion is a particularly important concept in functional programming, where corecursion and codata allow total languages to work with infinite data structures.

Examples

Corecursion can be understood by contrast with recursion, which is more familiar. While corecursion is primarily of interest in functional programming, it can be illustrated using imperative programming, which is done below using the generator facility in Python. In these examples local variables are used, and assigned values imperatively (destructively), though these are not necessary in corecursion in pure functional programming. In pure functional programming, rather than assigning to local variables, these computed values form an invariable sequence, and prior values are accessed by self-reference (later values in the sequence reference earlier values in the sequence to be computed). The assignments simply express this in the imperative paradigm and explicitly specify where the computations happen, which serves to clarify the exposition.

Factorial

A classic example of recursion is computing the factorial, which is defined recursively as $0!:=1$ and $n!:=n\times (n-1)!$ To compute the value of the function on a given input, the function calls itself with a different input, and repeats until it terminates. In the process, a large call stack develops. For example, to compute fac(3), recursively computing this calls in turn fac(3), fac(2), fac(1), fac(0) ("winding up" the stack), at which point recursion terminates with fac(0) = 1, and then the stack unwinds in reverse order. In this example a function returns a single value.

By contrast, the factorial can be defined corecursively, where instead of being a function, it is an iterator, which returns the list of all factorials, which may be concretely implemented as a generator. Symbolically, noting that computing the list of factorials requires keeping track of both n and f=n!, this can be represented as:

$n,f=(0,1):(n+1,f*(n+1))$

meaning "base case is $0!:=1$, with $(n+1)!:=n!\times (n+1)$". This is mathematically equivalent and almost identical to the recursive definition, but the $+1$ emphasizes that the list is built up (forwards), rather than being computed down (backwards) as in the $-1$. Note also the direct output of the corecursive function is not simply the factorial $f=n!$ itself, but also includes the auxiliary data of the index n, what step one is at.

In Python, the recursive function can be defined as:

def fac(n):
    if (n == 0):
        return 1
    else:
        return n*fac(n-1)

This could then be called for example by fac(5) to compute 5!

The corresponding corecursive generator can be defined as:

def faclist():
    n = 0
    fac = 1
    while True:
        yield fac
        n += 1
        fac *= n

This generates an infinite list of the factorials in order; a finite list can be produced by:

def faclist(k):
    n = 0
    fac = 1
    while (n <= k):
        yield fac
        n += 1
        fac *= n

This could then be called to produce the factorials up to 5! via:

for f in faclist(5):
    print f

Tree traversal

Tree traversal via a depth-first approach is a classic example of recursion. Dually, breadth-first traversal can very naturally be implemented via corecursion.

Without using recursion or corecursion, one may traverse a tree by starting at the root node, placing the child nodes in a data structure, then removing the nodes in the data structure in turn and iterating over its children. If the data structure is a stack (LIFO), this yields depth-first traversal, while if the data structure is a queue (FIFO), this yields breadth-first traversal.

Using recursion, a (post-order) depth-first traversal can be implemented by starting at the root node and recursively traversing each child subtree in turn (the subtree based at each child node) – the second child subtree does not start processing until the first child subtree is finished. Once a leaf node is reached or the children of a branch node have been exhausted, the node itself is visited (e.g., the value of the node itself is outputted). In this case, the call stack (of the recursive functions) acts as the stack that is iterated over.

Using corecursion, a breadth-first traversal can be implemented by starting at the root node, outputting its value, then breadth-first traversing the subtrees – i.e., passing on the whole list of subtrees to the next step (not a single subtree, as in the recursive approach) – at the next step outputting the value of all of their root nodes, then passing on their child subtrees, etc. In this case the generator function, indeed the output sequence itself, acts as the queue. 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. Symbolically:

v,t = ([], FullTree) : (RootValues, ChildTrees)

meaning that at each step, one outputs the list of values of root nodes, then proceeds to the child subtrees. Generating just the node values from this sequence simply requires discarding the auxiliary child tree data, then flattening the list of lists (values are initially grouped by level (depth); flattening (ungrouping) yields a flat linear list).

These can be compared as follows. The recursive traversal handles a leaf node (at the bottom) as the base case (when there are no children, just output the value), and analyzes a tree into subtrees, traversing each in turn, eventually resulting in just leaf nodes – actual leaf nodes, and branch nodes whose children have already been dealt with (cut off below). By contrast, the corecursive traversal handles a root node (at the top) as the base case (given a node, first output the value), treats a tree as being synthesized of a root node and its children, then produces as auxiliary output a list of subtrees at each step, which are then the input for the next step – the child nodes of the original root are the root nodes at the next step, as their parents have already been dealt with (cut off above). Note also that in the recursive traversal there is a distinction between leaf nodes and branch nodes, while in the corecursive traversal there is no distinction, as each node is treated as the root node of the subtree it defines.

Notably, given an infinite tree, the corecursive breadth-first traversal will traverse all nodes, just as for a finite tree, while the recursive depth-first traversal will go down one branch and not traverse all nodes, and indeed if traversing post-order, as in this example (or in-order), it will visit no nodes at all, because it never reaches a leaf. This shows the usefulness of corecursion rather than recursion for dealing with infinite data structures.

In Python, this can be implemented as follows. The usual post-order depth-first traversal can be defined as:

def df(node):
    if node is not None:
        df(node.left)
        df(node.right)
        print node.value

This can then be called by df(t) to print the values of the nodes of the tree in post-order depth-first order.

The breadth-first corecursive generator can be defined as:

def bf(tree):
    tree_list = [tree]
    while tree_list != []:
        new_tree_list = []
        for tree in tree_list:
            if tree is not None:
                yield tree.value
                new_tree_list.append(tree.left)
                new_tree_list.append(tree.right)
        tree_list = new_tree_list

This can then be called to print the values of the nodes of the tree in breadth-first order:

for i in bf(t):
    print i

Definition

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. Dually, final (or terminal) data types can be defined as being the greatest fixpoint of a type equation; the isomorphism is then given by a final coalgebra.

If the domain of discourse is the category of sets and total functions, then final data types may contain infinite, non-wellfounded values, whereas initial types do not. 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.

Corecursion is then a technique for recursively defining functions whose range (codomain) is a final data type, dual to the way that ordinary recursion recursively defines functions whose domain is an initial data type.

The discussion below provides several examples in Haskell that distinguish corecursion. Roughly speaking, if one were to port these definitions to the category of sets, they would still be corecursive. This informal usage is consistent with existing textbooks about Haskell. Also note that the examples used in this article predate the attempts to define corecursion and explain what it is.

Discussion

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 (that were called up before, somewhere, so we receive a ready-made datum and get at its constituent sub-parts, i.e. "fields"), we ascend on the result by filling-in its "destructors" (or "observers", that will be called afterwards, somewhere - so we're actually calling a constructor, creating another bit of the result to be observed later on). Thus 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 strictly necessary 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 : next fibs
  where
    next (a: t@(b:_)) = (a+b):next t

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 = fibgen (0,1)
fibgen (x,y) = x : fibgen (y,x+y)

This employs only self-referential function to construct the result. If it were used with strict list constructor it would be an example of runaway recursion, but with non-strict list constructor it (corecursively) produces an indefinitely defined list.

This shows how it can be done in Python:

from itertools import tee, chain, islice, imap

def add(x,y): return (x + y)

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

for i in islice(fibonacci(),20):
  print i

Corecursion need not produce an infinite object; a corecursive queue 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. 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 apomorphism is a form of corecursion in the same way that a paramorphism is a form of recursion.

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

History

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 including producing more efficient algorithms (allowing 1 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.

See also

• Bisimulation
• Coinduction
• Recursion

References

• Lloyd Allison (1989-04). "Circular Programs and Self-Referential Structures". Software Practice and Experience. 19 (2): 99–109. doi:10.1002/spe.4380190202. {{cite journal}}: Check date values in: |date= (help)
• 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.
• Jon Barwise and Lawrence S Moss (1996-06). Vicious Circles. Center for the Study of Language and Information. ISBN 978-1-57586-009-1. {{cite book}}: Check date values in: |date= (help)
• Lawrence S Moss and Norman Danner (1997). "On the Foundations of Corecursion". Logic Journal of the IGPL. 5 (2): 231–257. doi:10.1093/jigpal/5.2.231.
• Kees Doets and Jan van Eijck (2004-05). The Haskell Road to Logic, Maths, and Programming. King's College Publications. ISBN 978-0-9543006-9-2. {{cite book}}: Check date values in: |date= (help)
• David Turner (2004-07-28). "Total Functional Programming". Journal of Universal Computer Science. 10 (7): 751–768. doi:10.3217/jucs-010-07-0751.
• Jeremy Gibbons and Graham Hutton (2005-04). "Proof methods for corecursive programs". Fundamenta Informaticae Special Issue on Program Transformation. 66 (4): 353–366. {{cite journal}}: Check date values in: |date= (help)
• Leon P Smith (2009-07-29), "Lloyd Allison's Corecursive Queues: Why Continuations Matter", The Monad Reader (14): 37–68
• Raymond Hettinger (2009-11-19). "Recipe 576961: Technique for cyclical iteration".
• M. B. Smyth and G. D. Plotkin (1982). "The Category-Theoretic Solution of Recursive Domain Equations". SIAM Journal on Computing. 11 (4): 761–783. doi:10.1137/0211062.