Lambda the Ultimate

One just needs to be aware that each author has slightly different definitions, e.g., many authors do not require schemes of diagrams to be categories themselves (just general graphs). This, of course, does not serve well to the theory in general, and undermines its use as a common dictionary for discussion of problems. The worst, probably, is unability to use intuition developed for definitions of one author working with text written by another :-(

On the bright side, (I think) there are not many such divergence points in category theory. Can you share your experience?

We definitely have cognitive problems here ;-)

on the other hand, looking ahead, i think his emphasis on diagrams is a good thing that is missing from other stuff i have skimmed through. and he seems to cover more topics.

this started as trying to explain different approaches to category theory, but i think i don't yet understand enough to do so. maybe it is more useful as guidance to anyone else thinking of learning from this paper?

pure mathematics is very annoying. on the one hand, all the precision is tedious. on the other, as soon as some precision is missed, or i overlook it, everything becomes uncertain... physics is so much easier, because you can (nearly) always look out of the window and check that you are making sense by seeing the maths at work.

Examples are:
groups and homorphisms,
topological spaces and contintuous functions,
vector spaces and linear functions.

While reasoning about categories you may abstract from concrete objects and their inner machinery. I think this power of abstraction, as well as ability to abstract multiple times (think functors and natural transformations) are next to main advantages of CT. The main one, though, I think is giving a common dictionary to discuss all these things (and a common intuition to manage all this complexity).

I think it should have been : (...) is the partial function g o f : A -o-> C defined above.

Anybody to confirm the mistake or I don't understand *anything* about functions and sets ?

Yes, that's a bug. It's a pity mathematicians do not use literate programming for their texts ;-)

Aye. I think computer scientists esp. those working on programming languages tend to be much more rigorous than your average mathematician.

No. In fact lambda calculus looks much less rigourous then other branchs. Category theory is mainstream mathematics ( sort of a lot of grad students try to avoid it as much as possible ). Granted it seems more abstract, but then hey, it tries to abstract the abstractions.

categorytheorygroup@yahoogroups.com

categorytheory@yahoogroups.com

though both are thinly populated.

TUNES: Category Theory 101

Anyone has more links ?

http://www.cs.toronto.edu/~sme/presentations/cat101.pdf

The Google cache is here.

I think there is broad agreement on the basic concepts, although sometimes there are several names for the same concept (for example, source versus domain, or arrow versus morphism).

The issue you take exception with, namely whether diagrams are functors or graph morphisms, is not really an issue, though, only a question of presentation. The reason is that every graph morphism to a category extends uniquely to a functor from the path category generated by its domain; conversely, every functor is a graph morphism from the underlying graph of its domain. (This is actually an adjunction between Grf and Cat.) If you define a diagram as a functor, then, you just have to be a little more careful to make sure that it preserves paths.

If you feel you would benefit from a more careful treatment of diagrams, then I recommend Barr and Wells' Category Theory for Computer Science; they are very conscientious in their explanation of diagrams, and it really pays off when you have to discuss (co)limits and sketches.

ehud: Aye. I think computer scientists esp. those working on programming languages tend to be much more rigorous than your average mathematician.

I think computer scientists are more formal, not really more rigorous. (There is a difference.) Mathematicians, BTW, seem to see CT as a way to be more rigorous without being more formal; computer scientists tend to see it as a way of being both more rigorous and formal, without being long-winded.

It's not available online, is it? I remember looking for it... I might end up supporting imperialistic Amazon by buying it (the book, not Amazon) :-)

This is a good distinction and worth keeping in mind, nad in general I'd have to agree with it. But I think this is only part of the story. The trend towards careful axiomatization and fanatical rigor in math is quite recent. Non-Euclidean geometry is quite a recent idea. Same goes for the axiomtization of set theory etc.

Due to the historical context, computer science began after this trend has already started, and from the get go was aware of the importance of formal reasoning as tool for achieving more rigorous results.

I am not sure whether this is the place to go into details concerning the philosophy of math (a personal hobby horse), but let me just say that where as most mathematicians decide that the formalist agenda has run its course, and work from a platonist framework, computer science remain true to the formal philosophy.

Nope, unfortunately not. Their other book, Toposes, Triples and Theories is, and is available from PLT Online, but it's much harder going. I haven't read it, and I dunno how it handles diagrams off-hand.

Ehud: The trend towards careful axiomatization and fanatical rigor in math is quite recent.

Yes. If by `recent' you mean since the beginning of the twentieth century... :) (I'm not trying to be sarcastic!)

computer science remain true to the formal philosophy

Since programs are elements of a formal language, this is somewhat unavoidable. Of course, when you are discussing the metatheory, nothing stops you from employing non-constructive (`Platonic') methods, but it's more economical just to use the same sort of logic at the meta-level that you use at the object-level.

Most proofs in CS are pretty easy, anyway, compared to ones in general mathematics, and don't seem to benefit much from employing non-constructive arguments. Also, if you work in a constructive metatheory, there is always the tantalizing possibility that you can internalize a meta-result---constructive proofs are programs.

Hm, I wonder how we (I?) got from `formal' to `constructive'; they are not the same.

Hm, I wonder how we (I?) got from `formal' to `constructive'; they are not the same.

Not by a long shot. But it is true that CS is not only more formal, but also more constructive.

Frank: Of course, when you are discussing the metatheory, nothing stops you from employing non-constructive (`Platonic') methods And when discussing meta-circular theory, you must employ non-constructive methods? Or am I treating Hoedel's theorem too liberally?