From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/607 Path: news.gmane.org!not-for-mail From: categories Newsgroups: gmane.science.mathematics.categories Subject: coinduction papers Date: Thu, 22 Jan 1998 16:39:30 -0400 (AST) Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: ger.gmane.org 1241017069 26484 80.91.229.2 (29 Apr 2009 14:57:49 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 14:57:49 +0000 (UTC) To: categories Original-X-From: cat-dist Thu Jan 22 16:40:37 1998 Original-Received: (from cat-dist@localhost) by mailserv.mta.ca (8.8.8/8.8.8) id QAA31811; Thu, 22 Jan 1998 16:39:30 -0400 (AST) Original-Lines: 71 Xref: news.gmane.org gmane.science.mathematics.categories:607 Archived-At: Date: Wed, 21 Jan 1998 21:22:55 +0000 (GMT) From: Dusko Pavlovic 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.