nLab
corecursion

Idea

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}(\mathrm{pred}(n),m)& \mathrm{if}n>0;\\ (0,\mathrm{pred}(m))& \mathrm{if}n=0,m>0;\\ *& \mathrm{if}m=n=0,\end{array}$$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 $\mathrm{pred}(x)$ is as defined at extended natural number.

   Then $(\overline{\mathbb{N}}\times \overline{\mathbb{N}},\mathrm{add})$ is an $H$-coalgebra. The unique coalgebra morphism $+:\overline{\mathbb{N}}\times \overline{\mathbb{N}}\to \overline{\mathbb{N}}$ (to the terminal coalgebra $\overline{\mathbb{N}}$) is addition on the extended natural numbers.

Reference

• Jiří Adámek, Introduction to Coalgebra