coinduction papers

coinduction papers

[categories]

Date: Wed, 21 Jan 1998 21:22:55 +0000 (GMT)
From: Dusko Pavlovic <D.Pavlovic@doc.ic.ac.uk>

Dear Categories,

Two papers about coinduction and guarded induction, one of them
joint work with Martin Escardo, are available from

	http://www.cogs.susx.ac.uk/users/duskop/	or
	ftp://ftp.cogs.susx.ac.uk/pub/users/duskop/

*Calculus in coinductive form* is not one of those funny calculi where
you can prove anything, just your old Newton-Leibniz-Taylor-Laplace
calculus, with a special emphasis on Taylor and Laplace, and a bit of
categories.

*Guarded induction*, on the other hand, is this logical principle
whereby, to prove a proposition p, you are allowed to use, among other
things, that very same proposition p --- erm, provided, of course,
that you make sure that it is #guarded#. This gives rise to various
funny calculi, and a bit of categories.

(Proper abstracts follow.)

With best wishes,
-- Dusko Pavlovic


===================================================================

	CALCULUS IN COINDUCTIVE FORM
	by D. Pavlovic and M.H. Escardo

	Abstract.

Coinduction is often seen as a way of implementing infinite objects.
Since real numbers are typical infinite objects, it may not come as a
surprise that calculus, when presented in a suitable way, is permeated
by coinductive reasoning.  What *is* surprising is that mathematical
techniques, recently developed in the context of computer science,
seem to be shedding a new light on some basic methods of calculus.

We introduce a coinductive formalization of elementary calculus that
can be used as a tool for symbolic computation, and geared towards
computer algebra and theorem proving.  So far, we have covered parts
of ordinary differential and difference equations, Taylor series,
Laplace transform and the basics of the operator calculus.



===================================================================

	GUARDED INDUCTION ON FINAL COALGEBRAS
	by D. Pavlovic

	Abstract.

We make an initial step towards categorical semantics of guarded
induction. While ordinary induction is usually modelled in terms of
least fixpoints and initial algebras, guarded induction is based on
*unique* fixpoints of certain operations, called guarded, on *final*
coalgebras. So far, such operations were treated syntactically. We
analyse them categorically. Guarded induction appears as couched in
coinduction.

The applications of the presented categorical analysis span across the
gamut of the applications of coinduction, from modelling of
computation to solving differential equations. A subsequent paper will
provide an account of some domain theoretical aspects, which are
presently left implicit.