David Corfield Induction & Coinduction

From Jacobs and Rutten A Tutorial on (Co)Algebras and (Co)Induction

Induction uses initiality of algebras. Initiality involves unique existence. Existence allows definition by induction. Uniqueness allows proof by induction.

Initial algebras are obtained from closed terms, generated by iteratively applying the algebra’s constructor operations.

Coalgebras relate to observation/destruction.

For induction, show that property hold for atomic terms, and then if for a term, also for operation acting on it. No subalgebras of initial algebra.

Coalgebraically, take machine which changes unknown state when a button is pressed repeatedly until light comes on. Observe number of times until light comes on {never, 0, 1,…}.

In an induction definition of a function $f$, one defines the values of $f$ on all constructors.

In a coinductive definition of a function $f$, one defines the values of all destructors on each outcome $f(x)$.

E.g, for lists of elements of $A$, algebras of $X \mapsto A \times X$, define

• $len(nil) = 0, len(cons(a, \sigma)) = 1 + len(\sigma)$
• $empty?(nil) = true, empty?(cons(a, \sigma)) = false$.

Constructors appear inside the function.

Define $ext(f)$ for $f$ applied to infinite list of $A$ elementwise, so give values of destructors

$head(ext(f)(\sigma)) = f(head(\sigma))$

$tail(ext(f)(\sigma)) = ext(f)(tail(\sigma))$

Function appears inside the destructors.

Another important point, not clear from the examples above, is that one naturally defines maps from an initial algebra or to a final coalgebra. (In particular, given an endofunctor $F$, there is a map from its initial algebra to its final coalgebra.)