Coalgebra
While induction is widespread and we employ it without a second thought, coinduction (Rutten, 2005) is not granted the same trust: every time we employ coinduction, we reassert its validity from basic principles. This makes coinduction look obscure and awkward. Instead, we can reason coinductively in the practical style promoted by Kozen and Silva: we apply coinductive hypotheses that need a coinductive step but not a base case. This is not to mean our reasoning is not formal: it is backed by formal principles the same way induction is.
Coalgebra is used to describe operational semantics. Applications of coalgebra include stream transducers, cellular automata, mathematical analysis or data containers.
- Comonad
- Comonads on a cartesian are monoidal
- Parameterised comonads
- machines and streams
- Coinductive cellular automata
- coalgebra of the real interval
- coalgebraic physics
- graded coalgebra
- graded comonoid
- Adamek’s theorem
References