Domain Theory and Semantics: II

Continuing where we left off last time, let’s actually do some maths and build up more of the machinery of domain theory.

We’ve already introduced the concept of CPOs and given an example in the set of natural numbers with a least element, \bot, attached and where the partial order is that all numbers are greater than \bot and all numbers are incomparable to each other. Of course, we didn’t actually prove that every chain in \mathbb{N}_{\bot} has a least upper bound so let’s establish that now since it’s illustrative.

Let Y be a chain in \mathbb{N}_{\bot}, and given the nature of the partial-ordering then given any i < j then Y_i \sqsubseteq Y_j, but Y_i \sqsubseteq Y_j means that either Y_i = Y_j or that Y_i = \bot and Y_j is a number. There are then only two structural forms the chain Y can take: it is either the constant chain of \bot or there exists some index i such that \exists n. \forall j. i \leq j \implies Y_i = n. In the former case, the least upper bound is \bot and in the second case the least upper bound is n. At this point, let’s introduce the notation for least upper bounds of chains which is that for a chain Y we have \bigsqcup_i Y_i is the least upper bound, if it exists.

Next, let’s address the claim I made last time about the continuous functions being a CPO themselves. First we need to define what the order on functions is: f \sqsubseteq g = \forall x. f(x) \sqsubseteq g(x). This defines a partial order, but how do we show that it’s complete? Since the ordering is defined pointwise, then we’ll define the leat upper bound pointwise as well. If Z is a chain of continuous functions, then we define \bigsqcup_i Z_i to be the function (\bigsqcup_i Z_i)(x) = \bigsqcup_i (Z_i(x)), in other words that the least upper bound of a chain of functions is the function that returns the least upper bounds of the pointwise chains. Since the codomain is a CPO, we know that these pointwise lubs always exist and that this is a well-defined construction. We have thus proven that continuous functions form CPOs.

Another important thing we want to address about CPOs is that if a CPO A is pointed, i.e. has a least element \bot, then every continuous function f : A \to A has a fixed point. We create a chain out of repeated applications of f to itself, starting with \bot. In other words, we define the chain F_i = f^i(\bot). Since A is a CPO then this chain has a lub, and we’ll call the lub fix(f). Now we need to prove that it’s really the fixed point. The algebra is as follows f(fix(f)) = f(\bigsqcup_i F_i) = \bigsqcup_i F_{i+1} where the last equality follows from the definition of continuity and the definition of F. We also know that \bigsqcup_i F_{i+1} = \bigsqcup_i F_i since dropping the first element of the sequence can’t change the upper bound, and putting these facts together we get that f(fix(f)) = fix(f) and thus we’ve actually defined the fixed point.

Note, though, that this isn’t always an interesting fixed point. If we’re modelling, say, a strict language then this construction applied to a type A that isn’t a function type will just give you \bot as the fixed point. It’s going to be important, however, that we always have the ability to make a fixed point.

Next, let’s talk a little bit more about our ideas of information ordering. So far we’ve asserted that we can think of chains as a sequence of observations about the computation. There’s something a little fishy about it so far, though, because we haven’t really established that all our observations are going to be in a form that we could actually see as intermediate states of the computation. Conceptually, I think of observations as some form of debugging or print statements you have running that shows data as its computed. In some sense, these observable states are very discrete. We can’t observe two-and-a-half elements in a list, there is a transition from two to three elements at some observation. Our definition of CPOs aren’t restrictive enough to enforce this kind of finiteness, so we need to consider a slightly more restrictive definition. First, we encode the idea of being in a “finite” state with the notion of compactness. An element x of a CPO is compact if, for any chain Y such that x \sqsubseteq \bigsqcup_i Y_i then there exists some y such that x \sqsubseteq y. (Note for the experts in the audience: I’m sticking to the language of chains whenever possible because I find sequences easier and, I believe, for our purposes in semantics it doesn’t actually make a difference. If I’m losing important generality please let me know.) When I first saw this definition I thought it was a bit unituitive, but I think the key idea is that it cannot be “arbitrarily close” to another element because that arbitrary closeness is related to finiteness of representation. It’s like the difference between 0.\overline{9} and 1, in a way? 0.\overline{9} doesn’t have a finite representation and cannot actually be computed, meanwhile the number 1 can. That’s not an exact comparison, but maybe it shows some of the analogy? (Also, if anyone has a better analogy I’d love to hear one.)

We will say that a CPO D has a basis if there exists a subset of D, D_0, such that for all d \in D then all the elements of D_0 that are less than d form a chain whose least upper bound is d. In other words, a subset is a basis if its elements can approximate any element of D. We call a CPO algebraic when it the set of its compact elements is a basis. The algebraic CPOs, or some richer subtype thereof, are an important tool for modelling programming languages within domain theory because algebraicity more or less means that every element is computable by some sequence of intermediate steps, all of which are computable.

I think I’m going to leave things here for now, and then start talking about the D_{\infty} construction next time since it’s a bit involved and this post is hitting the roughly 1000 word limit I want to keep technical posts to.

Advertisements

One thought on “Domain Theory and Semantics: II

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