Well, it’s been awhile since our last post on domain theory, but where we left off last time we’d talked a little bit more rigorously about what it means to be a CPO, the existence of fixed points in pointed domains, and about algebraic CPOs. Now we want to get to actually describing the construction that provides an explicit model of the untyped lambda calculus. It’s going to require a little bit of category theory, but it’s not going to be that bad, I promise.
First, though, I want to go back to compact elements and all that. So I was reading chapter 5 of Gunter’s semantics book, the chapter on notions of finite approximation and finite element, when it finally hit me what’s useful about the definition about compactness for elements and why it encompasses a notion of finiteness. As a reminder, an element is compact when for any chain such that then there is some element in the chain such that . Now, if we consider a chain where every element is less than whose least-upper-bound is then this condition means that we’ll have some element of the chain, , that is simultaneously and which means that it’s actually equal to . In simple words, it means that if you have a chain of approximations of a compact element then there can only be finitely many steps to the approximation before you reach the compact element. This is the sense in which compact elements are finite, in that they are reachable through finite steps of “computation” for some very abstract notion of computation as process.
Alright with that epiphany out of the way, we’ll start actually describing the construction. We’ll follow the approach in Tennent’s semantics book, because I think it does a really good, clear job of outling the pieces of the approach and showing how constructing models for the untyped lambda calculus is a special example of general solution of domain equations.
Here’s the basic outline of the argument. First, that we want to let our domain equations, such as , to be defined as the least-fix points of some kind of functor so that the equality in our domain equations is “really” just isomorphism. We also want to define a special kind of category of CPOs for two reasons. The first is that we want to have the arrows in the this category represent a notion of embedding, where an arrow exists iff is somehow a subdomain of , so that we can have a notion of infinite sequences of embeddable domains and show that such sequences have colimits. Now why is this important? Because such an infinite sequence represents all the finite approximations of some domain such as, I don’t know, a domain we’re trying to define as the least fixed point of a functor. Once we know such colimits exist, then we just need to show that our domain-building functor preserves colimits so that it’s action on the colimit is, again, a colimit of the sequence of finite approximations. What do we know about two colimits for the same diagram, girls and boys? That’s right! They’re isomorphic!
Wait, you might ask, how is this the least fixed point. That’s because this is a colimit in the category of CPOs and embeddings. To be more specific, assume that our sequence of domains is , our colimit of the sequence is and that is another domain that all of the can be embedded into consistently, i.e. it’s a cone over the diagram given by the sequence . The property of being a colimit means that there is an embedding such that all the embeddings into from must factor through . In words, this means that is the smallest domain that contains all the finite approximations in the sequence .
So that’s the basic idea. We’re going to
- define our notion of embedding
- show that sequences of embedded domains have a colimit
- show that the (diagonalization of the) exponential functor is colimit preserving
then, we will have shown how to create a model of the untyped lambda calculus as well as a number of other calculi.
Let’s start on step one. The notion of embedding we’ll use is that of “embedding-projection pairs”, often abbreviated as ep-pairs, and in some literature such as Amadio and Curien they’re called “injection-projection pairs”. An ep-pair between domains and , symbolically represented as , is a pair of continuous functions and such that
or, in words, that is a 1-1 continuous injection of into and is a continuous surjection that takes elements of to their best approximants in .
We’ll skip the details showing that for any category of domains that we want to use, such as CPO, that the corresponding category of domains that have embeddings as arrows truly is a category. It’s pretty simple to show, though, that identity arrows exist and that you can define an appropriately associative composition.
Instead, let’s go to showing that any sequence of domains and embeddings has a colimit. The definition of the colimit is fairly simple: it’s the set of partially-defined sequences such that
- there is some such that exists
- for any that exists, then
- if either or exists then both exist and
and is given a domain structure pointwise, so both comparisons and LUBs are defined by their action at each “slot” in the sequence. Since these are sequences of CPOs, we know that the pointwise LUBs must exist.
In order to show that this is a colimit, we first need to give arrows that commute with the . In more categorical language, we need to define the cone over the graph. Since such an embedding takes an element of to a sequence of elements in , we’ll basically use the pairs in order to generate a sequence from a given element, projecting it forward with repeated applications of the -s if and projecting it backwards with applications of -s if . Slightly more formally, we have that the sequence has elements given by if and if instead then we project “down” with . The projection is even simpler, as , or in other words the projection from a sequence down to the -th individual domain is just given by taking the -th element of the sequence. The nice thing is that the commutivity requirement we want follows immediately from the definition of the embedding and projection.
So now we’ve defined the cone, but we have to show it has the colimit property that says any other cone must be able to be factored through . Basically, the idea is that if we have another cone with base point a domain and embeddings then we’ll define our factoring map such that for all then . First, we note a couple of things: first that if we take then this composition creates a monotone sequence where . The reason for this is that composition is monotone and by the nature of embeddings we have that both and , from this we can conclude that in the continuous function space we then have that the LUB is well-defined. This will play the injection part of our embedding and then will be the “dual” defined as $\bigsqcup_i eta_i ⋅ . Noting, without proof, that then we can rather easily prove that and that , so this is a properly defined embedding. We still need to show that this embedding gives us the factoring that we want and that any other such embedding must be equal to .
Since this post has already gotten to be much longer than I intended, I think maybe I’ll leave things here for now and just write a part 4 sometime soon. I mostly just want to post something right now given that it’s been I think over a month since my last post and that’s far too long.