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 $\bar{\mathbb{N}}$, the extended natural number system. Define a function $add\colon \bar{\mathbb{N}} \times \bar{\mathbb{N}} \to 1 + \bar{\mathbb{N}} \times \bar{\mathbb{N}}$:

   $$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)$ is as defined at extended natural number.

   Then $(\bar{\mathbb{N}} \times \bar{\mathbb{N}}, add)$ is an $H$-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 \gt 0$ with $pred(n + m) = pred(n) + m$ if $n \gt 0$,
• $n + m \gt 0$ with $pred(n + m) = 0 + pred(m)$ if $n = 0$ and $m \gt 0$,
• $n + m = 0$ if $n = 0$ and $m = 0$.

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

Reference

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

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