Paper of the day: Category Theoretic Solution of Recursive Domain Equations

Okay, this paper was a reread but it was something that I needed to digest better than the first time. Smyth & Plotkin's classic paper. So what's the point of this paper?

Okay, so Dana Scott had this classic result where he built - as a colimit - a domain D\inf (think partially ordered set with some nice properties) that was isomorphic to the set of continuous functions from D\inf to D\inf, thus showing a particular technique in domain theory for building models of the untyped lambda calculus. Another way to put this is that D\inf is the fixed point of the functor F(D) = D -> D.

Well, the problem is that the original construction is fairly rigid, taking place only in a particular category of domains. So the point of this paper is try generalize it to all categories and functors that satisfy certain properties. So what properties do we require?

Well, first we can generalize the notion of omega chain from domain theory to category theory. It's basically the same thing if you think of an arrow from objects A and B to be the same as "A < B", so it's a countable diagram of objects with an arrow leading from the previous to the next object in the sequence.

So then what's a omega-continuous functor? Well, it's a functor that maps colimits of omega chains to colimits of the omega chain induced by the action of the functor. It's basically the interchange of function and limit we're used to from domain theory. Yay!

So the paper establishes one thing right off the bat: if you have a continuous functor and colimits of omega chains exist, then you'll have a fixed point of that functor. So the problem becomes figuring out when you have an omega-complete category.

However, requiring that the category we work in be omega-complete is actually a bit more restrictive than we want. Instead, we work in what are called O-categories which are categories enriched CPO. The bulk of the paper is about showing how most O-categories allow us to find the colimits in the subcategory of embeddings, which has nicer properties and can more readily be omega-complete, and then pull those colimits back to the original category.

It's actually really cool to work through, although I feel like I haven't done the best job of explaining it! The math isn't terribly deep diagram chasing, so if you're at all familiar with category theory you can follow it with a bit of work. I'll confess, though, that the first time I tried to read it I was sitting and scratching my head wondering that the point was, but the point seems to basically be that by generalizing the D\inf construction to its minimal requirements you can get away with using slightly weaker categories than used to be considered prior to this paper.