Examples 2.1.4 and 2.1.7 gave recipes for the type constructors ® and +, for sets and functions. In Section 2.3 we gave type-theoretic rules for these, and promised that we would find interpretations of them in other mathematical structures. We shall now do this with posets and domains. The sum of posets or domains is formed in the obvious way, as a disjoint union, ie the components are incomparable, so we concentrate on products and function-spaces.
Products of posets, domains, lattices and diagrams
PROPOSITION 3.5.1 Let (X, £ X) and (Y, £ Y) be preorders. We equip the cartesian product XxY with the componentwise order:
x1,y1 £ Xx Yx2,y2 if x1 £ Xx2 and y1 £ Yy2.
Then this makes XxY a preorder too. Also
The corresponding result for domains applies equally well to semilattices, lattices, Heyting (semi)lattices and complete (semi)lattices, so we state it for individual diagram shapes. We shall consider part (c) later.
PROPOSITION 3.5.2 Let X and Y be preorders and Á a diagram shape.
|
PROOF: In (a), q,f is an upper bound for the set of pairs iff q bounds the first components and f the second. Hence q,f is least (or locally least or mimimal) iff both q and f are. The other parts follow. []
COROLLARY 3.5.3 If X and Y are dcpos or ipos then so is XxY, the projections are Scott-continuous and pairing preserves continuity. []
Products of diagrams are used to handle multiple suffixes. Doubly indexed joins can be rearranged, as may doubly indexed meets, but Example 3.5.14 shows that meets cannot be interchanged with joins.
LEMMA 3.5.4 Let x(-),( = ):Áx J® X be a diagram. If either the expression on the left or that on the right is defined in
|
PROOF: Assuming that the intermediate joins exist, for q Î X,
|
PROPOSITION 3.5.5 Let Y be a preorder and f,g:X® Y be functions (the order, if any, on X is unimportant). Then the pointwise order between f and g is given by
f £ [X® Y] g if "x: X.f(x) £ Yg(x).
The preorder of monotone functions from X to Y is written [X® Y] or YX and is called the function-space. Then
PROOF:
LEMMA 3.5.7 Let \funf(-):Á® [X® Y]. If the joins on the right of
|
PROOF:
|
That part (b) above works and this doesn't illustrates the value of unique ness, cf Lemma 1.2.11; ``locally least'' may be good enough, but inserting ``minimal'' doesn't help. omitted diagram environment
COROLLARY 3.5.9 Let Y be a poset with all joins of shape Á.
So far we have been discussing the poset of all monotone functions, which is not what we want for domains. Abusing notation, we also write [X® Y] for the poset of Scott-continuous functions from X to Y, with the pointwise order, X and Y now being dcpos. Recall that pointwise joins gave joins of functions.
PROPOSITION 3.5.10 The same holds with [X® Y] reinterpreted to consist only of continuous functions. In particular, [X® Y] is a dcpo, and an ipo with ^[X® Y] = lx.^Y if ^Y exists.
PROOF: From Lemma 3.5.4, if each \funfj preserves Á-indexed joins (for each j Î J), and Új\funfj exists pointwise, then it too preserves Á- indexed joins. Moreover it is the join amongst join-preserving functions. []
Beware that we have not said that ev:[X® Y]xX® Y preserves joins.
Joint continuity Proposition 3.5.2 stated the properties of products of domains analogous to the result preceding it, apart from part 3.5.1(c). This deserves special consideration.
EXAMPLE 3.5.11 The function f:RxR® R defined by
|
There are several ways of reacting to this; in particular Exercise 3.20 shows what is missing in the case of binary meets or joins. For directed joins it turns out that the difficulty does not arise, but perhaps this just shows the poverty of order-theoretic representations of semantics.
LEMMA 3.5.12 The product of two directed, semidirected or confluent (Definition 3.4.1) posets has the same property. Moreover the diagonal function Á® ÁxÁ is cofinal ( Proposition 3.2.10) iff Á is semidirected, whilst the function Á® {*} is cofinal iff Á is inhabited. []
COROLLARY 3.5.13 A function f:Xx Y® Z of two arguments between dcpos is (jointly) continuous iff it is separately continuous. In particular ev:[X® Y]xX® Y is jointly continuous.
PROOF: Let Á be a directed diagram. Since Á® Áx Á is cofinal by Lemma 3.5.4 we have
|
|
We may compute binary meets pointwise if they commute with directed joins; a dcpo with this property is called a preframe. Infinite meets in [X® Y] may exist but need not be computed pointwise.
EXAMPLE 3.5.14 Consider X = Y = [0,1] Ì R (the unit interval) and (with J = N) let \funfn:X® Y by \funfn(x) = xn. The pointwise meet is discontinuous at 1 in both the Cauchy and Scott senses; the constantly 0 function is the meet in the function-space. []
It is common for function-spaces to inherit the properties of the target domain, irrespective of the source, because the function-space is often a subalgebra of a product. We have shown that this is the case for the existence of various classes of joins (see also Exercise 3.21), but there are simple counterexamples to this behaviour for the trichotomy property.
Scott's thesis The origin of the work in these three sections was Dana Scott's unexpected discovery that non-syntactic models of the untyped l-calculus could be constructed from certain topological spaces (1969). These very un-geometrical spaces were algebraic lattices endowed with Scott's topology. Their retracts, known as continuous lattices, also arose from abstract work in topological lattice theory [ GHK+80].
Scott proposed that topological continuity be used as an approximation to computability. There were precedents for this idea in recursion theory around 1955. Yuri Ershov observed the analogy between the lattice of recursively enumerable sets and a topology. The Rice-Shapiro Theorem says that any recursively enumerable set of partial recursive functions ( ie sets of codes such that if one code for a function N\rightharpoonup N belongs to the set then so do all others) is Scott-open. The Myhill-Shepherdson Theorem says that any recursive f:[N\rightharpoonup N]\rightharpoonup [N\rightharpoonup N], as we would write it domain-theoretically, is Scott-continuous.
Christopher Strachey and others applied Scott's work to denotational semantics of programming languages, where the lattice element T was inappropriate. Scott and his followers repeatedly simplified the theory for this new audience, with the result that order theory replaced topology in the formal development. In particular, the term Scott domain came to be applied to any boundedly complete algebraic dcpo X for which \Xfg is countable (Exercise 3.21).
Domain theory can solve, not only fixed point equations (Example 3.3.1), but also type-equations, such as X º [X® X] for the untyped l-calculus. The right hand side may involve any of the type-constructors on ipos in an arbitrarily complicated way, giving a domain of mathematical meanings for objects with functions, case analysis and non-determinism.
Here and in Section 4.7 we interpret the l-calculus , primitive recursion on N and the fixed point operator Y. Gordon Plotkin [Plo77] considered these as a programming language ( PCF), with call-by-name evaluation (Remark 2.3.4). He showed that any program (closed term of type N) whose denotation in IPO is a numeral in LiftN ( ie not ^) terminates with that value, so there is a link back from the semantics to the syntax. This can now be proved by methods like those in Section 7.7.
However, parallel or ( por(yes,^) = yes = por(^,yes)) is also interpreted in IPO, but is not definable in PCF, whose programs execute ``sequentially.'' The tight link is broken for higher order terms, as there exist such terms that can ``recognise'' por as an argument. By adding por and a similar ``existential quantifier'' to PCF, Plotkin was able to extend the correspondence to higher types. Gérard Berry eliminated por with a different notion of ``domain,'' cf Example 4.51, but more complicated examples recur. The sequentiality and ``full abstraction'' problems remained open for two decades; they were solved for PCF in 1994 by Abramsky, Hyland, Jagadeesan and Ong, using games.
Without bounded completeness, function-spaces of algebraic dcpos need not be algebraic. Achim Jung showed that his own L-domains (Exercise 3.34) and Plotkin's SFP domains are the two maximal cartesian closed categories ( ie closed under function-spaces) of algebraic dcpos [Jun90].
The search for cartesian closed or ``convenient'' categories in topology is much older, and equally inconclusive. The function-space SX (where S is the Sierpi\'nski space, Definition 3.4.10) only exists with the properties it should have when X is locally compact, and even when YX exists it need not be locally compact. A famous cartesian closed full subcategory of compact Hausdorff spaces was found by John Kelley [Kel55], and there are other approaches to topology with different notions of function-space. Example 9.4.11(f) shows how a certain generalised function-space first arose geometrically.
Because of the generality of the infinitary joins required in topology, a function may be topologically continuous without being computable. One can add the word ``effective'' throughout the theory, but it seems to me to be very clumsy to bolt together two subjects like this. There ought to be a common axiomatisation, of which the free model would be equivalent to recursion theory, but with another model consisting of certain spaces. Synthetic domain theory abolishes non-computable functions between sets themselves, by refining the underlying logic.
This cannot be done in classical logic, because the extra axioms (such as the Church-Turing thesis) conflict with excluded middle. However, the use of excluded middle so infests existing accounts of mathematical foundations that it was necessary to start from the beginning, although synthetic domain theory is beyond the scope of this book.