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.
|
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).
Lemma 3.5.12 and its corollary, about functions of two arguments, show how much easier it is to use directedness than sequences.
NOTATION 3.4.3 If Á is directed then we indicate this fact by an arrow when writing its directed join:
|
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
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
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
|
|
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 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. []