Corecursion

Not to be confused with Mutual recursion.

In computer science, corecursion is a type of operation that is dual to (structural) recursion. Whereas recursion consumes a data structure by first handling the topmost layer before descending into its inner parts, corecursion produces a data structure by first defining the topmost layer before defining its inner parts. Corecursion is a particularly important in total languages, as it allows encoding potentially non-terminating computations in a context where every function must terminate. It is supported by theorem provers Agda ^[1] and Rocq ^[2] .

Both corecursion and recursion can be thought of as operating on trees, which include data structures like lists and streams as special cases. Since recursion must terminate, it only works on trees that are well-founded, i.e. not infinitely deep, which are called data or initial data types; on the other hand, corecursion produces codata or final data types, which includes infinitely deep trees. Codata cannot be represented in memory directly, so is often implemented using self-referential data structures or lazy evaluation.

Data and codata

In total programming languages, the natural numbers may be defined as follows (using Haskell syntax ^[a] ):

dataNat=Zero|SuccNat

This states that every natural number is either zero or the successor of an existing natural number. For example, the number one is represented as Succ Zero, two as Succ (Succ Zero), three as Succ (Succ (Succ Zero)) and so on.

If we interpret the above declaration in an inductive way, then all natural numbers are generated like this, and we get our familiar set of natural numbers. Importantly, we can do recursion ^[b] on this set: for example, we can use it to make a list that repeats a value n times:

repeat::a->Nat->[x]repeatxZero=[]-- Base caserepeatx(Succn)=x:recursiven-- Inductive step

Note that the use of recursive n is crucial—we could not have written recursive (Succ n), because that is the function we are trying to define, and therefore it would loop forever. More specifically, the input must get smaller—or rather deeper, if seen as a data structure—each time we recurse.

The declaration may also be interpreted in a coinductive way, which may be denoted as:

codataCoNat=Zero|SuccCoNat

CoNat has all the natural numbers that Nat has automatically. But because codata can be infinitely deep, it has an extra term Succ (Succ (Succ (Succ …))) that continues on indefinitely—often denoted ∞. ^[3] This is unique to the conatural numbers, so it can only be constructed using corecursion:

infinity::CoNatinfinity=Succinfinity

While recursion requires that the input of the recursive call must get smaller each time, corecursion requires that the output of the recursive call must get larger each time. This is why we must write Succ infinity; just infinity = infinity would be disallowed as it loops forever.

To illustrate the duality between recursion and corecursion, we can encapsulate them in two functions, rec and corec. These functions' existence, together with the regular two constructors of Nat and CoNat, uniquely identify their respective types, and therefore allow rewriting all forms of recursion and corecursion in terms of them. ^[4]

rec::Nat->(Maybec->c)->crecZerof=fNothingrec(Succn)f=f(Just(recnf))corec::(c->Maybec)->c->CoNatcorecfbase=casefbaseofNothing->ZeroJustx->Succ(corecfx)

Conceptually, CoNat can be thought of as a state machine, where c is a type encapsulating the "current state". The function c -> Maybe c is a state transition function that either results in termination with Zero or continuation with Succ. We can rewrite the examples above using the functions:

repeatxn=recn(\s->casesofNothing->[]Justa->x:a)infinity=corec(\()->Just())()

A more complex example of codata is that of binary trees, where each node is either a leaf node, holding some data, or is a branch node that has exactly two children:

codataBinaryTreea=Leafa|Branch(BinaryTreea)(BinaryTreea)

This example has many more infinitely deep terms that can only be constructed by corecursion. For example, it can be infinitely deep only on the left-hand side, or on both sides, or alternating left and right:

infiniteLeft::a->BinaryTreeainfiniteLeftx=Branch(infiniteLeftx)(Leafx)infiniteBoth::BinaryTreeainfiniteBoth=BranchinfiniteBothinfiniteBothinfiniteAlternating::a->Bool->BinaryTreeainfiniteAlternatingxFalse=Branch(infiniteAlternatingxTrue)(Leafx)infiniteAlternatingxTrue=Branch(Leafx)(infiniteAlternatingxFalse)

