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 ff, one defines the values of ff on all constructors.

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

E.g, for lists of elements of AA, algebras of XA×XX \mapsto A \times X, define

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

Constructors appear inside the function.

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

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

tail(ext(f)(σ))=ext(f)(tail(σ))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 FF, there is a map from its initial algebra to its final coalgebra.)

Last revised on May 1, 2009 at 21:51:26. See the history of this page for a list of all contributions to it.