Editing Corecursion (section)

==Discussion==
{{cleanup|section|reason=mix of discussion, examples, and related concepts|date=July 2012}}
The rule for ''primitive corecursion'' on [[codata (computer science)|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"<ref>Leclerc and Paulin-Mohring, 1994</ref> we find
<syntaxhighlight lang="haskell">
hd (conc a s) = a               
tl (conc a s) = s

(sieve p s) = if div p (hd s) then sieve p (tl s)
              else conc (hd s) (sieve p (tl s))

hd (primes s) = (hd s)          
tl (primes s) = primes (sieve (hd s) (tl s))
</syntaxhighlight>
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 
:<math>p, s = (0, [2..]) : (hd(s), sieve(hd(s),tl(s)))</math>
or in Haskell, 
<syntaxhighlight lang="haskell">
(\(p, s@(h:t)) -> (h, sieve h t)) `iterate` (0, [2..])
</syntaxhighlight>
The authors discuss how the definition of <code>sieve</code> is not guaranteed always to be ''productive'', and could become stuck e.g. if called with <code>[5,10..]</code> as the initial stream.

Here is another example in Haskell. The following definition produces the list of [[Fibonacci numbers]] in linear time:
<syntaxhighlight lang=haskell>
fibs = 0 : 1 : zipWith (+) fibs (tail fibs)
</syntaxhighlight>

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:<ref>Hettinger 2009.</ref>
<syntaxhighlight lang="pycon">
>>> from itertools import tee, chain, islice
>>> def fibonacci():
...     def deferred_output():
...         yield from output
...
...     result, c1, c2 = tee(deferred_output(), 3)
...     paired = (x + y for x, y in zip(c1, islice(c2, 1, None)))
...     output = chain([0, 1], paired)
...     return result
>>> print(*islice(fibonacci(), 20), sep=', ')
0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181
</syntaxhighlight>

The definition of <code>zipWith</code> can be inlined, leading to this:

<syntaxhighlight lang="haskell">
fibs = 0 : 1 : next fibs
  where
    next (a: t@(b:_)) = (a+b):next t
</syntaxhighlight>

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:

<syntaxhighlight lang="haskell">
fibs = fibgen (0,1)
fibgen (x,y) = x : fibgen (y,x+y) 
</syntaxhighlight>

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 [[lazy evaluation|non-strict]] list constructor this guarded recursion gradually produces an indefinitely defined list.

{{anchor|corecursive queue breadth-first tree traversal}}Corecursion need not produce an infinite object; a corecursive queue<ref>Allison 1989; Smith 2009.</ref> is a particularly good example of this phenomenon. The following definition produces a [[Breadth-first search|breadth-first traversal]] of a binary tree in the ''top-down'' manner, in linear time (already incorporating the flattening mentioned [[#Tree traversal|above]]):

<syntaxhighlight lang="haskell">
data Tree a b = Leaf a
              | Branch b (Tree a b) (Tree a b)

bftrav :: Tree a b -> [Tree a b]
bftrav tree = tree : ts
  where
  ts = gen 1 (tree : ts)

  gen  0   p                 =         []           
  gen len (Leaf   _     : p) =         gen (len-1) p
  gen len (Branch _ l r : p) = l : r : gen (len+1) p
  --       ----read----        ----write-ahead---

-- bfvalues tree = [v | (Branch v _ _) <- bftrav tree]
</syntaxhighlight>

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 (<small>''<code>gen len p</code>''</small> produces its output <small>''<code>len</code>''</small> notches ahead of its input back-pointer, <small>''<code>p</code>''</small>, 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.  <!-- Even if the result is finite, this example depends on lazy evaluation due to the use of self-referential data structures.

why the above was removed: it isn't true: --> 

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 call#Tail recursion modulo cons|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:

<syntaxhighlight lang="prolog">
bftrav( Tree,  [Tree|TS]) :- bfgen( 1, [Tree|TS],   TS).

bfgen( 0, _,   []) :- !.  % 0 entries in the queue -- stop and close the list
bfgen( N, [leaf(_)      |P],   TS      ) :- N2 is N-1, bfgen( N2, P,   TS).
bfgen( N, [branch(_,L,R)|P],   [L,R|TS]) :- N2 is N+1, bfgen( N2, P,   TS).
%%         ----read-----      --write-ahead--
</syntaxhighlight>

Another particular example gives a solution to the problem of breadth-first labeling.<ref>Jones and Gibbons 1992.</ref> The function <code>label</code> 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.

<syntaxhighlight lang="haskell">
label :: Tree a b -> Tree Int Int 
label t = tn
  where
  (tn, ns) = go t (1:ns)

  go :: Tree a b -> [Int] ->  (Tree Int Int, [Int])
  go (Leaf   _    ) (i:a) = (Leaf   i      , i+1:a)
  go (Branch _ l r) (i:a) = (Branch i ln rn, i+1:c)
       where
       (ln, b) = go l a
       (rn, c) = go r b
</syntaxhighlight>
Or in Prolog, for comparison,
<syntaxhighlight lang="prolog">
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).
</syntaxhighlight>

An [[apomorphism]] (such as an [[anamorphism]], such as [[Unfold (higher-order function)|unfold]]) is a form of corecursion in the same way that a [[paramorphism]] (such as a [[catamorphism]], such as [[Fold (higher-order function)|fold]]) is a form of recursion.

The [[Coq (software)|Coq]] proof assistant supports corecursion and [[coinduction]] using the CoFixpoint command.