Again, corecursion on binary trees has a more general form based on a "state machine"-like constructor:

corec::(c->Eithera(c,c))->c->BinaryTreeacorecfbase=casefbaseofLeftx->LeafxRight(x,y)->Branch(corecfx)(corecfy)

M-types

In a dependently-typed setting, codata can be encoded using M-types, which are dual to W-types. Given a type A and an A-indexed family of types B, one can form the M-type ${\displaystyle {\mathsf {M}}_{a:A}B(a)}$, representing the type of trees whose nodes are labelled with elements of A and who child nodes are indexed by the set B(a). In pseudocode, M-types (and their corecursion principle) may be defined as:

codataMa(b::a->*)=M{root::a,branch::broot->Mab}corec::(c->(root::a,broot->c))->c->Mabcorecfbase=let(root,branch)=fbaseinM{root=root,branch=\i->corecf(branchi)}

As an example, the natural and conatural numbers may be constructed as W- and M-types of the same function:

f::Bool->*fFalse=Void-- Zero case (no branches)fTrue=()-- Succ case (one branch)Nat=WBoolfCoNat=MBoolf

M-types can be proven to exist in many elementary topoi, and their existence follows from the existence of W-types. ^[5]

Mathematical description

The above section showed that there is an intimate link between natural and conatural numbers and Maybe c, and similarly between binary trees and Either a (c, c). This link is made precise by showing that Nat is in bijection with Maybe Nat, and CoNat with Maybe CoNat; explicitly, this bjiection associates Zero with Nothing and Succ n with Just n. In other words, Nat and CoNat are fixed points (up to isomorphism) of the map ${\displaystyle X\mapsto X+1}$.

The difference between data and codata is that data is the least such fixed point, while codata is the greatest. In this way, recursion can be summarized as the statement that "every element of the type was generated only by the given constructors (Zero and Succ in the case of Nat/CoNat)", while corecursion states that "every value that can be analysed using the constructors as cases exists".

From a category-theoretic perspective, CoNat can be precisely defined as the final coalgebra of the endofunctor ${\displaystyle X\mapsto X+1}$. ^[4] Unfolding this definition, we have that:

• There is a function pred :: CoNat -> Maybe CoNat. "Pred" stands for "predecessor", and the intuition is that it subtracts one from the conatural number or gives Nothing otherwise. In other words, pred Zero = Nothing and pred (Succ n) = Just n. This shows that CoNat is a coalgebra of the functor, but not necessarily the final one.
• For every type c and function f :: c -> Maybe c, there is a function corec f :: c -> CoNat such that pred (corec f x) = fmap (corec f) (f x).
  
  Breaking this down futher, if f x = Just y then corec f x = Succ (corec f y), while if f x = Nothing then corec f x = Zero—this matches the definition of corec we are familiar with.
• corec is unique in the following sense: for any other function g :: c -> CoNat that also satisfies pred (g x) = fmap g (f x), g x = corec f x. This ensures that CoNat is a final coalgebra.

Maybe c can be replaced with any other functor in the above description to obtain the definition of any other coinductive type.

Not all functors have final coalgebras. For example, Cantor's theorem tells us that no set can be in bijection with its powerset, and therefore the powerset functor a -> Bool has no final coalgebra. However, in the case of polynomial functors or quotient polynomial functors ^[6] , final coalgebras always exist; polynomial functors are functors that can be expressed in the form ${\displaystyle \textstyle X\mapsto \sum _{a:\alpha }X^{\beta (a)}}$ for a type α and α-indexed type family β(a). The M-type is exactly the construction of this final coalgebra. ^[5]

Coinduction

While one can reason about coinductive data types using the uniqueness of corec directly, it is often more convenient to use coinduction, which can prove equalities of codata. Given a final coalgebra A of a polynomial functor F—i.e. ${\displaystyle \textstyle F(X)=\sum _{a:\alpha }X^{\beta (a)}}$— we say that a relation ${\displaystyle R\subseteq A\times A}$ is a bisimulation if, for all ${\displaystyle (a,b)\in R}$, ${\displaystyle {\text{root}}(a)={\text{root}}(b)}$ and ${\displaystyle {\text{branch}}(a,i)R{\text{branch}}(b,i)}$ for all ${\displaystyle i:B({\text{root}}(a))}$. Here, ${\displaystyle {\text{root}}}$ and ${\displaystyle {\text{branch}}}$ refer to the maps:

