10.dvi @ Applied General TopologyUniversidad Polit�ecnica de ValenciaVolume 1, No. 1, 2000pp. 129 - 152 On domains witnessing increase ininformationDieter SpreenAbstract. The paper considers algebraic directed-completepartial orders with a semi-regular Scott topology, called regulardomains. As is well known, the category of Scott domains andcontinuous maps is Cartesian closed. This is no longer true, ifthe domains are required to be regular. Two Cartesian closedsubcategories of the regular Scott domains are exhibited: regulardI-domains with stable maps and strongly regular Scott domainswith continuous maps. Here a Scott domains is strongly regular ifall of its compact open subsets are regular open. If one considersonly embeddings as morphisms, then both categories are closedunder the construction of dependent products and sums. More-over, they are !-cocomplete and their object classes are closedunder several constructions used in programming language seman-tics. It follows that recursive domains equations can be solved andmodels of typed and untyped lambda calculi can be constructed.Both kinds of domains can be used in giving meaning to program-ming language constructs.2000 AMS Classi�cation: 68Q55, 06B35, 03B15, 03B40, 18B30Keywords: Scott domains, dI-domains, semi-regular topology, programminglanguage semantics, recursive domain equations, dependent product, dependentsum, lambda calculus 1. IntroductionDomains and domain-theoretic models of the lambda calculus were discoveredby Dana Scott [12] in the fall of 1969 when he was working with ChristopherStrachey at Oxford on the semantics of programming languages. In developinghis approach he built on well understood ideas from recursive function theoryusing higher type functionals. But while people in this area were mainly inter-ested in total functions, he started right away to consider also partial objects.Similar work was done by Yuri L. Ershov [6] in Russia at nearly the same time.He too was motivated by the theory of functionals in computability theory. 130 Dieter SpreenA domain is a structure modelling the notion of approximation and of com-putation. A computation performed using an algorithm proceeds in discretesteps. After each step there is more information available about the result ofthe computation. In this way the result obtained after each step can be seen asan approximation of the �nal result.To be a bit more formal, a domain is a structure having one binary relationv, a partial order, often called information order, with the intended meaningthat x v y just in case x is an approximation of y or y contains at least asmuch information as x. We also require that a domain should include a leastelement modelling no information. To guarantee the existence of the result ofa computation, that is, of a consistent set of approximations, every directedsubset of a domain must have a least upper bound. Directed subsets containconsistent information. The information contained in a �nite set of elements isconsistent, if the set is bounded from above.In any step of a computation a computing device can process at most a �niteamount of information. Domain elements containing only �nite information arecalled compact. We shall consider only algebraic domains in this paper. Thismeans that every point is the least upper bound of all compact elements belowit.As has already been said, for elements x and y of a domain, x v y meansthat y contains at least the information contained in x. In this paper we areinterested in domains with the property that if the information contained ina compact element can be enlarged, then it can be enlarged in at least twoessentially di�erent ways. This means that for any two distinct compact ele-ments x and y with x v y there is a further compact element z above x whichis inconsistent with y. It follows in this case that x < y not only indicatesthat y properly includes the information contained in x, but that there is alsoa witness for this, namely a point z with x v z such that y and z are notbounded from above. This excludes situations in which x < y, but x uniquelydetermines y.Each domain comes with a canonical order-consistent topology, the Scotttopology. It turns out that the just mentioned requirement on the informationorder is equivalent to the fact that the Scott topology is semi-regular. Therefore,we call domains satisfying the above condition regular. It is the aim of thispaper to show that large subclasses of regular domains have su�cient closureproperties so that they can be used for de�ning the meaning of programminglanguage constructs.As we shall see, both the separated and the coalesced sum of families of (atleast two) regular domains are regular again. The same holds for the prod-uct and|in the case of �nite families|for the smash product. Moreover, thecategory of regular domains with embedding/projections as morphisms is !-cocomplete: the inverse limit of any !-cochain of regular domains is regularagain. In addition, this category is closed under the construction of dependentsums. On domains witnessing increase in information 131An important closure property needed for the interpretation of programminglanguages that allow procedures taking functions as inputs is closure under thefunction space construction. As is well known, the class of algebraic domainsis not closed under this construction. Therefore, one usually restricts oneself tothe subclass of Scott domains, when giving meaning to programming languageconstructs. Unfortunately, the Scott domain of continuous maps between tworegular Scott domains need not be regular again. However, we shall present twosubclasses of the regular Scott domains that are closed under the correspondingfunction space construction.First, we consider the subclass of regular dI-domains. dI-domains have beenintroduced by G�erard Berry [4] in order to show that certain continuous mapsare not lambda de�nable. With stable maps as morphisms their category isCartesian closed. The same is true for the full subcategory of regular dI-domains. We show more generally that the category of dI-domains and rigidembedding/projections is closed under the construction of dependent products.Since the dI-domains are also closed under the other constructions mentionedabove, regular dI-domains can be used in giving meaning to functional pro-grams. Recursive domain equations have a solution [13] and stable regularmodels for typed and untyped lambda calculi can be constructed [2].The second way we take is to strengthen the regularity requirement. Thestronger condition is such that not only all basic Scott open sets are regularopen, but all �nite unions of such sets. These are exactly the compact opensubsets of the domain. We call domains satisfying the stronger requirementstrongly regular. As we shall see, this class is closed under nearly all the do-main constructions mentioned earlier. Moreover, we show that the category ofstrongly regular Scott domains and embedding/projections is closed under theconstruction of dependent products. It follows that the category of stronglyregular Scott domains with continuous maps as morphisms is Cartesian closed.Thus, strongly regular Scott domains too are well suited for de�ning the se-mantics of programming languages. Again, recursive domain equations have asolution and strongly regular models for typed and untyped lambda calculi canbe constructed.The paper is organized as follows. In Section 2 regular domains are intro-duced. An example is given showing that the category of regular Scott domainswith continuous maps is not Cartesian closed. In the next two sections, twoCartesian closed subcategories are exhibited.First, in Section 3, regular dI-domains are considered and then, in Section 4,strongly regular Scott domains. In both cases it is proved that the categories ofthese domains with embedding/projections as morphisms are closed under theconstruction of dependent products. Further closure properties of the regularand the strongly regular domains are studied in Section 5. Some �nal remarksappear in Section 6. 132 Dieter Spreen2. Regular domainsLet (D;v) be a partial order with smallest element ?. We write x < y, ifx v y and x 6= y. For a subset S of D, #S = fx 2 D j (9y 2 S)x v y g and"S = fx 2 D j (9y 2 S)y v xg, respectively, are the lower and the upper setgenerated by S. The subset S is called consistent if it has an upper bound. S isdirected, if it is nonempty and every pair of elements in S has an upper boundin S. D is a directed-complete partial order (cpo) if every directed subset Sof D has a least upper bound FS in D, and D is bounded-complete if everyconsistent subset has a least upper bound in D. In particular, if a pair fx;yg isconsistent this is denoted by x " y. In a bounded-complete cpo any consistentpair fx;yg has a least upper bound which is written as x t y.An element x of a cpo D is compact if for any directed subset S of D therelation x v FS always implies the existence of an element u 2 S with x v u.We write K(D) for the set of compact elements of D. If for every y 2 D theset #fyg \ K(D) is directed and y = F#fyg \ K(D), the cpo D is said to bealgebraic and !-algebraic, if, in addition, K(D) is countable. Note that insteadof algebraic cpo we also say domain. Standard references for domain theoryand its applications are [8, 7, 1, 14, 2].Let us �rst consider some examples. For a set A such that ? =2 A setA? = A [ f?g and order it by the at ordering x v y if x = ? or x = y.Obviously, all elements of A? are compact. Thus, A? is a domain.A further example of a domain is the set P(!) of sets of natural numbers,ordered by set inclusion. Here, the �nite sets are exactly the compact elements.The cpo of lazy natural numbers is the set!L = fsn(?) j n 2 ! g [ fsn(0) j n 2 ! g [ fs!(?)gwith s0(?) = ? and s0(0) = 0, ordered byx v y , x = ? _ x = y _ [x = sm(?) ^ (9z)y = sm(z)]:Note that the last case includes y = s!(?), setting s!(?) = sm(s!(?)). In thiscase all elements except s!(?) are compact and s!(?) is the least upper boundof all sm(?) with m 2 !.Other examples are the Cantor domain, that is the set of all �nite andin�nite sequences of 0's and 1's, ordered by the pre�x ordering, and the Bairedomain, that is the set of all �nite and in�nite sequences of natural numbers,also ordered by the pre�x ordering. In both cases the �nite sequences are thecompact elements.The product D � E of two cpo's D and E is the Cartesian product of theunderlying sets ordered coordinatewise. Obviously, K(D �E) = K(D) �K(E).As is well known, on each cpo there is a canonical topology: the Scott topol-ogy. A subset X is open, if it is upwards closed with respect to v and intersectseach directed subset of D of which it contains the least upper bound. In casethat D is algebraic, this topology is generated by the sets "fzg with z 2 K(D).Let us now introduce the class of domains we want to study in this paper. On domains witnessing increase in information 133De�nition 2.1. A domain D is regular if for all u;v 2 K(D)u 6v v ) (9z 2 K(D))v v z ^ u "� z:Note that all domains mentioned in the examples above are regular, exceptin the case of domains A? where A is a singleton. Moreover, the product oftwo regular domains is regular again. If D is bounded-complete, the abovecondition can be simpli�ed.Lemma 2.2. Let D be a bounded-complete domain. Then D is regular if andonly if for all u;v 2 K(D)v < u ) (9z 2 K(D))v v z ^ u "� z:Proof. The \only if" part is obvious. For the \if" part only the case that u andv are not comparable with respect to the partial order has to be considered.If u "� v take z = v. In the opposite case the least upper bound x of u and vexists, which is compact as well. Thus, there is some z 2 K(D) such that v v zand x "� z. It follows that also u "� z. �This shows for two elements u and v of a regular bounded-complete domaincontaining �nite information that if u contains more information than v, thenthere is a witness for this, that is, an element containing at least as muchinformation as v, but the information contained in which is inconsistent withthe information contained in u.As we shall show next, the regularity of a domain, which was de�ned viathe partial order, can also be expressed in topological terms. For a subset Xof D let int(X), cl(X) and ext(X), respectively, be the interior, the closureand the exterior of X with respect to the Scott topology. Then X is regularopen if X = int(cl(X)). Moreover, D is semi-regular if all basic open sets"fzg with z 2 K(D) are regular open. Note that for z 2 K(D), ext("fzg) =Sf"fz0g j z0 2 K(D) ^ z0 "� z g.Lemma 2.3. Let D be a domain with compact element u. Then the followingtwo statements are equivalent:(1) (8v 2 K(D))[u 6v v ) (9z 2 K(D))v v z ^ u "� z].(2) The set "fug is regular open.Proof. In order to see that (1) implies (2), assume that there is some v 2int(cl("fug))n"fug. Then u 6v v. Because of (1) there exists some z 2 K(D)with v v z such that fu;zg is not consistent. It follows that z 2 int(cl("fug)).Hence z 2 cl("fug), which implies that "fzg intersects "fug. Thus, u and zhave a common upper bound, contradicting what has been said about u and zbefore.For the proof that (1) is a consequence of (2) let v 2 K(D) such that u 6v v.Since "fug is regular open, it follows that v 2 ext("fug), which means thatfu;vg cannot be consistent. �Corollary 2.4. A domain is regular if and only if its Scott topology is semi-regular. 134 Dieter SpreenMaps between cpo's are not only required to preserve information but alsocomputations: the value under a map of the result of a computation shouldnot contain more information than what is obtained from the approximatingobjects.De�nition 2.5. Let D and E be cpo's. A map f : D ! E is said to be Scottcontinuous if it is monotone and for any directed subset S of D,f(GS) = Gf(S):It is well known that Scott continuity coincides with topological continuity.Therefore, in what follows we use the shorter term continuous instead of Scottcontinuous.Denote the collection of all continuous maps from D to E by [D ! E].Endowed with the pointwise order, that is, f vp g if f(x) v g(x) for all x 2 D,it is a cpo again. Since [D ! E] need not be algebraic, even if D and E are, oneconsiders subclasses of domains which have this property, when using domainsin programming language semantics, e.g. Scott domains.De�nition 2.6. A Scott domain is a bounded-complete !-algebraic cpo.As is widely known, the category SD of Scott domains and continuous maps isCartesian closed: the one-point domain f?g is the terminal object, the domainproduct is the categorical product and the space of continuous maps betweentwo Scott domains is the categorical exponent.For two Scott domains D and E and elements d 2 K(D) and e 2 K(E) de�nethe step function (d & e): D ! E by(d & e)(x) = (e if d v x,? otherwise.Then the compact elements of [D ! E] are exactly the maps of the formFf(di & ei) j i � ng, where d0; : : : ;dn 2 K(D) and e0; : : : ;en 2 K(E) sothat whenever I � f0; : : : ;ng is such that fdi j i 2 I g is consistent, then sois fei j i 2 I g.The next example shows that in general the function space [D ! E] of tworegular Scott domains D and E need not be regular again.Example 2.7. Consider the Scott domains D and E de�ned by the followingdiagrams: d3 @@ @ @@ @ @ d4 ~ ~~ ~~ ~ ~ @@ @ @@ @ @ d5 ~ ~~ ~~ ~ ~ d1 @@ @@ @ @@ d2 ~~ ~ ~~ ~~ d0 D e3 BB BB BB BB e4 || || || || e1 BB BB BB BB e2 || || || || e0 E On domains witnessing increase in information 135and de�ne f1, f2 2 [D ! E] by f1 = (d2 & e1) and f2 = (d1 & e1) t (d5 &e1). Then both maps are compact. Obviously, f1 and f2 are not comparablewith respect to the pointwise order, but have a common upper bound, thatis, f2 2 cl("ff1g). We want to show now that "ff2g is included in cl("ff1g),which implies that "ff1g is not regular open. Assume to this end that thereis some f 2 [D ! E] with f2 vp f and f1 "� f. Then e1 v f(y), if d1 v yor y = d5. Moreover, there is some z 2 D such that f1(z) and f(z) have nocommon upper bound. Then d2 v z, since for z 2 D with d2 6v z we have thatf1(z) = e0 v f(z). Moreover z 62 fd4;d5g. Thus z = d2, which implies thatfz;d1g and hence also ff(z);f(d1)g are consistent. It follows that f(z) 6= e2,from which we obtain that f1(z) and f(z) have a common upper bound, incontradiction to our assumption. Hence "ff2g is a subset of cl("ff1g).In the following sections we introduce two subclasses of the regular Scottdomains which are closed under the construction of function spaces. As weshall see moreover, they are also closed under several other constructions usedin denotational semantics. To this end we need the following de�nitions.De�nition 2.8. An embedding/projection (f;g) from a cpo D to a cpo E isa pair of continuous maps f : D ! E and g : E ! D such that g � f = idD, theidentity map on D, and f � g vp idE. The map f is called embedding and gprojection.Normally, we write an embedding/projection as (fL;fR). Note that the mapfR is uniquely determined by fL, and vice versa [13]. Embeddings are one-to-one and preserve compactness as well as least upper bounds of �nite consistentsets of domain elements [11]. Moreover, both the embedding and the projectionare strict, that is, they map least elements onto least elements.Suppose (fL;fR) is an embedding/projection from C to D and (gL;gR) isan embedding/projection from D to E. Then the composition of (fL;fR) and(gL;gR) is de�ned by(gL;gR) � (fL;fR) = (gL � fL;fR � gR):Let SDep denote the category of Scott domains and embedding/projections.Any partially ordered set may be viewed as a category. For a cpo D, thisis done by letting the objects of the category be the elements of D and lettingthe morphism set between objects x and y be the one-point set f�x;yg preciselywhen x v y and the empty set otherwise.Let F : D ! SDep be a functor. Recall that this means that F(x) is adomain for each x 2 D, and if x v y then F(�x;y) is an embedding/projectionfrom F(x) to F(y) such that F(�x;x) = idF(x), and if x v y and y v z thenF(�x;z) = F(�y;z) � F(�x;y). When x v y we shall use the notation Fx;y forF(�x;y).De�nition 2.9. Let D be a cpo. A functor F : D ! SDep is continuous if forany directed subset S of D, F(FS) is a colimit of the diagram(fF(x) j x 2 S g;fFx;y j x;y 2 S ^ x v y g): 136 Dieter SpreenA section of F is a map f : D ! SfF(x) j x 2 D g with f(x) 2 F(x), for allx 2 D.De�nition 2.10. Let D be cpo and F : D ! SDep be a continuous functor.An section f of F is said to be(1) monotone if FLx;y(f(x)) v f(y), for all x;y 2 D with x v y.(2) continuous if f is monotone and for every directed subset S of D,f(GS) = GfFLx;FS(f(x)) j x 2 S g:3. Regular dI-domainsIn this section we restrict our attention to the subclass of regular dI-domains.De�nition 3.1. A Scott domain D is a dI-domain if it satis�es the two ax-ioms d and I:� Axiom d: For all x;y;z 2 D, if y " z thenx u (y t z) = (x u y) t (x u z):� Axiom I: For all u 2 K(D), #fug is �nite.Note that in a bounded-complete domain any two elements x and y have agreatest lower bound x u y. Moreover, observe that by Axiom I all elements ofa dI-domain below a compact element are also compact.The elements of a dI-domain can be generated by a special kind of compactelements.De�nition 3.2. Let D be a bounded-complete domain. An element u 2 D is acomplete prime if for any consistent subset S of D the relation u v FS alwaysimplies the existence of an element x 2 S with u v x.The complete primes in a dI-domain D turn out to be those compact elementsthat have a unique element below them in the domain order [15]. As followsfrom a result of Winskel, every element in D is the least upper bound of allcomplete primes below it.In the context of dI-domains it is usual to work with embedding/projectionsthat satisfy an additional requirement.De�nition 3.3. An embedding/projection (f;g) from a dI-domain D to a dI-domain E is rigid if for all x 2 D and y 2 E with y v f(x), f � g(y) = y. Themap f is called rigid embedding and g rigid projection.Note that rigid embeddings preserve greatest lower bounds of �nite sets ofdomain elements. Moreover, they map complete primes onto complete primes.As a consequence of this, rigid projections preserve the least upper bounds of�nite consistent sets of domain elements. We denote the category of dI-domainsand rigid embedding/projections by DIrep.For the following de�nition observe that for any bounded-complete domainD and elements x;y;z 2 D such that x;y v z, (xuy;�xuy;x; �xuy;y) is a pullbackof (�x;z; �y;z) in D viewed as a category. On domains witnessing increase in information 137De�nition 3.4. Let D be a bounded-complete domain, F : D ! DIrep a func-tor and f a section of F.(1) The functor F is stable if it is continuous and for all x;y;z 2 D withx;y v z, (F(x u y);Fxuy;x;Fxuy;y) is a pullback of (Fx;z;Fy;z).(2) Let F be stable. The section f of F is stable if it is continuous and forall x;y 2 D with x " y,f(x u y) = FRxuy;x(f(x)) u FRxuy;y(f(y)):For the remainder of this section we assume that D is a dI-domain andF : D ! DIrep a stable functor.Proposition 3.5. Let f be a stable section of F. Then for any x 2 D andv 2 K(F(x)) such that v v f(x), there are �u 2 K(D) and �v 2 K(F(�u)) with thefollowing properties:(1) �u v x.(2) v = FL�u;x(�v).(3) �v v f(�u).(4) (8y;z 2 D)[�u;y v z ^ FL�u;z(�v) v FLy;z(f(y)) ) �u v y].Proof. Let x 2 D and v 2 K(F(x)) with v v f(x). Sincef(x) = GfFLu;x(f(u)) j u 2 K(D) ^ u v xg;there is some û 2 K(D) with v v F L̂u;x(f(û)). Because #fûg is �nite, there isa minimal such û, say �u. Thus v v FL�u;x(f(�u)). Observe that F�u;x is rigid.Therefore v = FL�u;x � FR�u;x(v). Set �v = FR�u;x(v). Then �v 2 F(�u) and �v v f(�u).Moreover, �v is compact.Now, let y;z 2 D such that �u;y v z and FL�u;z(�v) v FLy;z(f(y)). Set vy =FRy;z � FL�u;z(�v). Then vy 2 F(y). Moreover, it follows as above that FL�u;z(�v) =FLy;z(vy). Since F is stable, we have that (F(�uuy);F�uuy;�u;F�uuy;y) is a pullbackof (F�u;z;Fy;z). Therefore, there is some v̂ 2 F(�u u y) with FL�uuy;�u(v̂) = �v andFL�uuy;y(v̂) = vy. It follows that v̂ v FR�uuy;�u(f(�u)) u FR�uuy;y(f(y)). Because f isstable as well, we obtain that v̂ v f(�uuy) and hence that v v FL�uuy;x(f(�uuy)).Then �u = �u u y, by the minimality of �u, which implies that �u v y. �This result justi�es the following de�nition.De�nition 3.6. Let f be a stable section of F. The setTr(f) = f(u;v) j u 2 K(D) ^ v 2 K(F(u)) ^ v v f(u)^ (8y;z 2 D)[u;y v z ^ FLu;z(v) v FLy;z(f(y)) ) u v y]gis called trace of f.Lemma 3.7. Let f be a stable section of F. Then the trace of f has thefollowing properties:(1) If (u0;v0); : : : ;(un;vn) 2 Tr(f) such that fu0; : : : ;ung has least upperbound �u, then fFLu0;�u(v0); : : : ;FLun;�u(vn)g has a least upper bound, say �v,and (�u; �v) 2 Tr(f). 138 Dieter Spreen(2) If (u;v) 2 Tr(f), x;z 2 D and v0 2 F(x) such that u;x v z andv0 v FRx;z�FLu;z(v), then there exists u0 v u so that FLx;z(v0) 2 FLu0;z(F(u0))and (u0;FRu0;z � FLx;z(v0)) 2 Tr(f).(3) If (u;v);(u0;v0) 2 Tr(f) and for some z 2 D with u;u0 v z, FLu;z(v) =FLu0;z(v0), then u = u0 and hence v = v0.Proof. (1) If fu0; : : : ;ung has least upper bound �u, then we have for i � n thatFLui;�u(vi) v f(�u). Hence, fFLu0;�u(v0); : : : ;FLun;�u(vn)g has a least upper bound �v.Both, �u and �v are compact. It remains to show that (�u; �v) 2 Tr(f).We have already observed that �v v f(�u). Now, let y;z 2 D with �u;y v zand FL�u;z(�v) v FLy;z(f(y)). Then we have for i � n that ui v z and FLui;z(vi) vFLy;z(f(y)). Since (ui;vi) 2 Tr(f) it follows that ui v y, for i � n, which impliesthat �u v y.(2) Let (u;v) 2 Tr(f) and x;z 2 D with u;x v z. Moreover, let v0 2 F(x)such that v0 v FRx;z � FLu;z(v). Then FLx;z(v0) v FLu;z(v). Since v is compact, wehave that also FLu;z(v) is compact. Hence, FLx;z(v0) is compact as well. Notethat FLx;z(v0) v FLu;z(v) v FLu;z(f(u)) v f(z):Therefore, by Proposition 3.5, there is some (u0; �v) 2 Tr(f) such that u0 v zand FLx;z(v0) = FLu0;z(�v). Because u;u0 v z and FLu0;z(�v) = FLx;z(v0) v FLu;z(f(u)),it follows that u0 v u.(3) If (u;v);(u0;v0) 2 Tr(f) and for some z 2 D with u;u0 v z, FLu;z(v) =FLu0;z(v0), then v0 v f(u0) and thus FLu;z(v) = FLu0;z(v0) v FLu0;z(f(u0)). Since(u;v) 2 Tr(f), it follows that u v u0. In the same way we obtain that u0 v u.Therefore u = u0 and hence FLu;z(v) = FLu;z(v0), which implies that v = v0, asFLu;z is one-to-one. �The next lemma shows how a stable section can be recovered from its trace.Lemma 3.8. (1) A stable section f of F can be computed from its trace inthe following way:f(x) = GfFLu;x(v) j u v x ^ (u;v) 2 Tr(f)g:(2) Every set of pairs (u;v) with u 2 K(D) and v 2 K(F(u)) satisfyingProperties (1)-(3) of Lemma 3.7 is a trace of the stable section of Fde�ned by the formula above.Proof. (1) Because of Property (1) of Lemma 3.7 the set of all FLu;x(v) with(u;v) 2 Tr(f) and u v x is directed and thus has a least upper bound. Obvi-ously, the right-hand side of the formula is less than or equal to the left-handside. If v 2 K(F(x)) with v v f(x), then, by Proposition 3.5, there is some(u0;v0) 2 Tr(f) with u0 v x and v = FLu0;x(v). It follows that v is less than orequal to the right-hand side of the formula. Since f(x) is the least upper boundof all such v, the same is true for f(x). On domains witnessing increase in information 139(2) We have to show that if X satis�es Properties (1)-(3) of Lemma 3.7, thenthe map f de�ned byf(x) = GfFLu;x(v) j u v x ^ (u;v) 2 X g:is a stable section of F with Tr(f) = X.The map f is well de�ned, since the set fFLu;x(v) j u v x ^ (u;v) 2 X g isdirected by Property 3.7(1) and therefore has a least upper bound.Obviously, f is monotone. To see that it is continuous, let S be a directedsubset of D and let v 2 K(F(FS)) with v v f(FS). It follows that there issome (�u; �v) 2 X so that �u v FS and v v FL�u;FS(�v). Since �u is compact aswell, there is some x 2 S with �u v x. Thus FL�u;x(�v) v f(x), which implies thatv v FLx;FS(f(x)). Since f(FS) is the least upper bound of all such v, we havethat f(FS) v FfFLx;FS(f(x)) j x 2 S g. The converse inequality is obvious,by monotonicity.For the veri�cation of stability it su�ces to show for x;y;z 2 D with x;y v zthat FRxuy;x(f(x)) u FRxuy;y(f(y)) v f(x u y). Let to this end (u;v);(u0;v0) 2 Xwith u v x and u0 v y. Since the binary operator u is continuous [7], we onlyhave to verify thatFRxuy;x � FLu;x(v) u FRxuy;y � FLu0;y(v0) v f(x u y):Set �v = FRxuy;x�FLu;x(v)uFRxuy;y �FLu0;y(v0). Then �v v FRxuy;x�FLu;x(v);FRxuy;y �FLu0;y(v0). Hence, by Property 3.7(2), there is some �u v u such that(3.1) FLxuy;x(�v) 2 FL�u;x(F(�u))and (�u;FR�u;x � FLxuy;x(�v)) 2 X. Moreover, there is some �u0 v u0 such that(3.2) FLxuy;y(�v) 2 FL�u0;y(F(�u0))and (�u0;FR�u0;y�FLxuy;y(�v)) 2 X. Note that �u v x v z and �u0 v y v z. In additionFL�u;z � FR�u;x � FLxuy;x(�v) = FLx;z � FL�u;x � FR�u;x � FLxuy;x(�v)= FLx;z � FLxuy;x(�v) (by (3.1))= FLxuy;z(�v)= FL�u0;z � FR�u0;y � FLxuy;y(�v) (by (3.2))By Property 3.7(3) we therefore have that �u = �u0. Thus �u v x u y. It followsthat FR�u;x � FLxuy;x(�v) = FR�u;xuy � FRxuy;x � FLxuy;x(�v) = FR�u;xuy(�v):Since (�u;FR�u;xuy(�v)) 2 X and �v 2 FL�u;xuy(F(�u)), by (3.1), we obtain that �v =FL�u;xuy � FR�u;xuy(�v) v f(x u y).Next, we show that Tr(f) contains X. If (u;v) 2 X then v v f(u). Lety;z 2 D such that u;y v z and FLu;z(v) v FLy;z(f(y)). Since FLu;z(v) is compact,if follows from the de�nition of f that there is some (û; v̂) 2 X with û v y and 140 Dieter SpreenFLu;z(v) v FLy;z � F L̂u;y(v̂). By Property 3.7(2) we now obtain that there exists au0 v û so that(3.3) FLu;z(v) 2 FLu0;z(F(u0))and (u0;FRu0;z �FLu;z(v)) 2 X. Thus, we have that (u;v);(u0;FRu0;z �FLu;z(v)) 2 X,u;u0 v z and, because of (3.3), FLu0;z�FRu0;z�FLu;z(v) = FLu;z(v). Therefore u = u0,by Property 3.7(3). Since u0 v û v y it follows that (u;v) 2 Tr(f).Finally, we have to verify that also X contains Tr(f). Let (u;v) 2 Tr(f).Then v v f(u). As above it follows that there is some u0 v u so that(u0;FRu0;u(v)) 2 X and v 2 FLu0;u(F(u0)). Then v v FLu0;u(f(u0)). As a con-sequence of the minimality condition in the de�nition of a trace we obtain thatu v u0. Thus u = u0, which means that (u;v) 2 X. �De�ne �DF to be the set of all stable sections of F and order it by the stableordering, that is f vs g , Tr(f) � Tr(g):Then �DF with the stable ordering is the dependent product of F over D.Our next goal is to show that �DF is a dI-domain. To this end we need thefollowing lemma.Lemma 3.9. Let f be a stable section of F and I � Tr(f). Moreover, letI0 = f(x;y) 2 Tr(f) j (9(u;v) 2 I)x v u ^ FLx;u(y) v v gand X = f(x;y) 2 Tr(f) j(9(u0;v0); : : : ;(un;vn) 2 I0)x = Fi�n ui ^ y = Fi�n FLui;x(vi)g:Then the following three statements hold:(1) The set X has Properties (1)-(3) of Lemma 3.7.(2) The stable section g de�ned by X according to Lemma 3.8(2) is thesmallest stable section h of F with h vs f and I � Tr(h).(3) If the set I is �nite, so is X.Proof. (1) Property 3.7(1) holds by construction and 3.7(3) is inherited fromTr(f). It remains to show that also 3.7(2) holds. Let (u;v) 2 X and forx;z 2 D with u;x v z let v0 2 F(x) such that v0 v FRx;z � FLu;z(v). Since Xis contained in Tr(f) there is some u0 v u so that FLx;z(v0) 2 FLu0;z(F(u0)) and(u0;FRu0;z � FLx;z(v0)) 2 Tr(f). We show that (u0;FRu0;z � FLx;z(v0)) 2 X.Because (u;v) 2 X, there are (u0;v0); : : : ;(un;vn) 2 I0 so that u = Fi�n uiand v = Fi�n FLui;u(vi). De�ne u0i = ui u u0, for i � n. Then u0 = Fi�n u0i. AsFLx;z(v0) 2 FLu0;z(F(u0)) there exists v̂ 2 F(u0) with FLx;z(v0) = FLu0;z(v̂). Thenv̂ = FRu0;z � FLx;z(v0). For i � n set ~vi = FLui;u(vi) u FLu0;u(v̂). It follows that~vi v FLui;u(vi);FLu0;u(v̂). Therefore FLui;u �FRui;u(~vi) = ~vi = FLu0;u �FRu0;u(~vi). Since On domains witnessing increase in information 141(F(u0i);Fu0i;u0;Fu0i;ui) is a pullback of (Fu0;u;Fui;u), we obtain that there is somev0i 2 F(u0i) with FLu0i;u0(v0i) = FRu0;u(~vi) and FLu0i;ui(v0i) = FRui;u(~vi). ThenFLu0i;ui(v0i) = FRui;u(~vi) v FRui;u � FLui;u(vi) = vi:Thus (u0i;v0i) 2 I0. Moreover, FLu0i;u0(v0i) = FRu0;u(~vi) v FRu0;u � FLu0;u(v̂) = v̂ andGi�n FLu0i;u0(v0i) = Gi�n FRu0;u(~vi)= FRu0;u(Gi�n ~vi)= FRu0;u(Gi�n FLui;u(vi) u FLu0;u(v̂))= FRu0;u(FLu0;u(v̂) u (Gi�n FLui;u(vi)))= FRu0;u(FLu0;u(v̂) u v)= FRu0;u � FLu0;u(v̂)= v̂:Here, we used thatFLu0;u(v̂) = FLu0;u � FRu0;u � FRu;z � FLx;z(v0) v FRu;z � FLx;z(v0) vFRu;z � FLx;z � FRx;z � FLu;z(v) v v:It follows that (u0; v̂) 2 X.(2) Properties 3.7(1)-(3) imply for any stable section h of F with I � Tr(h) �Tr(f) that X � Tr(h).(3) Since embeddings are one-to-one and Axiom I holds in D and all F(x)with x 2 D, it follows that if I is �nite, so is I0. Obviously kXk � 2kI0k.Therefore, also X is �nite in this case. �Theorem 3.10. Let D be a dI-domain and F : D ! DIrep a stable functor.Then �DF is a dI-domain. The compact elements in �DF are exactly thesections with �nite trace.Proof. As is easily seen, �DF is a cpo. If S is a subset of �DF with up-per bound f, then it follows with Lemma 3.9 that the section generated bySfTr(h) j h 2 S g is the least upper bound of S. Thus, �DF is bounded-complete. Obviously, the sections of F with �nite trace are the compact ele-ments. Therefore, �DF is a Scott domain and Axiom I holds. With Lemmas 3.7and 3.8 it is readily veri�ed for two section f and g that Tr(f) \ Tr(g) is thetrace of f ug. By using the two lemmas once more we then obtain that Axiom dis satis�ed as well. �In the special case of a constant functor F , say F(x) = E for x 2 D, onehas the well known fact that the space [D !s E] of stable maps from D to Eis a dI-domain again. Indeed, the category of dI-domains and stable maps isCartesian closed [7]. 142 Dieter SpreenNow, let RDIrep be the category of regular dI-domains and rigid embed-ding/projections. We will show that for a stable functor F : D ! RDIrep thedependent product domain �DF is also regular.Theorem 3.11. Let D be a dI-domain and F : D ! RDIrep a stable functor.Then �DF is a regular dI-domain.Proof. We only have to verify the condition in Lemma 2.2. Let f;g 2 K(�DF).Since Tr(f) is �nite, we have that f("fug) is �nite as well. Hence there is somex 2"fug so that for all z 2 D with x v z, FLx;z(f(x)) = f(z). Obviously, we canassume that x is compact. By the formula in Lemma 3.8(1) we moreover obtainthat there is some (û; v̂) 2 Tr(f) with û v x and f(x) = F L̂u;x(v̂). BecauseF L̂u;x(v̂) v F L̂u;x(f(û)) v f(x) = F L̂u;x(v̂);we also have that f(û) = v̂. Let y = f(x).Now, suppose that f < g. Then Tr(f) & TrL(g). Thus, there is some(u;v) 2 Tr(g) n Tr(f).Claim 3.12. FLu;x(v) 6v y.Proof. Assume that v v FRu;x � F L̂u;x(v̂). By Property 3.7(2) there is then someu0 v û so that FLu;x(v) 2 FLu0;x(F(u0)) and (u0;FRu0;x � FLu;x(v)) 2 Tr(f). Itfollows that (u0;FRu0;x � FLu;x(v)) 2 Tr(g). Since (u;v) 2 Tr(g) as well andFLu0;x �FRu0;x �FLu;x(v) = FLu;x(v), we obtain with Property 3.7(3) that u = u0 andFRu0;x � FLu0;x(v) = v. Hence (u;v) 2 Tr(f), a contradiction.This shows that v 6v FRu;x � F L̂u;x(v̂), which implies that FLu;x(v) 6v F L̂u;x(v̂) =y. �Claim 3.13. (u0;v0) 2 Tr(f) ^ u0 " x ) u0 v x ^ FLu0;x(v0) v y.Proof. With u0 " x we also have that u0 " û. Then (u0 t û;FLu0;u0tû(v0) tF L̂u;u0tû(v̂)) 2 Tr(f), by 3.7(1). HenceF L̂u;u0tx(v̂) v FLu0tû;u0tx(FLu0;u0tû(v0) t F L̂u;u0tû(v̂))v FLu0tû;u0tx(f(u0 t û))v f(u0 t x)= F L̂u;u0tx(v̂);(3.4)which implies that FLu0;u0tû(v0) t F L̂u;u0tû(v̂) = F L̂u;u0tû(v̂). With 3.7(3) we thushave that û = u0 t û, that is, u0 v û v x. Therefore, we obtain from (3.4) thatFLu0;x(v0) v F L̂u;x(v̂) = y. �Since F(x) is regular and FLu;x(v) 6v y there is some �v 2 K(F(x)) so thaty v �v and FLu;x(v) "� �v. De�neX = Tr(f) [ f(x; ~v)~v 2 K(F(x)) ^ ~v v �v^(@(�u; �v) 2 Tr(f))�u v x ^ FL�u;x(�v) = ~vg: On domains witnessing increase in information 143If we have checked that X has Properties 3.7(1)-(3), we know that X is thetrace of a section �f 2 K(�DF) with f vs �f. Suppose that g; �f vs h, forsome h 2 �DF . Then FLu;x(v) v g(x) v h(x) and �v = �f(x) v h(x), which isimpossible as FLu;x(v) "� �v. Thus g "� �f.It remains to check that X has the properties of Lemma 3.7.(1) Obviously, it is su�cient to consider the case that n = 1. Let (u0;v0),(u1;v1) 2 X so that fu0;u1g is consistent. If (u0;v0);(u1;v1) 2 Tr(f) we aredone. So, without restriction, let us assume that (u0;v0) =2 Tr(f). Then u0 = xand v0 v �v. If (u1;v1) =2 Tr(f) too, then u1 = x and v1 v �v. In the oppositecase we obtain with Claim 3.13 that u1 v x and FLu1;x(v1) v �v. Therefore, inboth cases v0 t FLu1;x(v1) exists below �v.In order to see that (x;v0 t FLu1;x(v1)) 2 X n Tr(f) assume that there issome (�u; �v) 2 Tr(f) such that �u v x and FL�u;x(�v) = v0 t FLu1;x(v1). Thenv0 v FL�u;x(�v). With Property 3.7(2) it follows that there is some u0 v �u so thatv0 2 FLu0;x(F(u0)) and (u0;FRu0;x(v0)) 2 Tr(f). Hence, we have that u0 v x andFLu0;x � FRu0;x(v0) = v0, contradicting the fact that (u0;v0) 2 X n Tr(f).(2) We only have to consider the case that (x; ~v) 2 X n Tr(f), z;z0 2 D andv0 2 F(z) such that x;z v z0 and v0 v FRz;z0 � FLx;z(~v). Then FRx;z0 � FLz;z0(v0) v~v v �v.If there is some (�u; �v) 2 Tr(f) with �u v x and FL�u;x(�v) = FRx;z0 � FLz;z0(v0), itfollows that �u;z v z0. Moreover FLz;z0(v0) v FLx;z0(~v). Since the embeddings arerigid, we therefore obtain thatFL�u;z0(�v) = FLx;z0 � FL�u;x(�v) = FLx;z0 � FRx;z0 � FLz;z0(v0) = FLz;z0(v0):Hence FLz;z0(v0) 2 FL�u;z0(F(�u)). As �v = FR�u;z0 � FLz;z0(v0), we have that (�u;FR�u;z0 �FLz;z0(v0)) 2 Tr(f). But Tr(f) is contained in X.In the opposite case we obtain that (x;FRx;z0 � FLz;z0(v0)) 2 X n Tr(f). Notehere that we have already seen that FLz;z0(v0) v FLx;z0(~v), which implies thatFLz;z0(v0) 2 FLx;z0(F(x)).(3) Let (u0;v0);(u1;v1) 2 X such that u0;u1 v z and FLu0;z(v0) = FLu1;z(v1),for some z 2 D. The case that both pairs are contained in Tr(f) is obvious.Without restriction let (u0;v0) 2 X n Tr(f). Then u0 = x. If (u1;v1) 2 Tr(f)we obtain with Claim 3.13 that u1 v x, contradicting the fact that (u0;v0) 2X n Tr(f). Hence (u1;v1) 2 X n Tr(f), which means that also u1 = x. �As a special case we obtain that the dI-domain of stable maps from a dI-domain to a regular dI-domain is regular again [9].Theorem 3.14. The category of regular dI-domains and stable maps is Carte-sian closed. 4. Strongly regular Scott domainsIn this section we consider Scott domains which satisfy a strengthened reg-ularity condition. 144 Dieter SpreenDe�nition 4.1. A domain D is strongly regular, if every �nite union of basicopen sets "fzg with z 2 K(D) is regular open.Note that in the Scott topology the �nite unions of basic opens are just thecompact open subsets of the domain. By Lemma 2.3 every strongly regulardomain is regular. Among the examples given in Section 2 only the domainsA? generated by �nite nonempty sets A are not strongly regular.The following characterization will turn out to be useful in the remainder ofthis section. We call a subset S of K(D) subbasis, if every compact element ofD is the least upper bound of a �nite subset of S.Lemma 4.2. Let S be a subbasis of a domain D. Then the following threestatements are equivalent:(1) D is strongly regular.(2) For any subset X of S and all v 2 K(D) the next condition holds:(8u 2 X)u 6v v ) (9z 2 K(D))[v v z ^ (8u 2 X)u "� z]:(3) For any �nite subset X of S, Sf"fzg j z 2 X g is regular open.Proof. In order to see that (1) implies (2), let X be a �nite subset of S andv 2 K(D) such that for all u 2 X, u 6v v. Since Sf"fug j u 2 X g is regularopen, it follows that "fvg intersects ext(Sf"fug j u 2 X g). Hence, there issome z 2 K(D) such that v v z and for all u 2 X, u "� z.For the proof that (3) follows from (2), let X be a �nite subset of S and setU = Sf"fug j u 2 X g. Moreover, assume that there is some v 2 int(cl(U))nU.Then we have for all u 2 X that u 6v v. Because of (2) there exists some z 2K(D) such that v v z and for all u 2 X, z "� u. It follows that z 2 int(cl(U)).Hence z 2 cl(U), which implies that "fzg intersects U. Thus, for some u 2 X,u and z have a common upper bound. This contradicts what has been saidabout z before.It remains to show that (1) is a consequence of (3). Let Y be �nite subsetof K(D). Then for any y 2 Y there is some �nite subset Xy of S such y is theleast upper bound of Xy. Thus[f"fyg j y 2 Y g = [fTf"fug j u 2 Xy g j y 2 Y g:By distributivity it follows that Sf"fyg j y 2 Y g is a �nite intersection over�nite unions of basic open sets "fzg with z 2 S. Since every such �nite unionis regular open by (3), and the class of regular open sets is closed under �niteintersections, we obtain that Sf"fyg j y 2 Y g is regular open. �It follows that a domain is strongly regular, exactly if every compact elementthat does not extend �nitely many given compact elements ui can be extendedto a compact element which contains additional information, contradictory tothe information coded into the ui.We will now consider the dependent product of a continuous family of Scottdomains. Let to this end D be Scott domain and F : D ! SDep a continuousfunctor. On domains witnessing increase in information 145De�ne �DF to be the set of all continuous sections of F , and order �DFpointwise, that is, letf vp g , (8x 2 D)f(x) vF(x) g(x):Then �DF with the pointwise order is the dependent product of F over D.As will follow from the next theorem the sections (u & v) with u 2 K(D)and v 2 K(F(u)) form a subbasis of �DF . Here (u & v) is de�ned by(u & v)(x) = (FLu;x(v) if u v x,?F(x) otherwise.The following result has been established in [5, 10].Theorem 4.3. Let D be a Scott domain and F : D ! SDep a continuous func-tor. Then �DF is a Scott domain. The compact elements are exactly the leastupper bounds of �nite consistent sets of sections of the form (u & v).Let SRSDep be the category of strongly regular Scott domains and embed-ding/projections, let D be strongly regular and F : D ! SRSDep. We shallshow next that �DF is also strongly regular. We do this by using an idea ofU. Berger, to which the next lemma is due as well.Lemma 4.4. Let D be strongly regular and u0; : : : ;un�1;v0; : : : ;vm�1 2 K(D).Moreover, let all vj be pairwise distinct. Then there exist z0; : : : , zm�1 2 K(D)with the following properties:(1) (8j < m)vj v zj.(2) (8j < m)(8i < n)[ui 6v vj ) ui "� zj].(3) (8j1;j2 < m)[j1 6= j2 ) zj1 "� zj2].Proof. The lemma will be proved by induction on m. The case m = 0 is trivial.Therefore, let m > 0. Moreover, without restriction, let vm�1 be minimalamong v0; : : : ;vm�1. SetX = fy 2 fu0; : : : ;un�1;v0; : : : ;vm�2g j y 6v vm�1 g:Since D is strongly regular, there is some zm�1 2 K(D) such that vm�1 v zm�1and y "� zm�1, for all y 2 X. Thus Properties (1) and (2) hold for j = m � 1.Because vm�1 is minimal and the vj are pairwise distinct, we moreover havethat vj "� zm�1, for j < m � 1.Now, by applying the induction hypothesis to u0; : : : ;un�1 and v0; : : : , vm�2we obtain that there are z0; : : : ;zm�2 2 K(D) such that Properties (1)-(3) hold.Because of our choice of zm�1 (1) and (2) then also hold for z0; : : : ;zm�1. ForProperty (3) we only have to show that for all j < m � 1, zj "� zm�1. Assumethat zj " zm�1, for some j < m�1. Since vj v zj, it then follows that vj " zm�1as well, which is impossible by our choice of zm�1. �Theorem 4.5. Let D be a strongly regular Scott domain and F : D ! SRSDepa continuous functor. Then �DF is strongly regular. 146 Dieter SpreenProof. We verify Condition (2) in Lemma 4.2 for the subbasisS = f(u & y) j u 2 K(D) ^ y 2 K(F(u))g:Let to this end gi;a = (ui & yai ) 2 S (i < n, a < bi) such that u0; : : : ;un�1 arepairwise distinct, let f = Ff(vj & zj) j j 2 J g 2 K(�DF), and assume thatgi;a 6vp f, for i < n and a < bi. We have to construct a section h 2 K(�DF)with f vp h and h "� gi;a, for i < n and a < bi.Obviously, gi;a 6vp f if and only if yai 6v f(ui). Since every domain F(ui)is strongly regular, there is some ~yi 2 K(F(ui)), for each i < n, such thatf(ui) v ~yi and yai "� ~yi, for all a < bi. Because D is strongly regular too, itfollows with the preceding lemma that there are �u0; : : : ; �un�1 2 K(D) such thatthe following properties hold:(1) (8i < n)ui v �ui.(2) (8i < n)(8j 2 J)[vj 6v ui ) vj "� �ui].(3) (8i1; i2 < n)[i1 6= i2 ) �ui1 "� �ui2].For i < n let �yi = FLui;�ui(~yi). We shall show now that the set f(�ui & �yi) j i