Domain Theory and Semantics: III

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 D_{\infty} 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 x is compact when for any chain Y such that x \sqsubseteq \bigsqcup_i Y_i then there is some element y in the chain such that x \sqsubseteq y. Now, if we consider a chain where every element is less than x whose least-upper-bound is x then this condition means that we’ll have some element of the chain, y, that is simultaneously y \sqsubseteq x and x \sqsubseteq y which means that it’s actually equal to x. 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 D_{\infty} 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 D = D \to D, 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 D \to E exists iff D is somehow a subdomain of E, 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 D_i, our colimit of the sequence is D_{\infty} and that E is another domain that all of the D_i can be embedded into consistently, i.e. it’s a cone over the diagram given by the sequence D_i. The property of being a colimit means that there is an embedding h : D_{\infty} \to E such that all the embeddings into E from D_i must factor through h. In words, this means that D_{\infty} is the smallest domain that contains all the finite approximations in the sequence D_i.

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 ( \to ) 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 D and E, symbolically represented as D \triangleleft E, is a pair of continuous functions f : D \to E and g : E \to D such that

  • g \cdot f = id_{D}
  • f \cdot g \sqsubseteq id_{E}

or, in words, that f is a 1-1 continuous injection of D into E and g is a continuous surjection that takes elements of E to their best approximants in D.

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 D_i and embeddings (f_i : D_i \to D_{i+1}, f_i^P : D_{i+1} \to D_i) has a colimit. The definition of the colimit is fairly simple: it’s the set of partially-defined sequences s : \mathbb{N} \to \bigcup_i D_i such that

  1. there is some j such that s_j exists
  2. for any s_j that exists, then s_j : D_j
  3. if either s_j or f_i^P (s_{j+1}) exists then both exist and s_j = f_j^P(s_{j+1})

and D_{\infty} 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 \eta_i : D_i \triangleleft D_{\infty} that commute with the f_i : D_i \triangleleft D_{i+1}. In more categorical language, we need to define the cone over the graph. Since such an embedding takes an element of D_i to a sequence of elements in D_{\infty}, we’ll basically use the pairs (f_j,f_j^P) in order to generate a sequence from a given element, projecting it forward with repeated applications of the f-s if i \le j and projecting it backwards with applications of f^P-s if i > j. Slightly more formally, we have that the sequence \eta_i(d) has elements given by \eta_i(d)(j) = (f_{j-1} \cdot f_{j-2} \cdot \ldots f_i)(d) if i \le j and if instead i > j then we project “down” with \eta_i(d)(j) = (f_{j}^P \cdot \ldots f_{i-1}^P)(d). The projection is even simpler, as \eta_i^P(s) = s_i, or in other words the projection from a sequence down to the i-th individual domain is just given by taking the i-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 D_{\infty}. Basically, the idea is that if we have another cone with base point a domain E and embeddings \psi_i : D_i \triangleleft E then we’ll define our factoring map h : D_{\infty} \triangleleft E such that for all i then \psi_i = h \cdot \eta_i. First, we note a couple of things: first that if we take \psi_i \cdot \eta_i^P then this composition creates a monotone sequence where psi_i \cdot \eta_i^P \sqsubseteq psi_{i+1} \sqsubseteq \eta_{i+1}^P. The reason for this is that composition is monotone and by the nature of embeddings we have that both \psi_i \sqsubseteq \psi_{i+1} and \eta_i^P \sqsubseteq \eta_{i+1}^P, from this we can conclude that in the continuous function space we then have that the LUB \bigsqcup_i \psi_i \cdot \eta_i^P is well-defined. This will play the injection part of our embedding h and then h^P will be the “dual” defined as $\bigsqcup_i eta_i ⋅ psi_i^P. Noting, without proof, that \bigsqcup_i \eta_i \cdot \eta_i^P = id_{D_{infty}} then we can rather easily prove that h^P \cdot h = id_{D_{infty}} and that h \cdot h^P \sqsubseteq id_{D_{infty}}, 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 h.

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.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s