Practical Foundations of Mathematics

Paul Taylor

3.5  Products and Function-Spaces

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

(a)
the projections p0:x,y x and p1:x,y y are monotone;

(b)
if a:G X and b:G Y are monotone functions then so is the function a,b:G Xx Y defined by a(-),b(-);

(c)
a function p:XxY Z is (jointly) monotone iff it is monotone in each argument, for each constant value of the other;

(d)
if X and Y are posets, ie their order relations X and Y are antisymmetric, then Xx Y is also a poset. []

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.

(a)
Let x(-),y(-): XxY be a diagram. Then the joins
(Xx Y)

i  
xi,yi = X

i  
xi, Y

i  
yi
coincide in the sense that if one exists then so does the other, and then they are equal.

(b)
If X and Y have all joins of shape then so does XxY.

(c)
The projections p0:x,y x and p1:x,y y preserve joins.

(d)
If a:G X and b:G Y preserve joins of shape then so does the pair a,b:G XxY.

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



i  


j J 
xi,j =

-20mui ,j x J-20mu 
xi,j =

j J 


i  
xi,j,
then so is the one in the middle and then they are equal.

PROOF: Assuming that the intermediate joins exist, for q X,


"i.  q

j J 
xi,j

"i,j.  q xi,j

"j.  q

i  
xi,j
and each of these is equivalent to q lying above the corresponding join. Substituting each of the three joins for q, they must be equal. []

Pointwise meets and joins  

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

(a)
ev:[X Y]x X Y, given by f,x f(x), is monotone;

(b)
if p:GxX Y is monotone then so is \expx p:G [X Y], defined by lx.p (-,x);

(c)
[X Y] is a poset, ie the pointwise order is antisymmetric, if Y is.

PROOF:

(a)
[[a]] If f,x1 g,x2 then f g and x1 x2, so using the pointwise order, monotonicity and transitivity, we have a square omitted diagram environment

(b)
[[b]] Joint monotonicity implies separate.

(c)
[[c]] f g f iff "x: X.f(x) Y g(x) Y f(x) whilst f = g iff "x: X.f(x) = g(x) . []

EXAMPLES 3.5.6

(a)
[X W], where X is a set with the discrete order and W is the type of propositions, is isomorphic to the powerset P(X) under inclusion.

(b)
[Xop W], where X is a poset, is isomorphic to shv(X), the lattice of lower sets (Definition 3.1.7).

(c)
Similarly [X W]op is the lattice of upper sets (Example 3.1.6(f)).

(d)
[X LiftY], where X and Y are (discrete) sets and LiftY carries the information order (Definition  3.3.7), is isomorphic to the poset of partial functions X\rightharpoonup Y with the extension order (Definition  3.3.3).

LEMMA 3.5.7 Let \funf(-): [X Y]. If the joins on the right of

[X Y]

i  
\funfi = lx. Y

i  
\funfi(x)
exist then so does the join on the left, and the equation holds.

PROOF:

(a)
If we have {\funfi|i:} q (in particular if the function q is the join) then each set { \funfi(x)|i:} has an upper bound, namely q(x):
if $q."x."i.\funfi(x) q(x) then "x.$u."i.\funfi(x) u.

(b)
The function p:x \Xi (\funfi(x )), if it exists, is monotone, because if x x then " i.\funfi(x) \funfi(x) p(x) and so since p(x) is the least upper bound we have p(x) p(x). It follows that p is the join of the functions. []

REMARK 3.5.8

(a)
However, knowing that there is some {\funfi(x)|i: } \argux for each x X is not sufficient to give a bound for the set of functions, because x \argux need not be monotone. Indeed we need the axiom of choice (Definition  1.8.8) even to make this exist as a function.

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

(b)
Let q be a monotone upper bound of the two functions illustrated, so q(1) = f(1) = g(1), but q(0) must also take this value. This constant function is therefore the least upper bound in the function-space, but as q(0)\not u it is not the pointwise least upper bound. []

COROLLARY 3.5.9 Let Y be a poset with all joins of shape .

(a)
Then [X Y] also has all joins of shape  , computed pointwise;

(b)
ev(-,x) preserves them for each x;

(c)
of course ev(f,-) f preserves them iff f does;

(d)
for p:GxX Y, if p(-,x) preserves such joins for each x X then so does \expx p:G [X Y] by lx.p(-,x). []

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

f(x,y) = 2 x y x2+y2        except for f(0,0) = 0
is continuous in x for each fixed value of y and vice versa , but it is not continuous at (0,0) as a function of two variables. []

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

\dirsupdisplayixi,yi = \dirsupdisplayi,jxi,yj = \dirsupdisplayixi,\dirsupdisplayjyj
and separate continuity of f(-, yj) and f(xi,-) gives
f
\dirsupdisplayixi,\dirsupdisplayjyj
= \dirsupdisplayi f
xi,\dirsupdisplayjyj
= \dirsupdisplayi\dirsupdisplayj f(xi,yj),
whence joint continuity follows by cofinality again. []

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.