nLab corecursion




Corecursion exploits the existence of a morphism from a coalgebra for an endofunctor to a terminal coalgebra for the same endofunctor to define an operation. It is dual to recursion. See also coinduction.


  1. For the endofunctor H(X)=1+XH(X) = 1 + X on Set, the terminal coalgebra is ¯\bar{\mathbb{N}}, the extended natural number system. Define a function add:¯×¯1+¯×¯add\colon \bar{\mathbb{N}} \times \bar{\mathbb{N}} \to 1 + \bar{\mathbb{N}} \times \bar{\mathbb{N}}:

    add(n,m)={(pred(n),m) ifn>0; (0,pred(m)) ifn=0,m>0; * ifm=n=0, add(n, m) = \begin{cases} (pred(n), m) & if\; n \gt 0; \\ (0, pred(m)) & if\; n = 0,\; m \gt 0; \\ * & if\; m = n = 0, \end{cases}

    where pred(x)pred(x) is as defined at extended natural number.

    Then (¯×¯,add)(\bar{\mathbb{N}} \times \bar{\mathbb{N}}, add) is an HH-coalgebra. The unique coalgebra morphism +:¯×¯¯{+}\colon \bar{\mathbb{N}} \times \bar{\mathbb{N}} \to \bar{\mathbb{N}} (to the terminal coalgebra ¯\bar{\mathbb{N}}) is addition on the extended natural numbers. From this definition, we may read off these basic facts about ++:

  • n+m>0n + m \gt 0 with pred(n+m)=pred(n)+mpred(n + m) = pred(n) + m if n>0n \gt 0,
  • n+m>0n + m \gt 0 with pred(n+m)=0+pred(m)pred(n + m) = 0 + pred(m) if n=0n = 0 and m>0m \gt 0,
  • n+m=0n + m = 0 if n=0n = 0 and m=0m = 0.

(From the last two, it’s immediate to prove by coinduction that 0+m=m0 + m = m for all mm.)


  • Jiří Adámek, Introduction to Coalgebra (pdf)

  • Lawrence Moss, Norman Danner, On the Foundations of Corecursion (journal, pdf)

Last revised on July 21, 2021 at 14:03:24. See the history of this page for a list of all contributions to it.