${\displaystyle {\begin{aligned}{\text{root}}&:A\rightarrow \alpha \\{\text{branch}}&:\prod _{a:A}\beta ({\text{root}}(a))\rightarrow A\end{aligned}}}$

The principle of coinduction states that for all bisimulations R on A and ${\displaystyle (a,b)\in R}$, ${\displaystyle a=b}$.

More generally, for a coalgebra map ${\displaystyle {\text{get}}:A\rightarrow F(A)}$, a relation R on A is a bisimulation if there exists a function ${\displaystyle f:R\rightarrow F(R)}$ satisfying, for all ${\displaystyle (a,b)\in R}$,

• ${\displaystyle {\text{get}}(a)=F(\pi _{1})(f(a,b))}$ and
• ${\displaystyle {\text{get}}(b)=F(\pi _{2})(f(a,b))}$,

where π₁ and π₂ are the first and second projection maps ${\displaystyle R\rightarrow A}$. It can be seen this equivalent to the polynomial case by setting ${\displaystyle f(a,b)=({\text{root}}(a),i\mapsto ({\text{branch}}(a,i),{\text{branch}}(b,i)))}$. The required equalities can also be expressed as a commutative diagram:

Coinduction is easy to prove from the uniqueness of corec: π₁ and π₂ both satisfy the required property to be equal to corec f, and are therefore equal to each other, thus showing that ${\displaystyle a=\pi _{1}(a,b)=\pi _{2}(a,b)=b}$. ^[4]

Example: Conatural number addition

To demonstrate the usage of coinduction, we will prove some basic properties about addition on conatural numbers. Addition can be defined identically to how it is defined for natural numbers: ^[3]

add::CoNat->CoNat->CoNataddaZero=aadda(Succb)=Succ(addab)

This definition, while valid, hides some amount of complexity. We may alternatively write:

addZeroZero=Zeroadd(Succa)Zero=Succ(addaZero)adda(Succb)=Succ(addab)

This definition makes the translation to corec straightforward:

iterate::(CoNat,CoNat)->Maybe(CoNat,CoNat)iterateZeroZero=Nothingiterate(Succa)Zero=Just(a,Zero)iteratea(Succb)=Just(a,b)addab=coreciterate(a,b)

We can prove that ${\displaystyle a+0=a}$ by coinduction on the relation ${\displaystyle \{(a+0,a)|a\in \mathbb {N} ^{\infty }\}}$ (where ${\displaystyle \mathbb {N} ^{\infty }}$ is the set of conatural numbers). First, it follows from the definition of addition that ${\displaystyle a+0=0\iff a=0}$; second, if we assume that ${\displaystyle (x+1,y+1)}$ is of the form ${\displaystyle (a+0,a)}$ for some a, we must show that ${\displaystyle (x,y)}$ is also of this form. We have: $${\displaystyle x+1=a+0=(y+1)+0=(y+0)+1}$$Thus ${\displaystyle x=y+0}$, and therefore ${\displaystyle (x,y)=(y+0,y)}$ as required.

The identity ${\displaystyle (a+1)+b=(a+b)+1}$ may be similarly proven by coinduction on ${\displaystyle \{(((a+1)+b)-1,a+b)|a,b\in \mathbb {N} ^{\infty }\}}$ (remember the relation must necessarily include ${\displaystyle (0,0)}$); finally, commutativity—${\displaystyle a+b=b+a}$—results from similar straightforward coinduction on ${\displaystyle \{(a+b,b+a)|a,b\in \mathbb {N} ^{\infty }\}}$. ^[7]

In programming languages

If the domain of discourse is the category of sets and total functions (such as in theorem provers like Agda and Rocq), then final types (codata) may contain infinite, non-wellfounded values, whereas initial types (data) do not. ^{[8] [9]} 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. ^[10]

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

• Bisimulation
• Coinduction
• Recursion
• Anamorphism

Notes

