查看“︁共递归”︁的源代码

{{distinguish|互递归}}

'''共递归'''在计算机科学重视一类操作，与[[递归_(计算机科学)|递归]]在范畴论上[[对偶]]。因而递归是分析地工作，把数据分解为更小的数据直至达到基本情况。共递归是合成地工作，从基本情况构造出数据。共递归的数据是自己一点一点构造出来的。一个类似但不同的概念是''[[生成式递归]]''（generative recursion）。 
 
共递归常与[[惰性求值]]配合，产生一个潜在无穷结构的有限子集。 
{{transH}}

== 例子 ==
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 (computer programming)|generator]] facility in Python. In these examples local variables are used, and [[Assignment (computer science)|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 <math>0! := 1</math> and <math>n! := n \times (n-1)!</math>

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)'', where the final result is calculated as ''3*2 =: 6'' and finally returned. In this example a function returns a single value.

This stack unwinding can be explicated, defining the factorial ''corecursively'', as an [[Iteration|iterator]], where one ''starts'' with the case of <math>1 =: 0!</math>, 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 {{nobreak|<math>n! \times (n+1) =: (n+1)!</math>.}} The corecursive algorithm thus defined produces a ''stream'' of ''all'' factorials. This may be concretely implemented as a [[Generator (computer programming)|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:
:<math>n, f = (0, 1) : (n + 1, f \times (n+1))</math>
or in [[Haskell (programming language)|Haskell]], 
<syntaxhighlight lang=haskell>
  (\(n,f) -> (n+1, f*(n+1))) `iterate` (0,1)
</syntaxhighlight>
meaning, "starting from <math>n, f = 0, 1</math>, on each step the next values are calculated as <math>n+1, f \times (n+1)</math>". This is mathematically equivalent and almost identical to the recursive definition, but the <math>+1</math> 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 <math>-1</math> decrement. Note also that the direct output of the corecursive function does not simply contain the factorial <math>n!</math> 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.

Note the connection with [[denotational semantics]], where the [[Denotational semantics#Denotations of recursive programs|denotations of recursive programs]] is built up corecursively in this way.

In Python, a recursive factorial function can be defined as:{{efn|Not validating input data.}}
<syntaxhighlight lang=python>
def factorial(n):
    if n == 0:
        return 1
    else:
        return n * factorial(n - 1)
</syntaxhighlight>
This could then be called for example as <code>factorial(5)</code> to compute ''5!''.

A corresponding corecursive generator can be defined as:
<syntaxhighlight lang=python>
def factorials():
    n, f = 0, 1
    while True:
        yield f
        n, f = n + 1, f * (n + 1)
</syntaxhighlight>
This generates an infinite stream of factorials in order; a finite portion of it can be produced by:
<syntaxhighlight lang=python>
def n_factorials(k):
    n, f = 0, 1
    while n <= k:
        yield f
        n, f = n + 1, f * (n + 1)
</syntaxhighlight>
This could then be called to produce the factorials up to ''5!'' via:
<syntaxhighlight lang=python>
for f in n_factorials(5):
    print(f)
</syntaxhighlight>
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,
<syntaxhighlight lang=python>
def nth_factorial(k):
    n, f = 0, 1
    while n < k:
        n, f = n + 1, f * (n + 1)
    yield f
</syntaxhighlight>
As can be readily seen here, this is practically equivalent (just by substituting <code>return</code> for the only <code>yield</code> 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:
:<math>a, b = (0, 1) : (b, a+b)</math>
Note that because the Fibonacci sequence is a [[recurrence relation]] of order 2, the corecursive relation must track two successive terms, with the <math>(b, -)</math> corresponding to shift forward by one step, and the <math>(-, a+b)</math> corresponding to computing the next term. This can then be implemented as follows (using [[parallel assignment]]):
<syntaxhighlight lang=python>
def fibonacci_sequence():
    a, b = 0, 1
    while True:
        yield a
        a, b = b, a + b
</syntaxhighlight>
In Haskell, <syntaxhighlight lang=haskell> map fst ( (\(a,b) -> (b,a+b)) `iterate` (0,1) )</syntaxhighlight>

=== 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.{{efn|More elegantly, one can start by placing the root node itself in the structure and then iterating.}} If the data structure is a [[Stack (abstract data type)|stack]] (LIFO), this yields depth-first traversal, while if the data structure is a [[Queue (abstract data type)|queue]] (FIFO), this yields breadth-first traversal.

Using recursion, a (post-order){{efn|Post-order is to make "leaf node is base case" explicit for exposition, but the same analysis works for pre-order or in-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,{{efn|Breadth-first traversal, unlike depth-first, is unambiguous, and visits a node value before processing children.}} 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.{{efn|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.}} 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,{{efn|Assume fixed [[branching factor]] (e.g., binary), or at least bounded, and balanced (infinite in every direction).}} 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.{{efn|First defining a tree class, say via:
<syntaxhighlight lang=python>
class Tree:
    def __init__(self, value, left=None, right=None):
        self.value = value
        self.left  = left
        self.right = right

    def __str__(self):
        return str(self.value)
</syntaxhighlight>
and initializing a tree, say via:
<syntaxhighlight lang=python>
t = Tree(1, Tree(2, Tree(4), Tree(5)), Tree(3, Tree(6), Tree(7)))
</syntaxhighlight>
In this example nodes are labeled in breadth-first order:
     1
  2     3
 4 5   6 7
}}
The usual post-order depth-first traversal can be defined as:{{efn|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.}}
<syntaxhighlight lang=python>
def df(node):
    if node is not None:
        df(node.left)
        df(node.right)
        print(node.value)
</syntaxhighlight>
This can then be called by <code>df(t)</code> 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:{{efn|1=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.}}
<syntaxhighlight lang=python>
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
</syntaxhighlight>
This can then be called to print the values of the nodes of the tree in breadth-first order:
<syntaxhighlight lang=python>
for i in bf(t):
    print(i)
</syntaxhighlight>

==Definition== 
[[Initial and terminal objects|Initial data type]]s can be defined as being the [[least fixpoint]] ([[up to isomorphism]]) of some type equation; the [[isomorphism]] is then given by an [[Initial algebra|initial]] [[F-algebra|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 [[F-coalgebra|coalgebra]].

If the domain of discourse is the [[category of sets]] and total functions, then final data types may contain infinite, [[Non-well-founded set theory|non-wellfounded]] values, whereas initial types do not.<ref>Barwise and Moss 1996.</ref><ref>Moss and Danner 1997.</ref> On the other hand, if the domain of discourse is the category of [[complete partial order]]s and [[Scott continuity|continuous functions]], which corresponds roughly to the [[Haskell (programming language)|Haskell]] programming language, then final types coincide with initial types, and the corresponding final coalgebra and initial algebra form an isomorphism.<ref>Smyth and Plotkin 1982.</ref>

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.<ref>Gibbons and Hutton 2005.</ref><!--G&H ascribe this definition to Barwise and Moss-->

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.<ref>Doets and van Eijck 2004.</ref> 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 (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=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)
</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 linear time:

<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 = 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  
</syntaxhighlight>

This definition takes an initial tree and produces a list of subtrees.   This list serves dual purpose as both the queue and the result (<small>''<code>gen len p</code>''</small> produces its output <small>''<code>len</code>''</small> notches after its input back-pointer, <small>''<code>p</code>''</small>, along the <small>''<code>queue</code>''</small>).  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: the Haskell code can be translated into Prolog quite straightforwardly. Prolog is not a lazy language. But it does have tail recursion modulo cons. Which is emulatable in Scheme, C, etc.

bftrav(Tree,Q):- Q=[Tree|R], bfgen(1,Q,R).
bfgen(0,_,[]):- !.
bfgen(N,[leaf(_)        |P], R       ):- N2 is N-1, bfgen(N2,P,R).
bfgen(N,[branch(_,Lt,Rt)|P],[Lt,Rt|R]):- N2 is N+1, bfgen(N2,P,R).
-->

Another particularly good 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 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.

<syntaxhighlight lang=haskell>
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′
</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]] proof assistant supports corecursion and [[coinduction]] using the CoFixpoint command.

== 历史 ==
Corecursion, referred to as ''circular programming,'' dates at least to {{Harv|Bird|1984}}, who credits [[John Hughes (computer scientist)|John Hughes]] and [[Philip Wadler]]; more general forms were developed in {{Harv|Allison|1989}}. The original motivations included 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.
{{transF}}

== 参见 ==
* {{tsl|en|Bisimulation|}}
* {{tsl|en|Coinduction|余归纳}}
* [[递归]]
* {{tsl|en|Anamorphism|}}

== 注释==
{{notelist}}

== 参考文献==
{{Reflist|2}}
{{refbegin}}
* {{Cite journal | last = Bird | first = Richard Simpson | authorlink = Richard Bird (computer scientist)| title = Using circular programs to eliminate multiple traversals of data | url = https://archive.org/details/sim_acta-informatica_1984-10_21_3/page/239 | doi = 10.1007/BF00264249 | journal = Acta Informatica | volume = 21 | issue = 3 | pages = 239–250 | year = 1984 | pmid =  | pmc = }}
* {{cite journal
| doi = 10.1002/spe.4380190202
| author = Lloyd Allison
| date = April 1989
| title = Circular Programs and Self-Referential Structures
| url = http://www.csse.monash.edu.au/~lloyd/tildeFP/1989SPE/
| journal = Software Practice and Experience
| volume = 19
| issue = 2
| pages = 99–109
| access-date = 2017-12-01
| archive-date = 2009-07-21
| archive-url = https://web.archive.org/web/20090721012510/http://www.csse.monash.edu.au/~lloyd/tildeFP/1989SPE/
| dead-url = no
}}
* {{cite techreport
| author = Geraint Jones and [[Jeremy Gibbons]]
| title = Linear-time breadth-first tree algorithms: An exercise in the arithmetic of folds and zips
| institution = Dept of Computer Science, University of Auckland
| year = 1992
| url = http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.5446
| access-date = 2017-12-01
| archive-date = 2012-10-06
| archive-url = https://web.archive.org/web/20121006013907/http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.5446
| dead-url = no
}}
* {{cite book |author1=[[Jon Barwise]] |author2=Lawrence S Moss |title=Vicious Circles |url=http://www.press.uchicago.edu/presssite/metadata.epl?mode=synopsis&bookkey=3630257 |publisher=Center for the Study of Language and Information |date=June 1996 |isbn=978-1-57586-009-1 |deadurl=yes |archiveurl=https://web.archive.org/web/20100621142601/http://www.press.uchicago.edu/presssite/metadata.epl?mode=synopsis&bookkey=3630257 |archivedate=2010年6月21日 |df= |access-date=2017年12月1日 }}
* {{cite journal
 |doi          = 10.1093/jigpal/5.2.231
 |author1      = Lawrence S Moss
 |author2      = Norman Danner
 |title        = On the Foundations of Corecursion
 |url          = http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.4243
 |journal      = Logic Journal of the IGPL
 |volume       = 5
 |issue        = 2
 |pages        = 231–257
 |year         = 1997
 |access-date  = 2017-12-01
 |archive-date = 2012-10-15
 |archive-url  = https://web.archive.org/web/20121015132704/http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.4243
 |dead-url     = no
}}
* {{cite book |author1=Kees Doets |author2=Jan van Eijck |title=The Haskell Road to Logic, Maths, and Programming |url=http://homepages.cwi.nl/~jve/HR/ |publisher=King's College Publications |date=May 2004 |isbn=978-0-9543006-9-2 |access-date=2017-12-01 |archive-date=2019-05-11 |archive-url=https://web.archive.org/web/20190511110751/https://homepages.cwi.nl/~jve/HR/ |dead-url=no }}
* {{cite journal
| author = David Turner
| date = 2004-07-28
| title = Total Functional Programming
| url = http://www.jucs.org/jucs_10_7/total_functional_programming
| journal = Journal of Universal Computer Science
| volume = 10
| issue = 7
| pages = 751–768
| doi = 10.3217/jucs-010-07-0751
| authorlink = David Turner (computer scientist)
| access-date = 2017-12-01
| archive-date = 2020-11-14
| archive-url = https://web.archive.org/web/20201114001344/http://www.jucs.org/jucs_10_7/total_functional_programming
| dead-url = no
}}
* {{cite journal
 |author1      = Jeremy Gibbons
 |author2      = Graham Hutton
 |title        = Proof methods for corecursive programs
 |journal      = Fundamenta Informaticae Special Issue on Program Transformation
 |volume       = 66
 |issue        = 4
 |pages        = 353–366
 |date         = April 2005
 |url          = http://www.cs.nott.ac.uk/~gmh/bib.html#corecursion
 |access-date  = 2017-12-01
 |archive-date = 2015-09-09
 |archive-url  = https://web.archive.org/web/20150909202739/http://www.cs.nott.ac.uk/~gmh/bib.html#corecursion
 |dead-url     = no
}}
* {{citation
| author = Leon P Smith
| date = 2009-07-29
| title = Lloyd Allison's Corecursive Queues:  Why Continuations Matter
| url = http://themonadreader.wordpress.com/2009/07/29/issue-14/
| journal = The Monad Reader
| issue = 14
| pages = 37–68
| accessdate = 2017-12-01
| archive-date = 2020-08-14
| archive-url = https://web.archive.org/web/20200814175546/https://themonadreader.wordpress.com/2009/07/29/issue-14/
| dead-url = no
}}
* {{cite web
| author = Raymond Hettinger
| title = Recipe 576961: Technique for cyclical iteration
| url = http://code.activestate.com/recipes/576961/
| date = 2009-11-19
| accessdate = 2017-12-01
| archive-date = 2009-11-25
| archive-url = https://web.archive.org/web/20091125231711/http://code.activestate.com/recipes/576961/
| dead-url = no
}}
* {{cite journal
| author = M. B. Smyth and [[Gordon Plotkin|G. D. Plotkin]]
| year = 1982
| title = The Category-Theoretic Solution of Recursive Domain Equations
| journal = [[SIAM Journal on Computing]]
| volume = 11
| issue = 4
| pages = 761–783
| doi = 10.1137/0211062
}}
* {{cite book
|author1=Leclerc, Francois  |author2=Paulin-Mohring, Christine
| title = Programming with Streams in Coq: A Case Study: the Sieve of Eratosthenes
| series = Types for Proofs and Programs: International Workshop TYPES '93. 
| year = 1993
| isbn = 3-540-58085-9
| pages = 191–212
| url = http://dl.acm.org/citation.cfm?id=189973.189981
| publisher = Springer-Verlag New York, Inc.
}}
{{refend}}
[[Category:范畴论]]
[[Category:递归论]]
[[Category:递归]]