categories: Re: coinduction

[Jeremy Gibbons <Jeremy.Gibbons@comlab.ox.ac.uk>]

> can anyone explain coinduction?
> in what sense it dual to induction?

We've heard some very erudite answers to these questions. I
don't know the questioner's background, but here is a
different answer, in case it helps.

In the algebraic approach to functional programming, an
initial datatype of a functor F is a datatype T and an
operation in : F T -> T for which the equation in h

  h . in = f . F h

has a unique solution for given f. We write "fold_F f" for
that unique solution, so

  h = fold_F f  <=>  h . in = f . F h

This is an inductive definition of fold, and the above
equivalence (the "universal property for fold") encapsulates
proof by structural induction.

(For example, when F X = 1+X, then T is N, the naturals. The
injection in : 1+N->N is the coproduct morphism [0,1+].
Folds on naturals are functions of the form

  fold_{1+} [z,s] 0     = z
  fold_{1+} [z,s] (1+n) = s (fold_{1+} [z,s] n)

To prove that a predicate p holds for every natural n is
equivalent to proving that the function p : N -> Bool is
equal to the function alwaystrue : N -> Bool that always
returns true. Now alwaystrue is a fold,

  alwaystrue = fold_{1+} [true,step]
    where step true = true

Therefore, to prove that p holds for every natural, we can
use the universal property:

      predicate p holds of every natural
  <=>
      p = alwaystrue
  <=>
      p = fold_{1+} [true,step]
  <=>
      p . [0,1+] = [true,step] . id+p
  <=>
      p(0) = true  and  p(1+n) = step(p(n))
  <=>
      p(0) = true  and  (p(1+n) = true when p(n) = true)

which is the usual principle of mathematical induction.)

Dually, a final datatype of a functor F is a datatype T and
an operation out : T -> F T for which the equation in h

  out . h = F h . f

has a unique solution for given f. We write "unfold_F f" for
that unique solution, so

  h = unfold_F f  <=>  out . h = F h . f

This is a coinductive definition of unfold, and the above
equivalence (the "universal property for unfold")
encapsulates proof by structural coinduction.

> how is it used to prove theorems?

Exactly the same way. For example, the datatype Stream A of
streams of A's is the final datatype of the functor taking X
to A x X. An example of an unfold for this type is the
function iterate, for which

  iterate f x = [ x, f x, f (f x), f (f (f x)), ... ]

defined by

  iterate f = unfold_{A x} <id,f>

One might expect that

  iterate f . f = Stream f . iterate f

and the proof of this fact is a straightforward application
of the universal property of unfold (that is, a proof by
coinduction).

Jeremy

-- 
Jeremy.Gibbons@comlab.ox.ac.uk
  Oxford University Computing Laboratory,    TEL: +44 1865 283508
  Wolfson Building, Parks Road,              FAX: +44 1865 273839
  Oxford OX1 3QD, UK.  
  URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html