1. Haskell, being a partial and lazy language, does not support either data or codata; we use its syntax for familiarity.
2. "Recursion" here is used in the technical sense of structural recursion, which is a type of recursion that analyses the structure of a type and always terminates. In the more general sense of the word used in computer science, corecursion is also a type of recursion.

References

1. Agda Authors. "Coinduction". Agda 2.8.0 documentation. Archived from the original on 2026-02-18. Retrieved 2026-03-13.
2. Inria, CNRS and contributors. "Coinductive types and corecursive functions". The Rocq Prover 9.1.0 documentation. Retrieved 2026-03-13.
3. Xie, Szumi; Bense, Viktor (2025-10-09). "The Conatural Numbers Form an Exponential Commutative Semiring". Proceedings of the 10th ACM SIGPLAN International Workshop on Type-Driven Development. TyDe '25. New York, NY, USA: Association for Computing Machinery: 52–63. doi:10.1145/3759538.3759654. ISBN   979-8-4007-2163-2.
4. Jacobs, Bart; Rutten, Jan (2011), "An introduction to (co)algebra and (co)induction", in Sangiorgi, Davide; Rutten, Jan (eds.), Advanced Topics in Bisimulation and Coinduction, Cambridge Tracts in Theoretical Computer Science, Cambridge: Cambridge University Press, pp. 38–99, doi:10.1017/CBO9780511792588.003, ISBN   978-1-107-00497-9 , retrieved 2026-03-14
5. van den Berg, Benno; De Marchi, Federico (2007-04-01). "Non-well-founded trees in categories". Annals of Pure and Applied Logic. 146 (1): 40–59. doi:10.1016/j.apal.2006.12.001. ISSN   0168-0072.
6. Avigad, Jeremy; Carneiro, Mario; Hudon, Simon (2019). Harrison, John; O'Leary, John; Tolmach, Andrew (eds.). "Data Types as Quotients of Polynomial Functors". 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs). 141. Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik: 6:1–6:19. doi: 10.4230/LIPIcs.ITP.2019.6 . ISBN   978-3-95977-122-1.
7. Rutten, J. J. M. M. (2000-10-17). "Universal coalgebra: a theory of systems". Theoretical Computer Science. Modern Algebra. 249 (1): 3–80. doi: 10.1016/S0304-3975(00)00056-6 . ISSN   0304-3975.
8. Barwise and Moss 1996.
9. Moss and Danner 1997.
10. Smyth and Plotkin 1982.

• Bird, Richard Simpson (1984). "Using circular programs to eliminate multiple traversals of data". Acta Informatica . 21 (3): 239–250. doi:10.1007/BF00264249. S2CID   27392591.
• Allison, Lloyd (April 1989). "Circular Programs and Self-Referential Structures". Software: Practice and Experience. 19 (2): 99–109. arXiv: 2403.01866 . doi:10.1002/spe.4380190202. S2CID   21298473.
• 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; Lawrence S. Moss (June 1996). Vicious Circles. Center for the Study of Language and Information. ISBN   978-1-57586-009-1. Archived from the original on 2010-06-21. Retrieved 2011-01-24.
• Lawrence S. Moss; Norman Danner (1997). "On the Foundations of Corecursion". Logic Journal of the IGPL. 5 (2): 231–257. CiteSeerX   10.1.1.40.4243 . doi:10.1093/jigpal/5.2.231.
• Kees Doets; Jan van Eijck (May 2004). The Haskell Road to Logic, Maths, and Programming. King's College Publications. ISBN   978-0-9543006-9-2.
• 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; Graham Hutton (April 2005). "Proof methods for corecursive programs". Fundamenta Informaticae . 66 (4): 353–366.
• 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" (PDF). SIAM Journal on Computing . 11 (4): 761–783. doi:10.1137/0211062. S2CID   8517995.
• Leclerc, Francois; Paulin-Mohring, Christine (1993). Programming with Streams in Coq: A Case Study: the Sieve of Eratosthenes. Types for Proofs and Programs: International Workshop TYPES '93. Springer-Verlag New York, Inc. pp. 191–212. ISBN   978-3-540-58085-0.