共递归
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" we find
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))
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, sieve h t)) `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 (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 can be done in Python as well:
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)
The definition of zipWith can be inlined, leading to this:
fibs = 0 : 1 : next fibs
  where
    next (a: t@(b:_)) = (a+b):next t
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 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 : gen 1 queue

    gen  0   p                 =         []           
    gen len (Leaf   _     : s) =         gen (len-1) s 
    gen len (Branch _ l r : s) = l : r : gen (len+1) s
This definition takes an initial tree and produces a list of subtrees.   This list serves dual purpose as both the queue and the result (gen len p produces its output len notches after its input back-pointer, p, along the queue).  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.
Another particularly good example gives a solution to the problem of breadth-first labeling. 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) = go t (1:ns)

    go :: Tree a b    -> [Int]  -> (Tree Int Int, [Int])
    go   (Leaf   _    ) (n:ns) = (Leaf   n       , n+1 : ns  )
    go   (Branch _ l r) (n:ns) = (Branch n l′ r′ , n+1 : ns′′)
                                where
                                  (l′, ns′ ) = go l ns
                                  (r′, ns′′) = go r ns′
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.