Corecursion

Last updated

In computer science, corecursion is a type of operation that is dual to recursion. Whereas recursion works analytically, starting on data further from a base case and breaking it down into smaller data and repeating until one reaches a base case, corecursion works synthetically, starting from a base case and building it up, iteratively producing data further removed from a base case. Put simply, corecursive algorithms use the data that they themselves produce, bit by bit, as they become available, and needed, to produce further bits of data. A similar but distinct concept is generative recursion , which may lack a definite "direction" inherent in corecursion and recursion.

Contents

Where recursion allows programs to operate on arbitrarily complex data, so long as they 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) in a sequence of finite steps. 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. Many functions that are traditionally analyzed as recursive can alternatively, and arguably more naturally, be interpreted as corecursive functions that are terminated at a given stage, for example recurrence relations such as the factorial.

Corecursion can produce both finite and infinite data structures as results, and may employ self-referential data structures. Corecursion is often used in conjunction with lazy evaluation, to produce only 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 by 0! := 1 and n! := n × (n - 1)!.

To recursively compute its result on a given input, a recursive function calls (a copy of) itself with a different ("smaller" in some way) input and uses the result of this call to construct its result. The recursive call does the same, unless the base case has been reached. Thus a call stack develops in the process. For example, to compute fac(3), this recursively calls in turn 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 and the results are calculated on the way back along the call stack to the initial call frame fac(3) that uses the result of fac(2) = 2 to calculate the final result as 3 × 2 = 3 × fac(2) =: fac(3) and finally return fac(3) = 6. In this example a function returns a single value.

This stack unwinding can be explicated, defining the factorial corecursively, as an iterator, where one starts with the case of , then from this starting value constructs factorial values for increasing numbers 1, 2, 3... as in the above recursive definition with "time arrow" reversed, as it were, by reading it backwards as . The corecursive algorithm thus defined produces a stream of all factorials. This may be concretely implemented as a generator. Symbolically, noting that computing next factorial value requires keeping track of both n and f (a previous factorial value), this can be represented as:

or in Haskell,

(\(n,f)->(n+1,f*(n+1)))`iterate`(0,1)

meaning, "starting from , on each step the next values are calculated as ". This is mathematically equivalent and almost identical to the recursive definition, but the emphasizes that the factorial values are being built up, going forwards from the starting case, rather than being computed after first going backwards, down to the base case, with a decrement. The direct output of the corecursive function does not simply contain the factorial values, but also includes for each value the auxiliary data of its index n in the sequence, so that any one specific result can be selected among them all, as and when needed.

There is a connection with denotational semantics, where the denotations of recursive programs is built up corecursively in this way.

In Python, a recursive factorial function can be defined as: [lower-alpha 1]

deffactorial(n:int)->int:"""Recursive factorial function."""ifn==0:return1else:returnn*factorial(n-1)

This could then be called for example as factorial(5) to compute 5!.

A corresponding corecursive generator can be defined as:

deffactorials():"""Corecursive generator."""n,f=0,1whileTrue:yieldfn,f=n+1,f*(n+1)

This generates an infinite stream of factorials in order; a finite portion of it can be produced by:

defn_factorials(n:int):k,f=0,1whilek<=n:yieldfk,f=k+1,f*(k+1)

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

forfinn_factorials(5):print(f)

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,

defnth_factorial(n:int):k,f=0,1whilek<n:k,f=k+1,f*(k+1)returnf

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.

Fibonacci sequence

In the same way, the Fibonacci sequence can be represented as:

Because the Fibonacci sequence is a recurrence relation of order 2, the corecursive relation must track two successive terms, with the corresponding to shift forward by one step, and the corresponding to computing the next term. This can then be implemented as follows (using parallel assignment):

deffibonacci_sequence():a,b=0,1whileTrue:yieldaa,b=b,a+b

In Haskell,

mapfst((\(a,b)->(b,a+b))`iterate`(0,1))

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.

Iteratively, one may traverse a tree by placing its root node in a data structure, then iterating with that data structure while it is non-empty, on each step removing the first node from it and placing the removed node's child nodes back into that data structure. If the data structure is a stack (LIFO), this yields depth-first traversal, and if the data structure is a queue (FIFO), this yields breadth-first traversal:

Using recursion, a depth-first traversal of a tree is implemented simply as recursively traversing each of the root node's child nodes in turn. Thus the second child subtree is not processed until the first child subtree is finished. 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. The call stack (of the recursive traversal function invocations) corresponds to the stack that would be iterated over with the explicit LIFO structure manipulation mentioned above. Symbolically,

