From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1808 Path: news.gmane.org!not-for-mail From: S.J.Vickers@open.ac.uk Newsgroups: gmane.science.mathematics.categories Subject: RE: Question Date: Fri, 26 Jan 2001 11:32:04 -0000 Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" X-Trace: ger.gmane.org 1241018118 581 80.91.229.2 (29 Apr 2009 15:15:18 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:15:18 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Fri Jan 26 14:54:32 2001 -0400 Return-Path: Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f0QHwwV07640 for categories-list; Fri, 26 Jan 2001 13:58:58 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Mailer: Internet Mail Service (5.5.2650.21) Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 39 Original-Lines: 89 Xref: news.gmane.org gmane.science.mathematics.categories:1808 Archived-At: Dusko says: > it's interesting that almost no one took michael healy's bait (attached). > Here's a message I sent to Michael Healey privately: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> There's a minefield of hotly held opinions behind this question, but let me try to give a couple of pragmatic considerations. 1. What is the most appropriate characterization (for present purposes) of collections? By elements or by functions? Set theory postulates that a collection is entirely determined by its elements. If functions are better, that's beginning to look more like a categorical approach. Examples: Topology - a space is not fully defined by saying what its points are. You only capture continuity when you look at the maps between spaces. Type theory - syntactic terms in general have free variables in them, effectively parameters, and these really correspond to functions rather than simple elements. 2. Do you want to consider a variety of logics? Set theory as such is solidly classical. To relax that you need to consider different formal systems, and then category theory usually provides tools for achieving better presentation independence than more syntactic approaches. <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< In this hurried response to Michael's posting I was trying to get across some sense of how category theory can help you see the wood for the trees - the "better presentation independence" is what Dusko refers to as "structuralist maths". > for software engineers, foundations are the link with the meaning of their > programs. having a slightly shorter history than math, they do not have > languages as natural as arithmetic, or calculus, but have to chose between > KIF and Ontolingua, and the various other versions of esperanto every day. > categories dam the flood of structure in software engineering, just like > they originally did in homology theory almost 60 years ago. some good math > may come out of it if taken from a good side. I agree. I looked up keywords like SUO (Standard Upper Ontology) and KIF (Knowledge Interchange Format) - they are about standard notations for expressing information - and some key issues seemed to be rather basic things like the meaning of first order logic. I found this depressing. As we know, categorical logic has some very clear accounts of this that have the great virtue of bringing out deep structure over superficialities of the logical syntax. It also makes it easier to question whether "self-evident" notation and axioms are actually meaningful and valid. But how can we bring these insights to the software engineering masses? It's not enough to say "first learn about category theory and then look for adjunctions, monads and everywhere". With this approach it seems all too easy to prescribe people categorical logic as a cure for their myopia, and then to find them trying to use it as reading glasses and wondering why it doesn't work. One of the things that makes Mac Lane's book such a masterpiece is the way it uncovers category theory as something already understood rather than presenting it as something new. The working mathematician is well familiar with reasoning about adjunctions and monads in special cases, and it's "just" a matter of uncovering the underlying pattern. Speaking for myself, after all these years I still understand a lot of category theory not in the abstract but through paradigms. Enriched categories? They're just rings, really. Or, at least, ringoids. Presheaves? They're just modules. Yoneda embedding? The free module on one generator is just the ring itself. The software engineer does not have the working mathematician's body of knowledge. I think to give them category theory we first have to explain, without mentioning categories, just why structure has to reside not inside the objects but amongst the morphisms: to explain a collection by its elements alone is not enough, even in a very basic logical framework. Steve Vickers Department of Pure Maths Faculty of Maths and Computing The Open University ----------- Tel: 01908-653144 Fax: 01908-652140 Web: http://mcs.open.ac.uk/sjv22