can anyone explain coinduction? in what sense it dual to induction? does it relate to the basic picture for a NNO? is there a (meaningful) concept of co-recursion? what would be the appropriate internal language? how is it used to prove theorems? Al Vilcius al.r@vilcius.com
Hi, Al Vilcius writes: From: "Al Vilcius" <al.r@VILCIUS.com> Date: Fri, 20 Oct 2000 08:57:20 -0400 Subject: categories: coinduction can anyone explain coinduction? Have a look at Bart Jacobs and Jan Rutten A Tutorial on (Co)Algebras and (Co)Induction Bulletin of the EATCS, Vol. 62, pp. 222-259, 1996. it is available on the authors homepages, for instance http://www.cs.kun.nl/~bart/PAPERS/JR.ps.Z Bye, Hendrik
In brief: If a structure has no nontrivial substructures, you can prove a property P is true of everything in the structure by proving that the elements with property P form a nonempty substructure. Take the structure to be N with the unary operation of successor and you get induction. Now say that in the opposite category: If a structure has no nontrivial congruences, you can prove that two objects are equal if they are equivalent under any congruence. (You can define "definition by coinduction" by a similar dualization.) This has found many applications in computer science (where the congruence is bisimulation). See J.J.M.M. Rutten, Universal coalgebra: a theory of systems. Theoretical Computer Science 249(1), 2000, pp. 3-80 and other papers by him on his website: http://www.cwi.nl/~janr/papers/ --Charles Wells
can anyone explain coinduction? in what sense it dual to induction? does it relate to the basic picture for a NNO? is there a (meaningful) concept of co-recursion? what would be the appropriate internal language? how is it used to prove theorems?
Al Vilcius al.r@vilcius.com
Charles Wells, 105 South Cedar St., Oberlin, Ohio 44074, USA. email: charles@freude.com. home phone: 440 774 1926. professional website: http://www.cwru.edu/artsci/math/wells/home.html personal website: http://www.oberlin.net/~cwells/index.html NE Ohio Sacred Harp website: http://www.oberlin.net/~cwells/sh.htm
Al Vilcius asks:
can anyone explain coinduction? in what sense it dual to induction?
and most people reply along the lines of:
The principle of induction says that initial algebras have no non-trivial subalgebras.
Coinduction says, dually, that the final coalgebra has no non-trivial quotients.
but wouldn't it be nice to keep the standard definition of induction, which says that the equations f(0) = c f(n+1) = g(f(n)) determine a unique f, given c and g? this is the definition that most first year students study, and many programmers use every day, usually without the slightest idea about subalgebras, or triviality. do we really gain anything by replacing this simple scheme by the higher-order statement about all subalgebras? ok, we do get the appearance of symmetry between induction and coinduction. but is the higher-order statement about quotients really the friendliest form of coinduction, suitable to be taken as the definition? i think barwise and moss somewhere describe coinduction as *induction without the base case*. the coinduction principle says that the equation X = a.X + bc.X determines a unique CCS-process, or a unique {a,b,c}-labelled hyperset. it also guarantees that the integral equation E(x) = 1 + \int_0^x E dt has a unique solution. (note that this is equivalent to the differential equation E(0) = 1 E = E' where the initial condition gives the base case for the power series solution. so the no-base-case slogan is just a matter of form? but note that E' = E, and more generally E' = h(E), for an analytic h, identifies two *infinite* streams, and is not a mere inductive step up the stream.) in any case, i contend that the practice of coinduction primarily consists of solving *guarded equations*, like the two above --- surely if you count the areas where people extensively use coinduction, without calling it by name, viz math analysis. ((it is true that computer scientists became aware of coinduction while working out the bisimulations etc, which is why the quotients came in light. but now it seems that the bisimulations were just the way to construct final coalgebras; whereas the coinduction, in analogy with the induction, should be a practically useful logical principle, available over the *given* final coalgebras.)) anyway, the heart of the matter probably lies in peter aczel's insight that the statement * V ---> PV is a final coalgebra for P = (finite) powerset functor equivalently means that * every accessible pointed graph has a unique decoration in V. presenting the graph definitions as systems of guarded equations (like in barwise and moss' book "vicious circles"), the above equivalence generalizes to the statement that * V --d--> FV is a final coalgebra for F iff * every system of guarded equations over V has a unique solution. where the notion of guarded is determined by F and d. this is, of course, just barwise and moss' solution lemma, lifted to F. or more succinctly : **V is a final fixpoint iff each guarded operation g:V-->V has a unique fixpoint** this, of course, supports the view that ***coinduction is solving guarded equations***... i was hoping to say more, but will have to leave it for later, and post this hoping to motivate discussion. unguardedly yours, -- dusko pavlovic PS i have a great appreciation for jan rutten's work on coinduction, but it seems to me that the title of *universal coalgebra* is a bit exaggerated. universal algebra does not dualize. by design, it is meant to be model theory of algebraic theories. what would be the "coalgebraic theories", leading to coalgebras as their models? what would their functorial semantics look like? (implicitly, these questions are already in manes' book.) and then, moving from coalgebraic theories to comonads, like from algebraic theories to monads, should presumably yield an HSP-like characterization for the categories of (comonad) coalgebras. but coalgebras for a comonad over a topos usually form just another topos. i may be missing something essential here, but then i do stand to be corrected.
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
participants (5)
-
Al Vilcius -
Charles Wells -
Dusko Pavlovic -
Hendrik Tews -
Jeremy Gibbons