"Recursion" has two meanings here. First, the recursive invocations of the tree traversal functions . More pertinently, we need to contend with how the resulting list of values is built here. Recursive, bottom-up output creation will result in the right-to-left tree traversal. 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.

A breadth-first traversal creating its output in the top-down order, corecursively, can be also implemented by starting at the root node, outputting its value, [lower-alpha 2] 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 values of all of their root nodes, then passing on their child subtrees, etc. [lower-alpha 3] 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,

meaning that at each step, one outputs the list of values in this level's nodes, then proceeds to the next level's nodes. 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). This is extensionally equivalent to the specification above. In Haskell,

concatMapfst((\(v,ts)->(rootValuests,childTreests))`iterate`([],[fullTree]))

Notably, given an infinite tree, [lower-alpha 4] 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. One caveat still remains for trees with the infinite branching factor, which need a more attentive interlacing to explore the space better. See dovetailing.

In Python, this can be implemented as follows. [lower-alpha 5] The usual post-order depth-first traversal can be defined as: [lower-alpha 6]

defdf(node):"""Post-order depth-first traversal."""ifnodeisnotNone: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: [lower-alpha 7]

defbf(tree):"""Breadth-first corecursive generator."""tree_list=[tree]whiletree_list:new_tree_list=[]fortreeintree_list:iftreeisnotNone:yieldtree.valuenew_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:

