From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1919 Path: news.gmane.org!not-for-mail From: Paul Taylor Newsgroups: gmane.science.mathematics.categories Subject: Re: Category Theory and Hereditarily-Finite Sets Date: Thu, 19 Apr 2001 19:29:13 +0100 Message-ID: <200104191829.TAA04249@koi-pc.dcs.qmw.ac.uk> NNTP-Posting-Host: main.gmane.org X-Trace: ger.gmane.org 1241018204 1205 80.91.229.2 (29 Apr 2009 15:16:44 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:16:44 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Thu Apr 19 17:49:51 2001 -0300 Return-Path: Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f3JKHPU13443 for categories-list; Thu, 19 Apr 2001 17:17:25 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 17 Original-Lines: 29 Xref: news.gmane.org gmane.science.mathematics.categories:1919 Archived-At: > Hereditarily-finite sets are becoming increasingly more popular > in computer science research. Why? Because some ill-advised first year maths lecturer told you that the element relation was the foundation of mathematics, maybe? > "object" is a hereditarily-finite set plus some structure on the set > and a "morphism" would be a structure-preserving function. If you're really interested in heredity, so the "structure" is the element relation, this is a well-founded coalgebra for the covariant powerset functor. Coalgebras for the powerset functor were first studied by Gerhard Osius in JPAA in 1974, although he considered recursion rather than induction. Well founded coalgebras for general functors (but with some emphasis on the powerset) are defined in Section 6.3 of my book "Practical Foundations of Mathematics" (Cambridge University Press, 1999). The exercises for that chapter show how various ideas with recursive programs may be expressed in these terms. In particular, unary recursion (with at most one recursive call at each level) is reduced to tail recursion (equivalent to while programs) together with an accumulator monoid. Paul