nLab coinduction




Coinduction is dual to induction. It generalises to corecursion.

It 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.



Let ¯\bar{\mathbb{N}} be the set of conatural numbers and take add:¯×¯1+¯×¯add\colon \bar{\mathbb{N}} \times \bar{\mathbb{N}} \to 1 + \bar{\mathbb{N}} \times \bar{\mathbb{N}}. 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.)


Many theorems of calculus involving formal power series f(x)= n0a nx nn!f(x) = \sum_{n \geq 0} \frac{a_n x^n}{n!} are naturally viewed as proofs by coinduction. The collection of power series k[[x]]k[ [x] ] over a field kk (say of characteristic 00) may be viewed as a stream coalgebra k k^\mathbb{N}, i.e., the terminal coalgebra of the endofunctor k×:SetSetk \times -:\; Set \to Set, with the coalgebra structure

eval 0,D=ddx:k[[x]] k×k[[x]] n0a nx nn! (a 0, n0a n+1x nn!)\array{ \langle eval_0, D = \frac{d}{d x} \rangle: k[ [x] ] & \to & k \times k[ [x] ] \\ \sum_{n \geq 0} \frac{a_n x^n}{n!} & \mapsto & (a_0, \sum_{n \geq 0} \frac{a_{n+1} x^n}{n!}) }

Thus if we set up a bisimulation \sim between two power series f,gf, g, establishing f(0)=g(0)f(0) = g(0) and (Df)(Dg)(D f) \sim (D g), we may conclude by coinduction that f=gf = g (else, k[[x]]/k[ [x] ]/\sim would be a proper quotient).

As an illustration: consider a field kk of characteristic 00 and, for rkr \in k, define (1+x) r(1 + x)^r to be the power series expansion of exp(rlog(1+x))\exp(r \cdot \log(1 + x)), where exp(x)= n0x nn!\exp(x) = \sum_{n \geq 0} \frac{x^n}{n!} and log(1+x)= n1(1) n+1x nn\log(1 + x) = \sum_{n \geq 1} (-1)^{n+1}\; \frac{x^n}{n} is the inverse of exp(x)1\exp(x)-1. To prove the generalized binomial theorem

(1+x) r=f(r) k0r k̲x kk!(1 + x)^r = f(r) \coloneqq \sum_{k \geq 0} \frac{r^\underline{k} x^k}{k!}

where r k̲r^\underline{k} is the falling power r(r1)(rk+1)r(r-1)\ldots (r-k+1), we introduce a bisimilarity

k0r k̲x kk!exp(rlog(1+x))\sum_{k \geq 0} \frac{r^\underline{k} x^k}{k!}\; \sim\; \exp(r \cdot \log(1 + x))

and observe first that the constant coefficients of f(x)f(x) and (1+x) r(1+x)^r are both 11, and that

D( k0r k̲x kk!)=r k0(r1) k̲x kk!D\left(\sum_{k \geq 0} \frac{r^\underline{k} x^k}{k!}\right) = r \sum_{k \geq 0} \frac{(r-1)^\underline{k} x^k}{k!}

(because r k+1̲=r(r1) k̲r^{\underline{k+1}} = r \cdot (r-1)^{\underline{k}}) and similarly

D(exp(rlog(1+x)))=rexp((r1)log(1+x))D\left(\exp(r \cdot \log(1 + x))\right) = r \cdot \exp((r-1) \cdot \log(1 + x))

by the chain rule, whence D(f/r)D((1+x) r/r)D(f/r) \sim D((1+x)^r/r). Hence f/rf/r is bisimilar to (1+x) r/r(1+x)^r/r, and we conclude in the terminal coalgebra that f(x)=(1+x) rf(x) = (1+x)^r.

See also


  • 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) (web or pdf)

About coinduction in cubical type theory:

Last revised on December 16, 2023 at 10:14:12. See the history of this page for a list of all contributions to it.