Subject: categories: coinduction

From: "Al Vilcius" <[email-masked]>
Date: Fri, 20 Oct 2000 08:57:20 -0400

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
[email-masked]

---

From: Hendrik Tews <[email-masked]>
Date: Fri, 20 Oct 2000 17:35:17 +0200 (MET DST)

Hi,

Al Vilcius writes:
   From: "Al Vilcius" <[email-masked]>
   Date: Fri, 20 Oct 2000 08:57:20 -0400
   Subject: categories: 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

---

From: Charles Wells <[email-masked]>
Date: Fri, 20 Oct 2000 18:19:57 -0700

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

>how is it used to prove theorems?

Charles Wells, 105 South Cedar St., Oberlin, Ohio 44074, USA.
email: [email-masked]. 
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

---

From: [email-masked] (Jesse F. Hughes)
Date: 20 Oct 2000 18:01:59 -0400

> how is it used to prove theorems?

The principle of induction says that initial algebras have no
non-trivial subalgebras.  Consider N, the initial successor algebra.
A subobject S of N is a subalgebra just in case there is a structure
map
s: S+1 -> S
such that the inclusion S -> N is a homomorphism.  This is just the
usual condition that 0 is in S and if n is in S, then so is its
successor.  Induction says that any such subalgebra exhausts the set
N.

Coinduction says, dually, that the final coalgebra has no non-trivial
quotients.  (To see that this is "really" a dual principle, we would
interpret "subalgebra" above as a regular subobject in the category of
algebras.)  However, the principle is usually stated in terms of
relations on a coalgebra, rather than quotients.  In these terms, the
principle of coinduction says: Any relation on <F,f> in the category
of coalgebras is a subrelation of equality.

Note: I stated the principles of induction/coinduction above for the
initial algebra/final coalgebra, resp.  However, just as induction
holds for any quotient of the initial algebra, coinduction holds for
any (regular) subcoalgebra of the final coalgebra.

I'm not sure what you're looking for in relation to NNOs.  An NNO is
the same as an initial algebra for the successor functor (assuming
that our category has coproducts).  The structure map N + 1 -> N is
given by [s,0], where s is the successor.  The final coalgebra for
successor is easily described (say, in Set):  It is the NNO with a
point adjoined for "infinity".  The structure map pred:F -> F + 1 fixes
infinity, takes n+1 to n and takes 0 to * (the element in 1 -- a kind
of "error condition").

As far as co-recursion goes, yes, there is a meaningful principle.
Namely, given any coalgebra <A,a>, there is a unique coalgebra
homomorphism from <A,a> to <F,f>.  Thus, for any set S together with a
function t:S -> S+1, there is a unique map h:S -> N u {infinity} such
that 
(1) if t(s) = *, then h(s) = 0
(2) else, h(t(s)) = h(s) - 1 (where infinity - 1 = infinity)
In other words, h here takes an element s to the least n such that
t^n(s) = *, if defined.  If, for all n, t^n(s) != *, then h(s) =
infinity.

I'll defer on the question of what the appropriate internal language
is.

As far as how coinduction is used to prove theorems: To show two
elements of the final coalgebra are equal, it suffices to find a
coalgebraic relation relating the elements.

Hendrik's suggestion (that you find Jacobs and Rutten's paper) is a
good one, but I hope these comments help until then.

-- 
Jesse Hughes
"Such behaviour is exclusively confined to functions invented by
mathematicians for the sake of causing trouble."
 -Albert Eagle's _A_Practical_Treatise_on_Fourier's_Theorem_

---

From: Dusko Pavlovic <[email-masked]>
Date: Thu, 26 Oct 2000 16:49:12 -0700

and most people reply along the lines of:

> non-trivial subalgebras.

> 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.

---

From: Jeremy Gibbons <[email-masked]>
Date: Mon, 30 Oct 2000 15:55:25 GMT

> 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

-- 
[email-masked]
  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