Coinduction is a method of proof which relies on the fact that any two states of the terminal coalgebra for an endofunctor HH must be equal if they are indistinguishable under repeated operations of HH. That is, there are no proper coalgebra quotient objects. Generally, we show the existence of a bisimulation between states of terminal coalgebra, that is a relation between states, such that when the coalgebra function is applied, the respective outputs are still related. Since any bisimulation must be contained within the identity relation, we can then conclude that the states are equal.

Coinduction is dual to induction. It generalises to corecursion.


Take add:¯×¯1+¯×¯add\colon \bar{\mathbb{N}} \times \bar{\mathbb{N}} \to 1 + \bar{\mathbb{N}} \times \bar{\mathbb{N}} as defined at corecursion, which defines an addition ++ on the extended natural numbers. We can then establish a bisimulation between the terms (n+m)(n + m) and (m+n)(m + n), from which we can conclude that this addition is commutative. (See p. 52 of Rutten Universal coalgebra: a theory of systems.)


  • Bart Jacobs, Jan Rutten, A tutorial on (Co)Algebras and (Co)Induction (pdf)

  • Davide Sangiorgi, Introduction to Bisimulation and Coinduction, Cambridge Universtity Press (2012) (web)

  • Davide Sangiorgi, Jan Rutten (eds.), Advanced Topics in Bisimulation and Coinduction, Cambridge Universtity Press (2012) (web)

Discussion of differential calculus in terms of coinduction is in

  • Martin Escardo, Duško Pavlović, Calculus in coinductive form (1998) (pdf)

Revised on April 22, 2015 06:42:50 by Tim Porter (