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, , attached and where the partial order is that all numbers are greater than and all numbers are incomparable to each other. Of course, we didn’t actually prove that every chain in has a least upper bound so let’s establish that now since it’s illustrative.
Let be a chain in , and given the nature of the partial-ordering then given any then , but means that either or that and is a number. There are then only two structural forms the chain can take: it is either the constant chain of or there exists some index such that . In the former case, the least upper bound is and in the second case the least upper bound is . At this point, let’s introduce the notation for least upper bounds of chains which is that for a chain we have 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: . 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 is a chain of continuous functions, then we define to be the function , 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 is pointed, i.e. has a least element , then every continuous function has a fixed point. We create a chain out of repeated applications of to itself, starting with . In other words, we define the chain . Since is a CPO then this chain has a lub, and we’ll call the lub . Now we need to prove that it’s really the fixed point. The algebra is as follows where the last equality follows from the definition of continuity and the definition of . We also know that since dropping the first element of the sequence can’t change the upper bound, and putting these facts together we get that 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 that isn’t a function type will just give you 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 of a CPO is compact if, for any chain such that then there exists some such that . (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 and 1, in a way? 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 has a basis if there exists a subset of , , such that for all then all the elements of that are less than form a chain whose least upper bound is . In other words, a subset is a basis if its elements can approximate any element of . 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 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.