From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1663 Path: news.gmane.org!not-for-mail From: Charles Wells Newsgroups: gmane.science.mathematics.categories Subject: Re: coinduction Date: Fri, 20 Oct 2000 18:19:57 -0700 Message-ID: <4.1.20001020180219.012fa110@mail.oberlin.net> References: <003301c03a95$49f73610$448a0dd8@main> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" X-Trace: ger.gmane.org 1241018004 32317 80.91.229.2 (29 Apr 2009 15:13:24 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:13:24 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Sun Oct 22 17:55:27 2000 -0300 Return-Path: Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id e9MKJbn12149 for categories-list; Sun, 22 Oct 2000 17:19:37 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Sender: cwells@mail.oberlin.net X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 In-Reply-To: <003301c03a95$49f73610$448a0dd8@main> Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 21 Original-Lines: 37 Xref: news.gmane.org gmane.science.mathematics.categories:1663 Archived-At: 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