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.

Examples

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

$$\mathrm{add}(n,m)=\{\begin{array}{ll}(n-1,m)& \mathrm{if}n>0;\\ (0,m-1)& \mathrm{if}n=0,m>0;\\ *& \mathrm{if}m=n=0.\end{array}$$add(n, m) = \begin{cases} (n - 1, m) & if\; n \gt 0; \\ (0, m - 1) & if\; n = 0,\; m \gt 0; \\ * & if\; m = n = 0. \end{cases}

This makes $\overline{\mathbb{N}}\times \overline{\mathbb{N}}$ into an $H$-coalgebra. The unique arrow to the terminal coalgebra defines addition on the natural numbers extended with $\mathrm{\infty }$.

Reference

• Jiří Adámek, Introduction to Coalgebra