Re: coinduction

[Dusko Pavlovic <dusko@kestrel.edu>]

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

> I have always considered the statement regarding existence of a unique

> function f to be the principle of recursion.

the recursion schema, as defined by godel in 1930, is a bit  stronger: g is
allowed to depend on n, not only on f(n).

> The principle of
> induction is, in my mind, the weaker principle that says that if a
> property holds of 0 and is closed under successor, then it holds of N.

in a topos, this principle is equivalent with the above schema. and the
schema itself, of course, just means that [0,s] : 1+N --> N is initial: any
algebra [c,g] : 1+X --> X induces a unique homomorphism f : N-->X. using the
exponents, we do recursion.

as i said last time, induction and recursion have been in heavy use for so
long, that they really don't leave much space for redefining, even for the
sake of symmetry with coinduction and corecursion.

-- dusko