nLab
corecursion
Corecursion
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
For the endofunctor H ( X ) = 1 + X H(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 ) if n > 0 ; ( 0 , pred ( m ) ) if n = 0 , m > 0 ; * if m = 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 H 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 > 0 n + m \gt 0 with pred ( n + m ) = pred ( n ) + m pred(n + m) = pred(n) + m if n > 0 n \gt 0 ,
n + m > 0 n + m \gt 0 with pred ( n + m ) = 0 + pred ( m ) pred(n + m) = 0 + pred(m) if n = 0 n = 0 and m > 0 m \gt 0 ,
n + m = 0 n + m = 0 if n = 0 n = 0 and m = 0 m = 0 .
(From the last two, it’s immediate to prove by coinduction that 0 + m = m 0 + m = m for all m m .)
Reference
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.