Practical Foundations of Mathematics

Paul Taylor

3.4  Domains

Domains abstract what is needed to prove Tarski's fixed point theorem. For the interpretation of programming languages, joins of w-sequences suffice, so many authors just consider w-complete posets with ^, though there are very many more specialised notions in the literature.

Directed diagrams   Aside from the fixed point theorem, carrying the completeness property for sequences verbatim through our working gets us caught in pedantic and ultimately confusing notation. For example, if we take such a join over two indices n and m we no longer have a sequence. The following definition is equivalent (in the sense of Proposition 3.2.10), but it is invariant under operations such as products.

It may be important that the diagram be computable (and a fortiori countable), but this is an issue which is best studied separately.

DEFINITION 3.4.1 A poset is directed if every finite subset F has an upper bound F i . Specialising this to the cases F = and F = {\numi1,\numi2}, directedness is equivalent to

is non-empty, ie it has an element, and "\numi1,\numi2.$i.\numi1 i\numi2 i.

Two similar but weaker notions turn out to be useful.

If the binary form (alone) holds then we say that is semidirected. Classically, a poset is semidirected iff it is either directed or empty.

We say that is confluent ( cf Definition 1.2.5) if
"\numi0,\numi1,\numi2.    \numi0 \numi1 \numi0 \numi2 $i.\numi1 i \numi2 i.

A directed lower subset of a poset X is called an ideal , and we write IdlX for the poset of them, ordered by inclusion. The analogy between lattices and rings which lies behind the name ideal ( cf Example 2.1.3(b)) was first noticed by Marshall Stone in 1935 (Exercises  3.10 and 3.11).


Any poset which has a greatest element is directed.

N with the arithmetical order is directed (w, Definition 3.3.9).

Any join-semilattice ( cf Definition  3.2.12) is directed.

A lower subset of a join-semilattice is directed (an ideal) iff it is a (lower) subsemilattice.

For any set X, the powerset P(X) and, more usefully, the finite powerset Pf(X) consisting of the finite subsets of X, are directed posets under inclusion; see Lemma  6.6.10(e).

Raw l-terms form a confluent preorder under (reverse) bh-reduction (the Church-Rosser Theorem, Fact  2.3.3).

A poset is confluent iff every connected component (Lemma  1.2.4) is directed.

Lemma 3.5.12 and its corollary, about functions of two arguments, show how much easier it is to use directedness than sequences.

Posets with directed joins  

NOTATION 3.4.3 If is directed then we indicate this fact by an arrow when writing its directed join:

\dirsupdisplayi xi.
Often this arrow is used instead of saying in words that the relevant set is assumed or has been shown to be directed.

DEFINITION 3.4.4 A poset which has all directed joins is called directed complete or a dcpo for short. If it also has a least element - from which it follows (without using excluded middle) that it has joins of all semidirected sets - then we call it an inductive poset or ipo.

The term complete partial order or cpo is commonly found instead of ipo in the literature, but we avoid it on the grounds that it conflicts with complete categories ( cf complete semilattices), which also have (the analogue of) finite joins. This confusion has been made worse by authors who use ``cpo'' for dcpo, ie not necessarily with bottom.

A (monotone) function between dcpos which preserves directed joins is said to be Scott-continuous. These are the most useful morphisms between ipos because we wish to allow programs to ignore inputs and so terminate even if these are not specified. This is peculiar from the point of view of universal algebra because not all of the structure is preserved. The fixed point theorem is essentially the only use of ^.

REMARK 3.4.5 Peter Freyd [Fre91] observed that the three notions of

domain (having, but with functions not necessarily preserving,  ^),

predomain (not necessarily having ^ at all) and

lift-algebra (both having and preserving ^)

ought to be formulated in tandem (Example 7.5.5(c)). Since we only intend to investigate function-spaces, where ^ gets in the way, we shall concentrate on dcpos (predomains). Notice that when the morphisms change, in this case whether or not they have to preserve ^, we change the names of the objects too, from domain or ipo to lift-algebra.