foriinbf(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. [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. [3]

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. [4]

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. [5] 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.

In "Programming with streams in Coq: a case study: the Sieve of Eratosthenes" [6] we find

hd(concas)=atl(concas)=s(sieveps)=ifdivp(hds)thensievep(tls)elseconc(hds)(sievep(tls))hd(primess)=(hds)tl(primess)=primes(sieve(hds)(tls))

where primes "are obtained by applying the primes operation to the stream (Enu 2)". 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,

(\(p,s@(h:t))->(h,sieveht))`iterate`(0,[2..])

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.

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

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

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 can be done in Python as well: [7]

fromitertoolsimporttee,chain,islice,imapdefadd(x,y):returnx+ydeffibonacci():defdeferred_output():foriinoutput:yieldiresult,c1,c2=tee(deferred_output(),3)paired=imap(add,c1,islice(c2,1,None))output=chain([0,1],paired)returnresultforiinislice(fibonacci(),20):print(i)

The definition of zipWith can be inlined, leading to this:

fibs=0:1:nextfibswherenext(a:t@(b:_))=(a+b):nextt

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 this guarded recursion gradually produces an indefinitely defined list.

Corecursion need not produce an infinite object; a corecursive queue [8] is a particularly good example of this phenomenon. 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):

dataTreeab=Leafa|Branchb(Treeab)(Treeab)bftrav::Treeab->[Treeab]bftravtree=tree:tswherets=gen1(tree:ts)gen0p=[]genlen(Leaf_:p)=gen(len-1)pgenlen(Branch_lr:p)=l:r:gen(len+1)p--       ----read----        ----write-ahead----- bfvalues tree = [v | (Branch v _ _) <- bftrav tree]

This definition takes a tree and produces a list of its sub-trees (nodes and leaves). This list serves dual purpose as both the input queue and the result (gen len p produces its output len notches ahead of its input back-pointer, p, along the list). 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.

This Haskell code uses self-referential data structure, but does not essentially depend on lazy evaluation. It can be straightforwardly translated into e.g. Prolog which is not a lazy language. What is essential is the ability to build a list (used as the queue) in the top-down manner. For that, Prolog has tail recursion modulo cons (i.e. open ended lists). Which is also emulatable in Scheme, C, etc. using linked lists with mutable tail sentinel pointer:

bftrav(Tree,[Tree|TS]):-bfgen(1,[Tree|TS],TS).bfgen(0,_,[]):-!.% 0 entries in the queue -- stop and close the listbfgen(N,[leaf(_)|P],TS):-N2isN-1,bfgen(N2,P,TS).bfgen(N,[branch(_,L,R)|P],[L,R|TS]):-N2isN+1,bfgen(N2,P,TS).%%         ----read-----      --write-ahead--

Another particular example gives a solution to the problem of breadth-first labeling. [9] The function label visits every node in a binary tree in the breadth first fashion, replacing each label with an integer, each subsequent integer bigger than the last by 1. This solution employs a self-referential data structure, and the binary tree can be finite or infinite.

label::Treeab->TreeIntIntlabelt=tnwhere(tn,ns)=got(1:ns)go::Treeab->[Int]->(TreeIntInt,[Int])go(Leaf_)(i:a)=(Leafi,i+1:a)go(Branch_lr)(i:a)=(Branchilnrn,i+1:c)where(ln,b)=gola(rn,c)=gorb

Or in Prolog, for comparison,

label(Tree,Tn):-label(Tree,[1|Ns],Tn,Ns).label(leaf(_),[I|A],leaf(I),[I+1|A]).label(branch(_,L,R),[I|A],branch(I,Ln,Rn),[I+1|C]):-label(L,A,Ln,B),label(R,B,Rn,C).

An apomorphism (such as an anamorphism, such as unfold) is a form of corecursion in the same way that a paramorphism (such as a catamorphism, such as fold) 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 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.

See also

Notes

  1. Not validating input data.
  2. Breadth-first traversal, unlike depth-first, is unambiguous, and visits a node value before processing children.
  3. Technically, one may define a breadth-first traversal on an ordered, disconnected set of trees – first the root node of each tree, then the children of each tree in turn, then the grandchildren in turn, etc.
  4. Assume fixed branching factor (e.g., binary), or at least bounded, and balanced (infinite in every direction).
  5. First defining a tree class, say via:
    classTree:def__init__(self,value,left=None,right=None):self.value=valueself.left=leftself.right=rightdef__str__(self):returnstr(self.value)
    and initializing a tree, say via:
    t=Tree(1,Tree(2,Tree(4),Tree(5)),Tree(3,Tree(6),Tree(7)))
    In this example nodes are labeled in breadth-first order: 1 2 3 4 5 6 7
  6. Intuitively, the function iterates over subtrees (possibly empty), then once these are finished, all that is left is the node itself, whose value is then returned; this corresponds to treating a leaf node as basic.
  7. Here the argument (and loop variable) is considered as a whole, possible infinite tree, represented by (identified with) its root node (tree = root node), rather than as a potential leaf node, hence the choice of variable name.

Related Research Articles

<span class="mw-page-title-main">Binary search tree</span> Rooted binary tree data structure

In computer science, a binary search tree (BST), also called an ordered or sorted binary tree, is a rooted binary tree data structure with the key of each internal node being greater than all the keys in the respective node's left subtree and less than the ones in its right subtree. The time complexity of operations on the binary search tree is linear with respect to the height of the tree.

<span class="mw-page-title-main">Binary tree</span> Limited form of tree data structure

In computer science, a binary tree is a tree data structure in which each node has at most two children, referred to as the left child and the right child. That is, it is a k-ary tree with k = 2. A recursive definition using set theory is that a binary tree is a tuple (L, S, R), where L and R are binary trees or the empty set and S is a singleton set containing the root.

ML is a functional programming language. It is known for its use of the polymorphic Hindley–Milner type system, which automatically assigns the data types of most expressions without requiring explicit type annotations, and ensures type safety; there is a formal proof that a well-typed ML program does not cause runtime type errors. ML provides pattern matching for function arguments, garbage collection, imperative programming, call-by-value and currying. While a general-purpose programming language, ML is used heavily in programming language research and is one of the few languages to be completely specified and verified using formal semantics. Its types and pattern matching make it well-suited and commonly used to operate on other formal languages, such as in compiler writing, automated theorem proving, and formal verification.

<span class="mw-page-title-main">Tree (data structure)</span> Linked node hierarchical data structure

In computer science, a tree is a widely used abstract data type that represents a hierarchical tree structure with a set of connected nodes. Each node in the tree can be connected to many children, but must be connected to exactly one parent, except for the root node, which has no parent. These constraints mean there are no cycles or "loops", and also that each child can be treated like the root node of its own subtree, making recursion a useful technique for tree traversal. In contrast to linear data structures, many trees cannot be represented by relationships between neighboring nodes in a single straight line.

<span class="mw-page-title-main">Breadth-first search</span> Algorithm to search the nodes of a graph

Breadth-first search (BFS) is an algorithm for searching a tree data structure for a node that satisfies a given property. It starts at the tree root and explores all nodes at the present depth prior to moving on to the nodes at the next depth level. Extra memory, usually a queue, is needed to keep track of the child nodes that were encountered but not yet explored.

<span class="mw-page-title-main">Depth-first search</span> Search algorithm

Depth-first search (DFS) is an algorithm for traversing or searching tree or graph data structures. The algorithm starts at the root node and explores as far as possible along each branch before backtracking. Extra memory, usually a stack, is needed to keep track of the nodes discovered so far along a specified branch which helps in backtracking of the graph.

In combinatory logic for computer science, a fixed-point combinator, is a higher-order function that returns some fixed point of its argument function, if one exists.

In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.

In computer science, tree traversal is a form of graph traversal and refers to the process of visiting each node in a tree data structure, exactly once. Such traversals are classified by the order in which the nodes are visited. The following algorithms are described for a binary tree, but they may be generalized to other trees as well.

In computer science, a tail call is a subroutine call performed as the final action of a procedure. If the target of a tail is the same subroutine, the subroutine is said to be tail recursive, which is a special case of direct recursion. Tail recursion is particularly useful, and is often easy to optimize in implementations.

In computer programming languages, a recursive data type is a data type for values that may contain other values of the same type. Data of recursive types are usually viewed as directed graphs.

In computer science, a leftist tree or leftist heap is a priority queue implemented with a variant of a binary heap. Every node x has an s-value which is the distance to the nearest leaf in subtree rooted at x. In contrast to a binary heap, a leftist tree attempts to be very unbalanced. In addition to the heap property, leftist trees are maintained so the right descendant of each node has the lower s-value.

<span class="mw-page-title-main">Recursion (computer science)</span> Use of functions that call themselves

In computer science, recursion is a method of solving a computational problem where the solution depends on solutions to smaller instances of the same problem. Recursion solves such recursive problems by using functions that call themselves from within their own code. The approach can be applied to many types of problems, and recursion is one of the central ideas of computer science.

The power of recursion evidently lies in the possibility of defining an infinite set of objects by a finite statement. In the same manner, an infinite number of computations can be described by a finite recursive program, even if this program contains no explicit repetitions.

In functional programming, fold refers to a family of higher-order functions that analyze a recursive data structure and through use of a given combining operation, recombine the results of recursively processing its constituent parts, building up a return value. Typically, a fold is presented with a combining function, a top node of a data structure, and possibly some default values to be used under certain conditions. The fold then proceeds to combine elements of the data structure's hierarchy, using the function in a systematic way.

A zipper is a technique of representing an aggregate data structure so that it is convenient for writing programs that traverse the structure arbitrarily and update its contents, especially in purely functional programming languages. The zipper was described by Gérard Huet in 1997. It includes and generalizes the gap buffer technique sometimes used with arrays.

In computing, a rose tree is a term for the value of a tree data structure with a variable and unbounded number of branches per node. The term is mostly used in the functional programming community, e.g., in the context of the Bird–Meertens formalism. Apart from the multi-branching property, the most essential characteristic of rose trees is the coincidence of bisimilarity with identity: two distinct rose trees are never bisimilar.

In descriptive set theory, the Kleene–Brouwer order or Lusin–Sierpiński order is a linear order on finite sequences over some linearly ordered set , that differs from the more commonly used lexicographic order in how it handles the case when one sequence is a prefix of the other. In the Kleene–Brouwer order, the prefix is later than the longer sequence containing it, rather than earlier.

In computer science, and in particular functional programming, a hylomorphism is a recursive function, corresponding to the composition of an anamorphism followed by a catamorphism. Fusion of these two recursive computations into a single recursive pattern then avoids building the intermediate data structure. This is an example of deforestation, a program optimization strategy. A related type of function is a metamorphism, which is a catamorphism followed by an anamorphism.

In mathematics, specifically in graph theory and number theory, a hydra game is a single-player iterative mathematical game played on a mathematical tree called a hydra where, usually, the goal is to cut off the hydra's "heads" while the hydra simultaneously expands itself. Hydra games can be used to generate large numbers or infinite ordinals or prove the strength of certain mathematical theories.

This article describes the features in the programming language Haskell.

References

  1. Barwise and Moss 1996.
  2. Moss and Danner 1997.
  3. Smyth and Plotkin 1982.
  4. Gibbons and Hutton 2005.
  5. Doets and van Eijck 2004.
  6. Leclerc and Paulin-Mohring, 1994
  7. Hettinger 2009.
  8. Allison 1989; Smith 2009.
  9. Jones and Gibbons 1992.