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