LEMMA 3.4.6 The composite of two Scott-continuous functions is Scott-continuous, as is the identity function. []

The Scott topology   Continuity may be expressed in terms of open or closed sets, but the correspondence partly depends on excluded middle.

DEFINITION 3.4.7 A subset A X of a dcpo is said to be Scott-closed if it is a lower subset and also closed (``upwards'') under directed joins. In particular any representable lower set X x is Scott- closed.

LEMMA 3.4.8 A function f:X Y between dcpos is Scott-continuous iff the inverse image f-1(B) of every Scott-closed subset B Y is again Scott-closed.

PROOF: For monotonicity, let x x X and consider B = Y f(x), so x f-1(B). Then x f-1(B) f(x) f(x).

Suppose that f-1(B) is Scott-closed, where x = xi, y = f(xi) and B = Y y. Then xi f-1(B) by monotonicity, so x f-1(B) by the order-theoretic definition of Scott-closure, ie f(x) B and f(x) = y by monotonicity.

Conversely, let B Y be any Scott-closed subset and xi f-1(B) X be a directed set with f(xi) = f( xi) B. Then xi f-1(B) as required. []

Classically there is a bijective correspondence between closed subsets and their complementary open subsets, but we shall define them separately.

PROPOSITION 3.4.9 Let (X, ) be a dcpo. Then for a subset U X, the characteristic function cU:X W is Scott- continuous iff

U is an upper set and

it is inaccessible by directed joins, ie for any directed diagram x(-): X, if \dirsupi xi U then $i.xi U.

Such subsets are said to be Scott-open, and they form a topology. For any Scott-continuous function f:X Y between dcpos, the inverse image of any open subset V Y is open. The converse holds so long as there are enough Scott-open sets to make the specialisation order (Example 3.1.2(i)) coincide with the given order.

PROOF: Directedness is needed to show that the whole set X is Scott-open, and that intersections of open subsets are open. Closure under unions is easy, and we leave the rest as an exercise, adapting the previous argument for closed sets. []

DEFINITION 3.4.10 The type of truth values is playing a topological role here, in which the point T is open and ^ is closed. This is called the Sierpi\'nski space, S. Intuitionistically, it is intermediate between 2 and W, though the considerations bearing on what its definition ought to be lie outside the scope of this book (see the footnote on page  Sierp footnote), so as with R we shall avoid questions that rely on the distinctions.

Classically, subsets of the form {x|x\not y} are Scott-open, but the Scott topology need not be sober [ Joh82, p. 46]. For an intuitionistic result, we restrict attention to a smaller class of domains, drawing upon another source of upper (so possibly open) subsets: those of the form x X.

DEFINITION 3.4.11 Let x X in a dcpo. If x X is Scott-open, ie


yi     $i.x yi
for all directed sets, then x is said to be compact or finitely generable. We write \Xfg X for the subset of compact elements. If, for each x X,
\Xfg x {y|x y \X fg} is directed with join x
then X is called an algebraic dcpo. The name arose by extension from algebraic lattices (Theorem  3.9.4), but since their algebraic aspect has really been lost, finitary or locally finitely generable would be better names. Algebraic dcpos satisfy the qualification of the previous result, as do the more general continuous dcpos [ GHK+80, Joh82].

PROPOSITION 3.4.12 A dcpo X is algebraic iff it is isomorphic to Idl(Y) for some poset Y. Then for any dcpo Q there is a bijection

omitted prooftree environment
In particular the topology is the lattice of monotone functions [Y W].

omitted diagram environment

PROOF: [ ] For X algebraic, put Y = \Xfg. Then = {y|x y Y} and x = give the isomorphism. [ ]  For any ideal Idl(Y), = {Y y|y }. is compact iff = Y y for some y Y. Finally, any continuous function f:X Q is determined by its values at compact elements. []