Dusko says:
it's interesting that almost no one took michael healy's bait (attached).
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> There's a minefield of hotly held opinions behind this question, but let me
Here's a message I sent to Michael Healey privately: 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 <favourite keyword> 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