g if and only if f(a) £ g(a) for all a Î L. The following straightforward result shows that Frm [L,M] is a DCPO.
(See Johnstone [13], Lemma 1.11, p. 47 for a proof.)
| Abstract |
This paper sets two goals. The first is to present algebraists with a purely order-theoretic derivation of the adjunction between the category DCPO of DCPOs (directed complete posets) and the category Frm of frames. This adjunction restricts to several Stone-type dualities which are well-known and of considerable interest to computer scientists. The second goal is to describe the object classes of these subdualities in terms familiar to algebraists, thereby making a large body of literature about them more accessible.
Since their introduction in the pioneering work of D. S. Scott and C. Strachey, the appealing properties of the posets used in denotational semantics have been expanded by logicians and theoretical computer scientists into a rapidly growing discipline called domain theory. The richness of the new field is attracting increasing numbers of mathematicians (present authors included) whose interests have previously lain outside of theoretical computer science. This paper is written with these people in mind. There are few survey papers or monographs devoted exclusively to the mathematical theory of domains. The recent monograph by Abramsky and Jung [2] and the text by Vickers [36] being exceptions. The beginner not versed in computer science who attempts to understand the theory is often confronted by interconnected, alternative approaches and unfamiliar literature and folklore. Our aim in this paper is to provide the reader, algebraists in particular, with some familiar ground from which the primary concepts of the field may be studied and appreciated.
We accomplish this aim in three steps. First, in Section 2, we provide the reader with a detailed account of the motivations behind the use of the most general posets appearing in domain theory and then, in Section 3, present a purely order-theoretic derivation of one of the field's key features: the contravariant adjunction between the categories DCPO and Frm . Second, in Section 4, we restrict the primary adjunction and use mostly lattice- theoretic techniques to obtain the important Stone-type duality between algebraic posets and bialgebraic frames. In Section 5, we provide an example of the relevance to algebraists of the objects studied in domain theory by connecting many classes of them to well-known classes of lattices and by showing that the object assignments of the duality in Section 4 yield new insights into the structure of the prime spectrum of distributive lattices. Finally, in Section 6, we further restrict this duality to categories of particular interest to denotational semantics.
Most of the results in this paper have appeared elsewhere - the novelty lies in the approach taken to their proofs. The categorical correspondences considered are usually derived from a topological viewpoint (see, for example Abramsky and Jung [2], Abramsky [1], or Mislove [21]) and trace their lineage to the approach in Lawson [17]. The standard approach masks the underlying order-theoretic nature of the results; in this paper, we make this nature foremost in consideration whenever possible. In keeping with this strategy, our order- theoretic notation will be standard, with the exception of the use of ^ and T to denote the least and greatest element, respectively, of a poset.
A program is a syntactic description of a computational process. As Abramsky observed in [1], there are three activities involved in program development:
The third task provides us with the fundamental logical relationship in program development: P \models f, where P is a program and f is a formula. This paper deals with the mathematics behind two approaches to the semantics of the triune process of program development. In the next few paragraphs, we introduce these approaches, then conclude the section with some motivation for the mathematical entities used in them. Throughout this section, we refer the reader to Abramsky [1], Abramsky and Jung [2], and Vickers [36], for the broader computer science context.
The denotational approach to programming languages, pioneered by D. S Scott and C. Strachey, seeks to develop a semantics of computation. Each syntactic category of programming language is assigned a type specifying which operations of the language may be performed upon it. A domain for a programming language is the underlying set of data objects for an admissable type, equipped with an information-based partial ordering. In the denotational approach, the elements of domains represent programs. The domains are assigned a topology based upon their ordering, known as the Scott topology, the open sets of which represent the formulas specifying programs. The fundamental relation is interpreted as set-inclusion: P\models fÛ P Î f.
The axiomatic approach to programming languages employs formal systems for reasoning about properties of programs. In the approach proposed by Abramsky [1], formulas specifying programs are viewed as elements of an abstract bialgebraic, distributive lattice L. Programs are viewed as those maps from L to the two-element chain {^,T} which preserve finie meets and arbitrary joins. In this approach, the fundamental relation is given by P\modelsfÛ P(f) = T.
The connection between these approaches is provided by a Stone-type duality. On one hand, the set ptL of all such maps from L to {^,T} forms an algebraic poset whose lattice of Scott-open sets is order-isomorphic to L. On the other hand, the Scott-open set lattice S(D) of an algebraic poset D is bialgebraic and distributive; and ptS(D) is order-isomorphic to D. The correspondence extends to a categorical duality which assures that axiomatic semantics is compatible with dentotational semantics - in the sense that the denotation of a program is identified with the set of specifications which are true of it. (See Abramsky [1], Robinson [25], and Vickers [36].)
Now that we have painted the broad picture of what semantics is about, let us consider more carefully the mathematical objects involved. Bialgebraic (that is, algebraic and dually algebraic), distributive lattices should be familiar enough to algebraists, but this may not be the case with domains. We therefore pause to consider the question ``What is a domain?" Domains were introduced by Dana Scott for modeling computation. Since the concept evolved to meet specific needs of computer scientists, to answer this question requires a look at these needs.
As mentioned above, data objects are usually assigned types specifying which operations of the language may be performed upon them. In denotational semantics, the mathematical models for types are called domains. What properties do these models have?
A computation is considered to be an algorithm acting successively upon a set of data objects to obtain increasingly refined approximations to a desired result. In this sense, computations are processes acting on types; a domain should therefore possess sufficient structure to allow mathematical meaning to be given to these processes. A computational process may be described by identifying each of its stages with a subset of the type whose total information contains that of the desired result. The idea behind this scheme is simple: with each application of the algorithm, the data objects produced should provide better approximations to the desired result. The sets associated with the stages of the process are to represent refinements in the approximations of the desired result. In this scheme, the end result of the process is viewed as a ``limit" of the approximating sets of data.
The structure of domains therefore depends on how we choose to formalize the loose notion that the end result of a computational process is a limit of the data given by its stages. To begin, models for types are viewed abstractly as posets, in which the relation x £ y implies that x is ``less defined" than y, or that the information content of y is a ``refinement" of that of x. Let T be a type endowed with such a partial ordering and suppose that P is a computational process acting on T. The nature of computers is such that, at any stage of P, the computer can act upon only finitely many data objects at a time. If subsequent stages are to represent refinements of the information content of a stage S, then for each finite F Í S, there should exist a subsequent stage S¢ of P and a data object d¢ Î S¢ such that d¢ is an upper-bound for F. Consequently, the stages of a computational process should form a directed subset of T. (Recall that a subset D of a poset is directed provided every finite subset of D has an upper bound in D.) It is natural, then, to consider computations in T to be joins of directed sets in T.
A poset P is directed complete (a DCPO) provided the join of every directed subset of P exists in P. In view of the previous discussion, it is reasonable to consider domains to be DCPOs.
Given DCPOs P and Q, a function f:P ® Q is Scott continuous provided f preserves directed joins. A program in a language L can be thought of as a map between types of L which preserve computational processes. In the abstract, a program in L is a Scott continuous map between domains of L. The class of all DCPOs with Scott continuous maps forms a category under function composition. We will use DCPO to denote this category.
A DCPO need not have a least element. It is customary to call a lower bounded DCPO a pointed DCPO. The full subcategory of DCPO whose object class consists of all pointed DCPOs is denoted by pDCPO. In Abramsky [1], a category of domains is defined to be any full subcategory of pDCPO. In most applications, however, categories of domains are required to be cartesian-closed. (A category is cartesain-closed provided it has finite limits and a self-functor adjoint to the formation of finite products.) The reason for this lies in the fact that finite products in subcategories of DCPO , when they exist, are usually cartesian products; and, when it exists, the object assignment of the adjoint to the finite cartesian product of DCPOs is the function space. (Given DCPOs C and D, the function space [C® D] is the set of all Scott continuous maps from C to D under the pointwise ordering.) The formation of finite cartesian products and function spaces both have natural meanings as type constructors - processes by which new types may be constructed from existing ones. The existence of function spaces is a highly desirable feature since, among other things, it allows the possibility of modelling recursion. For details on type constructors, see Abramsky [1], Abramsky and Jung [2], Plotkin [23,24], or Vickers [36].
The need for categories domains to be cartesian-closed stems from the special demands of modelling recursion; it is not necessary for a general order theoretic treatment of the subject. We will therefore postpone any detailed discussion of cartesian-closure until Section 6.
In many applications, it is also important to be able to express computations as limits (directed joins) of approximating ``essential" or ``explicitly computable" data objects. This need is reflected in the common requirement that domains be continuous or even algebraic as posets. The first DCPOs to be considered as models for computation were continuous lattices and were introduced by Scott in his fundamental works [26,27,28,29]. Today, continuous lattices form an important component of order theory in their own right (see, in particular Gierz et al. [7]); but their value to denotational semantics has been limited by the fact that their completeness as lattices brings about the existence of elements which cannot be assigned a natural computational meaning. However, continuous lattices do possess a structural property quite desirable in most models of computation.
A type may contain data objects with finite or infinite information content. For purposes of this discussion, we will refer to these objects as finite or infinite objects, respectively. We look upon the finite elements of a poset P as representing data objects whose information content may be obtained by computation in a finite time. Due to the finite nature of computers, infinite data objects in T can be given a natural computational meaning only as the suprema of directed sets of approximating finite data objects. Consequently, if we want to distinguish between finite and infinite data objects, the domain model for T should be a DCPO in which every element is the join of a directed set of ``finite" elements.
To understand what this should mean, we must devise a formal definition for ``finite data object". We want a finite approximation to a data object k to be essential to the computation of x and to any object which might refine x. By essential, we will mean that the end result of any computational process which is approximated by x must be at least as accurate as any finite object k which approximates x. In order theoretic terms, this means that if k £ x is finite and D is any directed subset of T such that x £ ÚD, then there exist d Î D such that k £ d. Any element k with this property is called relatively compact; or, more colorfully, way-below the element x (see Gierz et al. [7]).
A DCPO P is continuous if, for all p Î P, the set Wp of all elements way-below p is directed, and p = ÚWp. (A continuous lattice is simply a lattice which is also a continuous DCPO.) If we wish to distinguish between finite and infinite data objects in a type, it follows that its domain should be a continuous DCPO. (See Gierz et al. [7] for motivation of the term ``continuous".)
Strictly speaking, a relatively compact element in a DCPO is not truly finite, since it can itself be the supremum of an infinite directed set. To remedy this, we strengthen the requirement of relative compactness to the familiar notion of compactness: An element element k of a DCPO P is compact in P provided whenever D Í P is directed and k £ ÚD, then k £ d for some d Î D. Compact elements are inaccessible by directed joins. A DCPO P is algebraic provided, for all p Î P, the set Kp of all compact elements below p is directed and such that p = ÚKp.
Unfortunately, the full subcategory Algpos of DCPO whose object class consists of all algebraic posets, is not cartesian-closed. (For example, the function space [Z-® Z-] fails to be algebraic, where Z- denotes the negative integers under the usual ordering.) Computer scientists looking for type constructors in this context must search for cartesian-closed subcategories of Algpos . We will examine some of the most important of these categories in Section 6.
A function between DCPOs is computable provided it preserves directed joins. That is, if P and Q are DCPOs and f:P ® Q is a function, then f is computable provided f(ÚP D) = ÚQ{f(d) : d Î D} for all directed D Í P. Note that this condition is equivalent to the requirement f(ÚP D) £ ÚQ{f(d): d Î D} for all directed D Í P. Consequently, computability expresses the requirement that, at least for algebraic posets, every finite amount of information about the resulting value f(ÚP D) requires only a finite amount of information about the element ÚP D.
Computable functions between DCPOs are usually called Scott-continuous (or simply continuous) functions. The motivation for this lies with a natural topology which can be associated with any DCPO. Recall that an upperset of a poset P is a subset U of P with the property that, whenever u Î U and p Î P such that u £ p, then p Î U. A subset U of a DCPO P is Scott-open in P provided
It is routine to prove that the collection of Scott-open subsets of a DCPO P forms a topology (of open sets) on P. We call this topology the Scott topology for P and use S(P) to denote its corresponding lattice of open sets, ordered by set-inclusion.
It is routine to prove that a function between DCPOs is computable if and only if it is continuous with respect to their Scott topologies. Herein lies the motivation behind labeling computable functions as continuous. We will adhere to this convention for the remainder of this paper.
A frame is a complete lattice L which satisfies the join-infinite distributive law: For all X Í L and y Î L,
|
A function f:L ® M between frames L and M is called a frame homomorphism provided it preserves arbitrary joins and finite meets. In symbols, f is a frame homomorphism provided, for all X Í L and finite F Í L, we have
We note that frame homomorphisms preserve least and greatest elements. The class of all frames together with frame homomorphisms forms a category under function composition which we will denote by Frm .
All algebraic, distributive lattices are frames. We will denote by BiAlgFrm the full subcategory of Frm whose object class consists of all bialgebraic, distributive lattices. This category will play an important role in Section 4.
Given any set X and topology W of open sets on X, it is easy to see that the open set lattice of W is a frame; in particular, S(P) is a frame for any DCPO P.
Though it will not play a role in our considerations, we note that free frames exist. The free frame in countably many generators is the Lindenbaum algebra of propositional geometric logic (see Vickers [36]). The significance of the categorical duality between the full subcategory Algpos of DCPO and the full subcategory BiAlgFrm of Frm described in Section 4 below lies in the power it provides for developing the axiomatic semantics of programming languages using the techniques of denotational semantics. For details, the reader is referred to Abramsky [1], Robinson [25], and Vickers [36].
We have seen that every DCPO P may be associated with a frame, namely its lattice S(P) of Scott-open sets. This correspondence extends to a contravariant functor S:DCPO ® Frm . The morphism assignment f\longmapsto S(f) maps a continuous function f:P ® Q between DCPOs P and Q to the frame homomorphism S(f):S(Q) ®S(P) defined by S(f)(V) = f- 1(V). This contravariant functor has associated with it a companion functor pt:Frm ® DCPO , and together these functors provide a contravariant adjunction between these categories. The description of this companion functor requires some additional definitions and results.
Let L and M be frames and let Frm [L,M] denote the set of frame
homomorphisms from L to M under the pointwise order: fg if and only if f(a) £ g(a) for all a Î L. The following straightforward result shows that Frm [L,M] is a DCPO.
(See Johnstone [13], Lemma 1.11, p. 47 for a proof.)
Lemma 1
If L and M are frames, and D Í Frm [L,M] is a directed set, then
the map
D: L ® M defined by D(a) = ÚM{f(a) : f Î D} is the join of D in Frm [L,M]. In particular,
Frm [L,M] is a DCPO.
In all that follows, we will use 2 to denote the two element chain {^,T}. By Lemma 3.1, Frm [L,2] is a DCPO for any frame L. We will call the elements of this poset the points of L and denote the poset by pt(L).
We can now describe the companion functor to the contravariant functor S. For every frame homomorphism f:L ® M between frames L and M, let pt(f):ptM ® ptL be defined by pt(f)(x) = x°f, for all x Î pt(L). The object assignment L ® ptL coupled with the morphism assignment f\longmapsto pt(f) constitutes a contravariant functor pt:Frm ®DCPO .
Let l:IdDCPO ® pt°S be the following class of maps. For every DCPO P, the member lP :P® ptS(P) of the class l is the map defined by lP(q)(U) = TÛ q Î U.
Let r:IdFrm ® S°pt be the following class of maps. For every frame L, the member rL:L ®S(pt(L)) of the class r is defined by rL(a) = {x Î pt(L): x(a) = T}.
The straightforward, albeit tedious, proof of the next result is included for completeness. It makes use of the well-known connection between adjunctions and free pairs. We refer the reader to MacLane [19] for more information and note, as a word of caution, that the general result in that book is stated for covariant adjunctions.
Theorem 2
The functors S and pt form a contravariant adjunction
between DCPO and Frm . Moreover, the classes l and r are the units of this
adjunction.
Let P be a DCPO. We begin by showing that lP is continuous. Let D Í P be directed and let U Í P be Scott-open. By definition,
| ||||||||||||||||||||||||
Thus, lP(ÚD) = {lP(d): d Î D}; and
lP is continuous.
To prove the universal property, we must show that, for every frame L and continuous function f:P ® pt(L), there exists a unique frame homomorphism j:L ® S(P) such that pt(j)°lP = f.
For all a Î L, set j(a) = {p Î P: f(p)(a) = T}.
Since f is isotone, j(a) is clearly an upperset of P for all a Î L. To see that
v(a) is Scott-open, suppose that D Í P is directed and such that ÚP D Î j(a). It then follows that f(ÚP D)(a) = T. Since f is isotone, the set
{f(d): d Î D} is directed in pt(L). Since f is continuous, we therefore know that
f(ÚP D) = {f(d) : d Î D}. It follows that f(d)(a) = T for some d Î D; in particular, d Î j(a). This completes the proof that j(a) is Scott open.
The proof that j is a frame homomorphism is similar.
To establish that pt(j)°lP = f, observe that, for all p Î P, the morphism assignment of pt stipulates that (pt(j)°lP)(p) = lP(p)°j. Consequently, for all a Î L, we have
| ||||||||||
Thus, pt(j°lP) = f.
It remains to prove that j is unique. To this end, suppose that y:L ® S(P) is a frame homomorphism such that f = pt(y)°lP. Then, for all a Î L,
| ||||||||||||||||||||
[¯]
In the paragraphs to follow, we will prove that the contravariant adjunction (S,pt,l,r) described in Section 3 restricts to a dual equivalence between the category Algpos and an important full subcategory of Frm whose object class we now introduce.
A complete lattice L is biaglebraic provided both L and its order dual Lop are algebraic. As mentioned earlier, every algebraic, distributive lattice is a frame; we will use BiAlgFrm to denote the full subcategory of Frm whose object class consists of bialgebraic frames.
In the work to follow, we will prove that Algpos is dually equivalent to BiAlgFrm . This result is well-known among computer scientists (see Vickers [36], for example); however, our proof will be based upon purely lattice-theoretic ideas. We begin with some terminology.
Let L be a lattice. An element p of L is meet-prime (MP) in L provided, whenever F Í L is finite and such that ÙF £ p, then x £ p for some x Î F. We say p is meet- irreducible (MI) provided, whenever F Í L is finite and p = ÙF, then p = x for some x Î F. Every meet-prime element in L is meet-irreducible in L; the converse is true when L is distributive. Note that, if L has a greatest element, T, then the fact that T = ÙÆ precludes T from being meet-irreducible. An element j of L is join-prime (JP) or join-irreducible in L provided it is meet-prime, or meet-irreducible, respectively, in Lop.
Let L be a complete lattice. An element p of L is completely meet-prime (CMP) provided whenever X Í L is such that ÙX £ p, then x £ p for some x Î X. By similarly extending the definitions of MI, JI, and JP elements to include arbitrary meets and joins, we obtain the definitions for completely meet-irreducible (CMI), completely join-irreducible (CJI), and completely join-prime (CJP) elements, respectively. Observe that an element of L is CJP if and only if it is compact and join-prime in L.
In all that follows, let MP (L), MI (L), JP (L), and JI (L) denote the subposets of meet-prime, meet-irreducible, join-prime, and join-irreducible elements, respectively, of a lattice L. Likewise, we will use CMP (L), CMI (L), CJP (L), and CJI (L) to denote the subposets of completely meet-prime, completely meet-irreducible, completely join-prime, and completely join-irreducible elements, respectively, of a complete lattice L.
The meet-prime elements of a frame L are in bijective, order reversing correspondence with the points of L. Indeed, if p Î MP (L), then the function xp:L ® 2 defined by
|
is a point of L with x-1p(^) = ¯ p. (For any b Î L, ¯ b = { a Î L : a £ b}.) On the other hand, if x is a point of L, then, since x is a frame homomorphism, x-1(^) = ¯ px for some meet-prime px Î L, namely px = Úx-1(^). It is routine to prove that the assignments p \longmapsto xp and x \longmapsto px are mutually inverse and order reversing. For future reference, we state this correspondence as a lemma.
Lemma 1
If L is a frame, then MP (L) is dually order-isomorphic to pt(L). The dual isomrphism is implemented via the assignments p \longmapstoxp and x \longmapsto px described above.
A subset I of a poset P is a lowerset in P provided it is an upperset in Pop. (Note that ¯ p is a lowerset of P for all p Î P. It is called the principal lowerset generated by p in P.) It is easy to see that, given any poset P, the set L(P) of all lowersets of P, ordered by set-inclusion, is a bialgebraic, distributive lattice under the operations of set-intersection and union. It is well-known that every element of an algebraic lattice is the meet of a set of CMI elements. Using this fact, the following classic result provides several characterizations of bialgebraic frames, including the fact that every such frame is of the form L(P) for some poset P. For a proof of this result, we refer the reader to Crawley and Dilworth [4].
Theorem 2
For a complete lattice L, the following are equivalent:
Let L be a complete lattice and let a,b Î L. We say the ordered pair (a,b) splits L provided
(Note that b = {x Î L : b £ x}; it is the principal upperset generated by b in L.)
Lemma 3
Let L be a complete lattice. If (a,b) splits L, then a is CMP
and b is CJP in L.
[¯]
Given a complete lattice L and a,b Î L, set pb = Ú{x Î L : b \not £ x} and set ja = Ù{y : y \not £ a}.
Lemma 4
Let L be a complete lattice and let a,b Î L.
[¯]
Lemmas 4.3 and 4.4 imply that, for every complete lattice L, the assignments p ® jp and j ® pj constitute mutually inverse, isotone maps between CMP (L) and CJP (L). Consequently, we have the following result, recorded as a lemma for future reference.
Lemma 5
If L is a complete lattice, then CJP (L) is order isomorphic to
CMP (L). The isomorphism is implemented via the maps j ® pj and p® jp, where jp and pj are as defined above.
The following result describes when a point of a frame L is compact in ptL. Its simple proof relies on Lemmas 4.1 and 4.5 and is left to the reader.
Lemma 6
Let L be any frame, and let M be a frame in which every element is
the meet of a set of meet-prime elements.
We are now ready to prove that the contravariant adjunction (S,pt,l,r) restricts to a dual equivalence between Algpos and BiAlgFrm .
Let P be a DCPO and let x Î P. It is easy to see that x is Scott-open in P if and only if x Î K(P). Furthermore, it is easy to see that, whenever x is Scott-open for some x Î P, then x is CJP in S(P). With these observations in mind, we have the following result.
Lemma 7
Let P be an algebraic poset.
(i) x Î K(P)
(ii) x Î S(P), and
(iii) x Î CJP (S(P)). In view of these facts, Claims (2), (3), and (4) are immediate consequences of Claim (1) and Lemma 4.4. We therefore prove only Claim (1).
Let P be an algebraic poset, let U Î S(P), and let
|
It is clear that V Í U. To obtain the reverse inclusion, suppose that p Î U. Since P is an algebraic poset, Kp = ¯ p ÇK(P) is directed and such that ÚKp = p. Since U is Scott-open, it follows that there exist x Î Kp such that x Î U. Since p Î x, we see that p Î V. Consequently, U Í V, as desired.
[¯]
Lemma 8
If L is a bialgebraic frame, then pt(L) is an algebraic poset.
To this end, let p Î MP (L) and suppose that p is a lower-bound in L for a finite set F of CMP elements. We will find a CMP lower-bound for F in p. If p = ÙF, then the fact that p is meet-prime implies that p Î F. In this case, p is itself the CMP lower-bound we seek, so let us assume that p < ÙF.
For each q Î F, let jq be the CJP element of L corresponding to q and let J = {jq : q Î F}. Since p < ÙF, we know that jq \not £ p for all q Î F; hence, we know ÙJ \not £ p. By Theorem 4.2, there exists a CJP element c Î ¯ ÙJ such that c \not £ p. By Lemma 4.4, the element pc is CMP in L, and (pc,c) splits L. It must therefore be true that p £ pc. Since c £ ÙJ, it follows that pc £ ÙF. Thus, pc is the CMP lower-bound for F that we seek.
[¯]
Consider now the contravariant adjunction (S,pt,l,r) between the categories DCPO and Frm . In Lemmas 4.7 and 4.8, we have shown that S and pt restrict to contravariant functors between the categories Algpos and BiAlgFrm . To complete the proof that Algpos is dually equivalent of BiAlgFrm , we turn attention to the unit and counit of the adjunction.
Lemma 9
For every bialgebraic frame L, the map rL:L ®S(pt(L)) is a bijection.
|
It is easy to see that rL is an injection. Indeed, let a,b Î L be distinct. We may assume a \not £ b. Since L is bialgebraic, there is a CMP element p Î L such that a \not £ p but b £ p. Consequently, if xp is the point of L corresponding to p, we know xp(a) = T and xp(b) = ^. Thus, rL(a) ¹ rL(b).
To see that rL is a surjection, observe first that we know by Lemmas 4.7 and 4.8 that U Î S(pt(L)) implies that U = È{ x : x Î K(pt(L))}. Since rL is a frame homomorphism, it will thus suffice to prove that x is in the image of L under rL for all x Î K(pt(L)). To this end, let x Î K(pt(L)), let px be the CMP element of L associated with x, and let jpx be the CJP element of L associated with px. Observe that, by the construction of px and jpx (see Lemmas 4.5 and 4.6), we know
| |||||||||||||||||||||||||
Hence, we see that rL(jpx) = x; and x is indeed in the image of L under rL.
[¯]
Lemma 10
For every algebraic poset P, the map lP:P ® pt(S(P)) is a bijection.
|
To see that lP is an injection, suppose p,q Î P are distinct. We may assume that p \not £ q. Consequently, there exist compact x Î P such that x £ p but x \not £ q. Therefore, p Î x, but q Ï x. Hence, lP(p)( x) = T while lP(q)( x) = ^. It follows that lP(p) ¹ lP(q).
To see that lP is a surjection, suppose first that x is a compact point of S(P). By Lemma 4.6, x is a complete lattice homomorphism; hence, x-1(U) = U for some U Î S(P). It is clear that U Î CJP (S(P)); consequently, U = k for some k Î K(P). Observe that
| ||||||||||
Consequently, we see that x = lP(k). Now suppose that y is an arbitrary point
of S(P). Since pt(S(P)) is an algebraic poset, the set Ky = {x Î K(pt(S(P))) : x y} is directed, and y = Ky. Our previous arguments
concerning compact points tell us that lP-1(Ky) is directed in K(P). Since
lP is continuous, it follows that y = lP(ÚPlP- 1(Ky)). Thus,
lP is indeed a surjection.
[¯]
Let L be an algebraic frame and let P be an algebraic poset. By the proof of Lemma 4.9, the inverse of the map rL is defined by
|
Likewise, by the proof of Lemma 4.10, the inverse of the map lP is defined by
|
Clearly, both maps are isotone. Consequently, we see that L is order-isomorphic to S(pt(L)) and P is order-isomorphic to pt(S(P)). Combining Lemmas 4.7 through 4.10, we obtain the main result of this section.
Theorem 11
The contravariant adjunction (S,pt,l,r) restricts
to a dual equivalence between Algpos and BiAlgFrm .
In this section, we explore the connection between algebraic posets and bialgebraic members of an important class of distributive lattices. Recall that a complete lattice is said to be coherent provided it is order-isomorphic to the ideal completion of a bounded, distributive lattice. A poset is a member of the class of coherent lattices if and only if it is an algebraic frame whose compact elements form a bounded sublattice. For purposes of generality, we shall use the term precoherent to refer to any algebraic frame whose compact elements form a lower-bounded (rather than bounded), distributive lattice.
Coherent lattices form an important class of mathematical objects, due to their role in Stone-type dualities and to the fact that they possess logical presentations involving only finite conjunctions and disjunctions (see Johnstone [13]). In light of Theorem 4.11, we know that every bialgebraic, coherent frame has associated with it an algebraic poset whose lattice of Scott-open sets is order-isomorphic to the parent frame. The next few results establish an internal description of those algebraic posets whose lattices of Scott-open sets are bialgebraic, coherent (or precoherent) frames.
Let P be an algebraic poset and let S Í K(P). A set MS Í K(P) is called a complete set of minimal upper-bounds for S provided
Let P be an alebraic poset and let S Í K(P), and suppose that S has a finite complete set of minimal upper-bounds. In this case, it is clear that we may take this set to be an antichain. This antichain is unique, and we will let MUB(S) denote it (when it exists). In light of Theorem 4.2 and Lemma 4.9 note that the following statements are equivalent:
We will use the term coherent to refer to any algebraic poset in which every finite subset of compact elements has a finite complete set of minimal upper-bounds and use precoherent to refer to any algebraic poset in which every finite nonempty subset of compact elements has a finite complete set of minimal upper-bounds. We will let Coh and PCoh denote the full subcategories of Algpos whose object classes consist, respectively, of coherent and precoherent algebraic posets. The suggestive terminology is justified, as the next results prove.
Lemma 1
Let P be an algebraic poset and let S Í K(P) be finite and
nonempty.
Conversely, suppose that S has a finite complete set of minimal upper-bounds in K(P). Let MS be such a set. Let U = Ç{ s : s Î S}. If MS is empty, then U = Æ and is therefore compact in S(P). If MS is not empty, let V = È{ m : m Î MS}. By Lemma 4.7, each m is compact (indeed, CJP) in S(P); hence, V is compact in S(P). We will prove that U = V and is therefore compact.
Observe that, by construction, p Î U if and only if p is an upper-bound for S in P. Since P is an algebraic poset, it follows that p Î U if and only if there exist k Î K(P) such that k is an upper-bound for S and k £ p. Since MS is a complete set of upper-bounds for S, we see that p Î U if and only if p Î m for some m Î MS. Consequently, we must have p Î V; and U Í V. The reverse inclusion is obvious.
[¯]
In any algebraic lattice, the compact elements form a lower-bounded join subsemilattice. In a bialgebraic frame, every compact element is the join of a finite set of CJP elements. As a result, the following lemma is an immediate (albeit tedious) consequence of the distributive law.
Lemma 2
In a bialgebraic frame L, the following are equivalent.
The following results are direct consequences of Lemmas 4.7, 4.9, 5.1, and 5.2.
Lemma 3
Let L be a bialgbraic frame.
Lemma 4
Let P be an algebraic poset.
Coherent frames are often called spectral frames, especially in more topological approaches to the subject. This terminology may be traced to the well-known fact that the open-set lattice for the prime spectrum of a bounded, distributive lattice is a coherent frame (see Johnstone [13]). In this setting, coherent, bialgebraic frames are called spectral algebraic frames. The term ``coherent" is probably better known to order theorists and is becoming widely used in domain theory, accounting for our choice of the term.
Let CohFrm and PCohFrm denote the full subcategories of BiAlgFrm whose object classes consist of coherent and precoherent, bialgebraic frames, respectively. We now have the following result as an immediate consequence of Theorem 4.11.
Theorem 5
The category PCoh is dually equivalent to the category PCohFrm , and
the category Coh is dually equivalent to the category CohFrm . Both dualities are expressed
via appropriate restrictions of the adjunction (S,pt,l,r).
It is a well-known fact that a precoherent frame is bialgebraic if and only if its compact elements form a sublattice in which every element is a finite join of join-prime elements. (Indeed, this is a direct consequence of Theorem 4.2 and the observation that an element j of a frame is CJP if and only if it is compact and join-prime.) This observation, coupled with Lemmas 5.3 and 5.4, gives us the following results concerning the prime spectrum of lower-bounded, distributive lattices.
Theorem 6
For a poset P, the following statements are equivalent.
Likewise, for a poset P, the following statements are equivalent.
Suppose Pop is algebraic and precoherent. We know that S(Pop) is a bialgebraic, precoherent frame. Now, S(Pop) is order-isomorphic to the ideal completion of a lower-bounded, distributive lattice D in which every element is a finite meet of join-prime elements. The prime spectrum of D (that is, its prime ideals, ordered by set-inclusion) is order-isomorphic to MP (S(Pop)). Since MP (S(Pop)) is dually order-isomorphic to pt(S(Pop)) which in turn is dually order-isomorphic to P itself, we have the desired implication.
On the other hand, suppose that P is order-isomorphic to the prime spectrum of a lower-bounded, distributive lattice D in which every element is a finite join of join-prime elements. We know that the ideal completion, Idl(D), of D is a bialgebraic, precoherent frame. Hence, we know that P is dually order-isomorphic to the poset of meet-prime elements of a bialgebraic, precoherent frame; in other words, Pop is order-isomorphic to pt(Idl(D)). Hence, Pop is an algebraic, precoherent poset.
[¯]
The previous result, although a direct consequence of Theorem 4.11 and the well-known results of this section, does not seem to appear in the literature concerning algebraic posets. It provides additional insight into the classical problem of determining those classes of posets whose members may be realized concretely as the prime spectra of distributive lattices (see Balbes [3], Davey [5], and Speed [34]).
We conclude this section by introducing several object classes which arise from considering another important order-theoretic concept. Recall that a poset P is a tree provided ¯ p is a chain for all p Î P. A poset P is called a root-system provided its order dual Pop is a tree. Root-systems are often called dual trees. A lower-bounded, distributive lattice L is said to be relatively normal provided its prime spectrum is a root-system. Relatively normal lattices form a well-studied class of distributive lattices (for references, see Snodgrass and Tsinakis [33] or Hart and Tsinakis [12]).
We will say that a complete lattice is a member of the class ÁRN provided it is order-isomorphic to the ideal completion of a relatively normal lattice. Note that a lattice is a member of ÁRN if and only if it is an algebraic, precoherent frame whose subposet of meet-prime elements is a root-system. Members of this class possess a rich order theoretic structure which is extensively studied in Snodgrass and Tsinakis [33] and Hart and Tsinakis [12].
Let L be a bialgebraic, precoherent frame. In light of Lemma 4.8 and Lemma 4.1, we have the following result.
Lemma 7
For a frame L, the following statements are equivalent.
The next results allow us to expand upon this observation to establish a categorical correspondence between algebraic trees and bialgebraic members of the class ÁRN.
Lemma 8
Let P be an algebraic poset.
[¯]
We remark in passing that Lemma 5.8 is a direct consequence of the fact that any algebraic poset is the chain completion of its compact elements (see Markowsky [20]). Since no set of pairwise incomparable elements in a tree can have an upper-bound in that tree, the following result is a direct consequence of Lemma 5.8.
Lemma 9
Every algebraic tree is an algebraic, precoherent poset, and every
lower-bounded, algebraic tree is an algebraic, coherent poset.
Let AlgTree denote the full subcategory of PCoh whose object class consists of all algebraic trees, and let AlgTree^ denote the full subcategory of Coh whose object class consists of all lower-bounded, algebraic trees. Let BIRN denote the full subcategory of PCohFrm whose object class consists of all biaglebraic members of the class ÁRN, and let BIRNT denote the full subcategory of CohFrm whose object class consists of all bialgebraic members of the class ÁRN whose largest element is CJP. In light of Lemmas 5.8 and 5.9, we have the following result.
Theorem 10
The category AlgTree is dually equivalent to the category BIRN , and the
category AlgTree^ is dually equivalent to the category BIRNT . Both dualities are expressed via
appropriate restrictions of the adjunction (S,pt,l,r).
The next result provides another description of certain posets as the prime spectra of lower-bounded distributive lattices. It is a direct consequence of Lemmas 4.1 and 5.7.
Theorem 11
For a poset P, the following statements are equivalent.
Likewise, for a poset P, the following statements are equivalent.
In this section, we introduced coherent algebraic posets and their kin out of purely order-theoretic interest. In the next section, we turn from considering coherent algebraic posets and examine some of the reasons denotational semantics works with categories other than Algpos . In so doing, we will find ourselves returning once again to the objects introduced in this section.
Before presenting some of the subcategories of Algpos most useful in denotational semantics, we pause to discuss very briefly some of the constructions a theory of computation requires. It is by seeking subcategories closed under these constructions that most of the objects described in this section were identified. This discussion is based upon Vickers [36], Chapter 10 and Abramsky [[2]].
In most programming languages, data items are assigned types determining the operations that can be performed upon them. The notion of a data type is intuitive and not generally defined. There are essentially three classes of types: primitive types whose elements are identified directly, higher-order types which are built up from other types by means of acceptable type constructors, and recursively defined types. Primitive types include most predefined variable types, such as INTEGER, FLOATING POINT, etc. Acceptable type constructors are rules explaining how to make new elements from those of predefined types. Three commonly used type constructors are listed below.
Let S and T be two predefined types in a programming language. A higher-order type can be built from S and T using
Of course, one would want the resulting higher-order types to have the same information-based order structure that the predefined types possess. In other words, if the predefined types are all objects in DCPO or Algpos , then so should be the higher-order types constructed from them. Furthermore, one would ideally want the constructors to have some categorical meaning (as limits or colimits, etc.) recognizeable by the adjunction we described in Section 4.
The first two type constructors pose no problem in this regard. It is easy to prove that the category DCPO is closed with respect to the formation of arbitrary cartesian products and disjoint unions; moreover, these two constructions correspond to the categorical product and coproduct, respectively, in DCPO . Finite examples of these serve quite well as models for record-style and union-style constructions, respectively. The category Algpos is not as well-behaved; still, this category is closed under the formation of arbitrary disjoint unions and finite cartesian products - again sufficient to provide models for the first two type constructors.
It is the function-style type constructor that poses the difficulty -
and the interest. At first glance, one might assume that, given data types S
and T, the function-style type construction should produce the set TS;
that is, the set of all functions from S to T, partially ordered in the
usual pointwise fashion: f g Û f(s) £ g(s) for all s Î S.
The difficulty with this simple definition becomes immediately apparent, however,
when one realizes that there is no reason to assume TS will be a DCPO under
this ordering.
The natural solution would seem to be to take the result of the function-style construction to be the set HomDCPO(S,T) - the set of all Scott-continuous maps from S to T - and endow it with the usual pointwise partial ordering. Under this partial ordering, it is easy to prove that the set HomDCPO(S,T) is indeed a DCPO in its own right. We will call this DCPO the function space between S and T and denote it by [S® T].
As with the cartesian product, the function space is made more attractive as a model because its formation has a categorical interpretation as a special limit in DCPO . This limit is more subtle than products and coproducts, however, so we pause for a precise definition.
Let Cat = (Ob,Hom) be any category having finite products. For any objects A and B in Ob(Cat), we say the exponentiation of B with respect to A exists provided there is a Cat-object BA and a Cat-arrow Ev:BA × A ® B having the property that, for any Cat-object X and Cat-arrow h:X × A ® B, there is a unique Cat-arrow jh:X ® BA such that
|
The arrow Ev is called the evaluation arrow.
The category Set of all sets and functions between them has exponentiation - the object BA is the set of all functions from A to B. The evaluation map is simply the assignment Ev((f,a)) = f(a). It is this context which inspires the notation BA and the term ``evaluation arrow" for exponentiation in arbitrary categories. Given any set X and function h:X ×A ® BA, the map jh is defined as follows: for each x Î X, jh(x) is the map h(x,·):{x} × A ® B.
By using the same definitions as for the category Set, it can be shown that, for any DCPOs A and B, the function space [A ® B] coupled with the evaluation map Ev is the exponentiation (BA,Ev) in DCPO . As it is not directly germane to our purposes, we will leave the verification of this to the reader, remarking that the only difficulty lies in establishing that the maps Ev and jh defined above are Scott continuous (note, of course, that h:X × A ® BA is assumed Scott-continous in this context). This is easily accomplished using the following straightforward lemma (see Abramsky [2]).
Lemma 1
Let A, B, and C be DCPOs. A mapping f:A × B ® C
is Scott-continuous if and only if it is Scott-continuous in both coordinates.
A category Cat = (Ob,Hom) which possesses finite products, a terminal object, and exponentiation is said to be cartesian-closed. Cartesian-closed categories of DCPOs possess structure sufficient to define two of the three higher-order type constructors. The category DCPO is cartesian-closed; but, unfortunately, Algpos is not, since the function space [Z-® Z-] fails to be algebraic (where Z- denotes the negative integers under the natural ordering). In fact, even though every member of Z- is compact, the function space [Z- ® Z-] contains no compact elements at all.
A full, cartesian-closed subcategory of Algpos is usually referred to as a category of domains. We will devote the remainder of this section to identifying categories of domains.
Before continuing, however, we wish to point out that our definition of cartesian closure varies somewhat from that found in category theory texts. Cartesian closure is usually defined only for categories possessing all finite limits (see, for example, MacLane [19]). The definition we use is the one adopted in Smyth [32] and widely used in denotational semantics.
Let us now turn to finding categories of domains. We begin with some lemmas which tell us what we must be looking for. The next two theorems are based upon a result in Smyth [32].
Theorem 2
Let K be any full subcategory of DCPO possessing products of
pairs, the terminal object 1 = {^}, and a lower-bounded DCPO having at least two
elements. If A and B are K-objects and A ÕB denotes the product of A and B in
K, then A ÕB is order-isomorphic to the usual cartesian product A × B.
We first must prove that f is a bijection. To this end, note that, for every fixed a Î A and b Î B, there is exactly one x Î A ÕB such that p1(x) = a and p2(x) = b. To see why this is so, we need the terminal object. Given any fixed a Î A and b Î B, there certainly exist Scott-continuous maps s1:1 ®A and s2:1 ® B which ``select" a and b, namely the maps defined by s1(^) = a and s2(^) = b. Consequently, there exists a unique Scott continuous map l:1 ® A ÕB such that p1(l(^)) = a and p2(l(^)) = b. Simply let x = l(^). Of course, the same holds true in A × B - for any fixed a Î A and b Î B, there is exactly one y Î A × B such that p1(y) = a and p2(y) = b, namely y = (a,b).
It is now easy to see that f is a bijection. Let (a,b) Î A × B and let x Î A ÕB be such that p1(x) = a and p2(x) = b. By the choice of f, we know that p1(f(x)) = p1(x) = a and p2(f(x)) = p2(x) = b. Hence, we know that f(x) = (a,b); and f is a surjection. Since x is unique, it follows that f is an injection as well.
It remains to prove that f-1 is isotone. Let (a,b), (u,v) Î A × B be such that a £ A u and b £ B v. Let f-1((a,b)) = s and
f-1((u,v)) = t. We must prove that x y, where denotes the partial ordering
on A ÕB. To this end, let C be any lower-bounded K-object having at least two
elements. Define two maps h:C ® A and j:C ® B as follows: h(^C) = a, g(^C) = b, and h(x) = u, g(x) = v for all x > ^C. Both maps are clearly
Scott-continuous; hence, there exists a unique map k:C ® A ÕB such that
p1°k º h and p2 °k º g. Since k is Scott
continuous, we know that k(^C) k(x) for all x Î C. Furthermore, by the
uniqueness arguments given above, we know that k(^C) = s = f- 1((a,b)); and that, for
any x > ^C, k(x) = t = f-1((u,v)). Hence, s t, as desired.
[¯]
Of course, whenever the cartesian product of a pair of objects exists in a full subcategory K of DCPO , it is easy to prove that this object is the K-product of the pair in K. What the previous result tells us is that virtually any cartesian-closed full subcategory of DCPO will have the simple cartesian product as its finite product. (It is a routine exercise to prove that a category Cat has finite products if and only if the product of any pair of objects exists in Cat.) Hence, in searching for cartesian-closed subcategories of DCPO , we are justified in considering only those closed under finite cartesian products.
The next result tells us that, when considering exponentiation, for the most part, we need only look for closure with regard to the formation of function spaces.
Theorem 3
Let K be any full subcategory of DCPO possessing finite
products, the terminal object 1 = {^}, and a lower-bounded DCPO having at least
two elements. Let A,B be K-objects. If the exponentiation of B with respect to A
exists in K, then the exponentiation object BA is order-isomorphic to the function space
[A ® B].
We know that both BA and [A ® B] are DCPOs, and that (BA,Ev¢) is the exponentiation of B with respect to A in K. We also know that ([A ® B],Ev) is the exponentiation of B with respect to A in DCPO . Now, by definition, Ev¢:BA × A ® B, and Ev:[A® B] × A ® B. Hence, there exists a unique Scott continuous map j:BA ® [A® B] defined by
|
We will prove that j is the desired order-isomorphism.
We first prove that j is a bijection. First, observe that we may identify A with 1 ×A. Now, we can think of any f Î [A® B] as a map from 1 × A to B. Hence, there exists a unique Scott-continuous map hf:1® BA such that
|
for all a Î A. Thus, for each f Î [A® B], there is exactly one x Î BA such that j(x) = f, namely x = hf; and j is a bijection.
It remains to prove that j-1 is isotone. To this end, let
C be any lower-bounded K-object having at least two elements. Let f,g Î [D®E] be such that f g. (Recall that the ordering on [D® E] is pointwise.)
Define the map h:C ×A ® B by h((^C,a)) = f(a), and h((c,a)) = g(a) for
all c > ^C. The map h is clearly Scott-continuous. Once again, there exists a unique
Scott-continous map k:C ® BA such that Ev¢°k º h. There also exists a unique Scott continuous map g:C ® [A® B] such
that Ev°g º h. The uniqueness of k and g tells us that
j°k º g. Moreover, we know that, for all c Î C,
|
Let c0 > ^C be any element in C distinct from ^C, and
let h1:1® C and h2:1® C be the maps which
``select" ^C and c0, respectively. Clearly, h1 h2 in the DCPO [1® C]. Note that f º g°h1 and g º g°h2. Thus,
| |||||||||||||||
Likewise, j-1(g) º k°h2. Since k is isotone by assumption, it follows that k°h1 £ k°h2. Hence, j-1 is isotone.
[¯]
In light of the previous theorems, we see that we can identify most cartesian-closed full subcategories of DCPO simply by finding those closed under the formation of finite cartesian products and function spaces. Generally speaking, finite cartesian products pose no problem; the difficulties lie with the function space.
Henceforth, we shall restrict attention to full subcategories of Algpos . The category Algpos certainly possesses the terminal object 1, and it contains many lower-bounded objects having at least two elements - the schizoprhenic object 2 = {^,T} is just one example. It is not difficult to verify that Algpos is closed with respect to the formation of finite cartesian products. (Infinite cartesian products of algebraic posets may not be algebraic.) Unfortunately, as we have mentioned earlier, Algpos is not closed with respect to the formation of function spaces. In light of Theroem 6.3, we therefore know that Algpos is not cartesian-closed.
The counterexample demonstrating that Algpos is not closed with respect to the formation of function spaces now deserves some careful attention as it sheds light on what restrictions we must place on algebraic posets to obtain the desired closure. Let Z- denote the negative integers with their natural ordering and consider the function space FZ = [Z-® Z-].
Although every element of Z- is compact, we have claimed that FZ has no compact elements at all. Let us now prove this fact. Let f Î FZ, and consider the following family of functions: for all j Î Z-, let gj:Z- ® Z- be defined by
|
Remember that both x and j are negative in this context. Since f is isotone, it is easy to verify that each gj is isotone as well. Since Z- is a discrete chain, any isotone function from Z- to itself will be Scott continous; hence, each gj is a member of FZ. Furthermore, the set G = {gj : j Î Z-} is directed in FZ; indeed, G is an ascending chain in FZ whose join is f. Since gj is strictly less than f for all j Î Z-, it follows that f cannot be compact in FZ.
Let A and B be algebraic posets, and let f Î [A ® B]. One thing the previous discussion tells us is that requiring the range of f to be a subset of K(B) is not enough to guarantee that f is compact. We can say more about this, however.
Lemma 4
Let A and B be DCPOs. If the range of f Î [A ® B] is
a finite subset of K(B), then f is compact.
D. We must find some d Î D such that f d. We know that
|
Let x Î A and suppose that f(x) = bj. Since each bj is compact,
there must exist dj Î D such that f(x) £ B dj(x). If we let d
denote the upper bound in D for the set {d1, ..., dn}, then f d.
[¯]
The previous result gives us a clue about how to go about finding
compact functions in [A ® B]: Find some way to construct functions
f:A ® B whose range is a finite subset of K(B). We begin by
first working with lower-bounded, algebraic posets - the so-called
pointed algebraic posets. Let A be an algebraic poset and let B
be a pointed algebraic poset. Let a Î K(A) and b Î K(B). Define a
``step function" (a
b) as follows.
|
It is not difficult to verify that these step functions are Scott-continuous and hence compact members of [A ® B]. The following result is a consequence of the definition of the step functions; we record it as a lemma for future reference.
Lemma 5
Let A be an algebraic poset and let B be a pointed algebraic poset.
If a,b are compact elements in A and B, respectively, and if f Î [A® B] is such that b £ B f(a), then (a
b) f.
Let A be an algebraic poset and let B be a pointed algebraic poset. For any f Î [A ® B], we see that it is possible to construct a family of compact step functions below f. In all that follows, we will let
|
Unfortunately, there is no reason to suspect that the set Df is directed; hence, we cannot speak of its join in [A ® B]. We need to expand the set Df to a directed family of compact functions. The simplest way to create such a set would be to take all finite joins of members of Df. Of course, we cannot hope to do this in an arbitrary pointed algebraic poset, so we add some additional structure to the image poset B. Let us see what sort of structure is required.
We begin by considering a two-element set F = {(a1 b1),(a2 b2)} Í Df. We seek a compact function which is the
join in [A ® B] of F. Let F denote the
function we wish to create. Proceeding in the most natural way, we can define
( F)(x) = ^B whenever aj \not £ x for all j Î {1,2}.
Remembering that we want our function to be an upper-bound for the set F, we
also define ( F)(x) = bj whenever aj £ x and ak \not £ x
for k ¹ j. The problem arises with the remaining elements of A -
those contained in a1 Ç a2.
The simplest solution is to add structure to B by considering what are called lattice-like algebraic posets. An algebraic poset P is lattice-like provided
Note that every principal lowerset of a lattice-like algebraic poset is an algebraic lattice.
If we take B to be a lattice-like algebraic poset, then we can solve
the difficulty which arose in trying to define F. Let F = {(aj bj) : 1 £ j £ n} Í Df be nonempty. For each x Î A, let yj = (aj bj)(x).
The set {yj : 1 £ j £ n} has a join in ¯ f(x). Let y denote this join, and
let ( F)(x) = y.
In all that follows, given any set X, let Fin*(X) denote the set of all nonempty finite subsets of X,
By construction, we have F f for any F Î Fin*(Df). Observe that F is an upper-bound for F in [A ® B]. Notice
also that, using this definition, we can denote any step function (a b) Î Df by
F, simply by letting F = {(a b)}. Define a new set Dir(f) by
|
Lemma 6
Let A be an algebraic poset, let B be a lattice-like algebraic
poset, and let f Î [A ® B]. For any F Î Fin*(Df),
F is the join of F in ¯ f.
bj) : 1 £ j £ n} Î Fin*(Df) and suppose g Î ¯ f is an upper-bound for
F. For all x Î A, let yj = (aj bj)(x). The set {yj : 1 £ j £ n} has a join in ¯ g(x); and this join coincides with
the join of this set in ¯ f(x). Since ( F)(x) is defined
to be this join, it follows that ( F)(x) £ B g(x).
[¯]
In any DCPO, the join of a finite set of compact elements (when it exists) is necessarily compact. Consequently, we have the following result.
Lemma 7
Let A be any algebraic poset, and let B be a lattice-like algebraic
poset. If f Î [A ® B], then the set Dir(f) is directed in [A® B] with join f; in particular, [A ® B] is a pointed algebraic poset.
F and G. We will prove that the
function (F ÈG) is the upper bound we seek. We will prove that
F (F ÈG). The proof that G (F ÈG) is similar.
Let F = {(aj bj) : 1 £ j £ n} and let G = {(ck dk) : 1 £ k £ m}. Let x Î A and suppose that
( F)(x) = y. If there are no ck £ A x, then
((F ÈG))(x) = y - otherwise, ((F ÈG))(x) is
the join in B of the set {y}È{bk : ck £ x}. In either case,
it follows that ( F)(x) £ B ((F ÈG))(x).
It remains to prove that f º Dir(f). First note
that, for any x Î A,
|
Thus, it is clear that f(x) ³ B (Dir(f))(x). Now,
suppose that b ΠK(B) ǯ f(x). Since there must exist a0 ΠK(A) ǯ x, there exist step functions whose value at x is b, such as the function
(a0 b). Thus, there exist F Î Fin*(Df) such that b £ B (F)(x), namely any F containing (a0 b). Thus, we know
| ||||||||
Since the set Dir(f) consists of compact elements, we have now shown that [A ® B] is an algebraic poset. This poset clearly has a least element, namely the trivial map L:A ® B defined by L(x) = ^B.
[¯]
Let A be an algebraic poset and let B be a lattice-like algebraic
poset. As a consequence of the previous lemma, we know that every c Î K([A® B]) has the form F for some F Î Fin*(Dc). We will use this fact in the next result.
Lemma 8
If A is an algebraic poset and B is a lattice-like algebraic poset,
then [A ® B] is a lattice-like algebraic poset.
F :F Î H}. The set D is clearly directed; D is the element we
seek.
[¯]
Let LDom denote the full subcategory of Algpos whose object class consists of all lattice-like algebraic posets. We have just proven that LDom is closed with respect to the formation of function spaces. It is not difficult to prove that this category is also closed with respect to the formation of finite cartesian products. Hence, LDom is cartesian-closed and therefore a category of domains. (The symbol ``LDom" stands for lattice- like domain.) We record this observation as a theorem for future reference.
Theorem 9
The full subcategory LDom of Algpos whose object class consists of all
lattice-like algebraic posets is cartesian-closed and therefore a category of
domains.
Once again, we let B be a pointed algebraic poset so that we can
define (a b) for any compact elements a Î A and b Î B. We
already know that these functions are compact in [A ® B]; the
fundamental difficulty lies in extending the set Df to one which is directed
with join f
for any given f Î [A ® B]. By taking B to be a lattice-like
algebraic poset, we were able to accomplish this in a straightforward manner,
because this assumption allowed us to define finite joins for members of Df.
Of course, a set need not be closed with respect to finite joins in order to be
directed. Let us return to this problem with an eye to the pre-image poset A.
Let A be an algebraic poset, let B be a pointed algebraic poset,
and let f Î [A ® B]. Let (a1 b1) and (a2 b2) be members of
Df. The key issue is to find a compact upper-bound common to both functions which is itself
below f. The difficulty in defining this function lies with the set a1 Ça2. One way to begin tackling this problem is to require that A be precoherent. In so
doing, we know by Lemma 5.2 that a1 Ç a2 is compact in
S(A) - in particular, there exist k1, ..., kj such that a1 Ça2 = k1 È... È kn. Of course, we know from Lemma 5.2 that
we may take {k1, ..., kn} to be MUB(a1,a2). Intuitively, we would like to
define the upper-bound for F = {(a1 b1),(a2 b2)} using maps of the form
(kj ej), where kj Î MUB(a1,a2) and ej is any compact upper bound
for {b1,b2} in ¯ f(x). Unfortunately, we encounter essentially the same problem
- the set X = MUB(S) may be nonempty for some nonempty S Í MUB({a1,a2}), and some nonempty subset of X may in turn have a nonempty set of minimal
upper bounds, ad infinitim. We therefore place an additional restriction on the poset A which
says, in effect, that this sequence of sets of minimal upper bounds must terminate after finitely
many iterations.
To be precise, we introduce a new term. Let A be a precoherent, algebraic poset and let M Í K(A). We say that M is MUB -preclosed provided MUB(S) Í M for all S Î Fin*(M). It is easy to prove that the intersection of any family of MUB- preclosed subsets of K(A) is again MUB-preclosed. With this in mind, let X Î K(A) be nonempty and define the MUB-preclosure of X to be the intersection of all MUB-preclosed subsets of K(A) which contain X. We will let mpc(X) denote the MUB-preclosure of X in K(A). We will say that an algebraic poset A is strongly precoherent provided it is precoherent, and every finite, nonempty subset of K(A) has finite MUB-preclosure.
Lemma 10
Let A be a precoherent algebraic poset, and let M be a finite MUB-
preclosed subset of K(A). If x Î A is such that ¯ x ÇM ¹ Æ, then there is a largest member of M below x.
[¯]
It is the notion of finite MUB-preclosure coupled with the previous lemma
which enables us to solve the problems encountered in extending the basic compact step functions.
Let A be a strongly precoherent, algebraic poset and let B be a pointed algebraic poset. Let f Î [A ® B] and let F = {(aj bj) : 1 £ j £ n} Î Fin*(Df). Let M = mpc{a1, ..., an}.
We now assign to each u Î M a compact element in ¯ f(u)
according to the following recursive process. If u is minimal in M, then
u = aj for some j; let cu = (aj bj)(u) = bj in this case.
If u covers at least one member of M, let Xu denote the set of all members of
M covered by u and let cu be a compact upper-bound in ¯ f(u)
for {cv : v Î Xu}. (Note that each cv Î ¯ f(u) because
f is isotone.)
We are ready to define the function 
F. If
¯ x ÇM = Æ, let ( F)(x) = ^B; otherwise,
let ( F)(x) = cu, where u is the largest member of M in
¯ x.
Note that the above construction actually defines a family of functions - one for each choice of the compact elements cu. For each F Î Fin*(Df), let Bd(F) denote this set.
Lemma 11
Let A be a strongly precoherent, algebraic poset, let B be a
pointed algebraic poset, and let f Î [A ® B]. If F Î Fin*(Df), then
each one of the functions in Bd(F) is Scott-continuous and a compact upper-bound for
F in ¯ f.
F is Scott-continuous. Let D Í A be directed, and let x = ÚA D. Let F = {(aj bj) : 1 £ j £ n}, and let M = mpc{a1, ..., an}. For each m Î M, suppose that (F)(m) = cm. If ( F)(x) = ^B, then it must be true that ( F)(d) = ^B
for all d Î D. In this case, it is clear that ( F)(x) = ÚB{( F)(d) :d Î D}. Suppose ( F)(x) > ^B. Let T = M ǯ x. We know by
Lemma 6.10 that T has a largest element, m; in particular, ( F)(x) = cm.
Now, for each t Î T, t is Scott-open and contains x; hence, we know D Ç t ¹ Æ. For each d Î t ÇD, we know that ( F)(d) = ct; and we know that each ct £ B cm. If d Î D is such that d Ï t for
any t Î T, then we must have ( F)(d) = ^B, since D Í ¯ x.
Consequently, ÚB{( F)(d) : d Î D} = cm.
It is now clear that each F is a member of ¯f and an upper-bound for the set F. It remains to prove that each F is compact in [A ® B].
To this end, let D Í [A ® B] be directed and such
that F D. Note that, for each m Î M, we have (m cm) F. Since each (m cm) is compact by Lemma 6.4, there exist
dm Î D such that (m cm) dm. Let d denote any upper-bound in D for the
set {dm : m Î M}. It is easy to check that F d.
[¯]
Lemma 12
Let A be a strongly precoherent, algebraic poset, and let B be a
pointed algebraic poset. If, for each f Î [A ® B], we set D(f) = È{Bd(F) : F Î Fin*(Df)}, then D(f) is directed with join f. In particular, [A® B] is a pointed algebraic poset.
bj) : 1 £ j £ n}, and G = {(ck dk) : 1 £ k £ m} be members of Fin*(Df) and let F, G be members of Bd(F) and Bd(G), respectively. Let MF
denote the MUB-preclosure of X = {aj : 1 £ j £ n}, and let MG denote the
MUB-preclosure of Y = {ck : 1 £ k £ m}. Define a function (FÈG) Î Bd(F ÈG) as follows. Let x Î A. If x does not exceed any member of MF or
MG, then ((FÈG))(x) = ^B. Suppose that x exceeds some maximal nonempty
subset Sx of MF ÈMG. If Sx Í MF, then let ((FÈG))(x) = cu,
where u is the largest member of MF below x. Likewise, if Sx Í MG, let
((F ÈG))(x) = cv, where v is the largest member of MG below x. Otherwise,
let u Î MF and v Î MG denote the two maximal elements in MF ÈMG below x, and
let ((F ÈG))(x) = k, where k is any compact upper bound for {u,v} in
¯ f(x). The function (F ÈG) is the upper-bound we seek.
To see that D(f) º f, simply observe that, for all x Î A and all k Î K(B) ǯ f(x), there is a function g Î D(f) such that g(x) = k, namely g = (a k), where a is any
compact element below x. Hence, [A ® B] is algebraic. It is
easy to see that [A ® B] has a least element; namely the trivial
map which sends every member of A to ^B.
[¯]
Given algebraic posets A and B, we have shown that by placing additional restrictions on either the image or the pre-image poset, it is possible to guarantee that [A ® B] is an algebraic poset. The restrictions we placed on B gave rise to a cartesian-closed subcategory of Coh . It turns out that the restrictions placed on A also gives rise to a cartesian-closed subcategory of Coh , though proof of this fact is more difficult. We turn to this task next.
Let A be a coherent algebraic poset, and let S Í K(A). We say that S is MUB-closed provided MUB(X) Í S for all finite X Í M. Given any S Í K(A), we define the MUB-closure of S to be the intersection of all MUB-closed subsets of K(A) containing S. We denote this set by mc(S). Note that, if A is pointed, then mc(S) = mpc(S) È{^}. We will say that a pointed algebraic poset A is strongly coherent algebraic provided every finite subset of K(A) has finite MUB-closure. Observe that a poset pointed algebraic poset A is strongly coherent algebraic if and only if it is lower-bounded and strongly precoherent algebraic.
In denotational semantics, strongly coherent algebraic posets are usually called strongly algebraic; we adopt the more precise terminology since we have considered both coherent and precoherent posets. In the following results, we prove that [A ® B] is strongly coherent algebraic whenever both A and B are strongly coherent algebraic. We do this by following Abramsky [1] and presenting an alternative characterization for such posets which uses a well-known order-theoretic notion.
Let D be a DCPO. Recall that an isotone map f:D ® D is called a kernel operator provided it is idempotent and contracting; that is, f(x) £ x for all x. Kernel operators preserve all existing joins in D; hence, each kernel operator f is Scott-continuous. It is easy to see that the set Im(f) = {f(d) : d Î D} is a DCPO under the partial ordering inherited from D. Since f is a kernel operator, f has an upper adjoint gf:Im(f) ® D, namely the inclusion map. Since gf is clearly Scott-continuous, the fundamental adjoint relation f(p) £ q Û p £ gf(q) therefore implies that f preserves compact elements. The DCPO Im(f) is called the kernel retract of D under f. The kernel retract of D under f is the largest subset of D whose elements are fixed by f. In light of the previous discussion, it follows that any kernel retract of an algebraic poset is itself an algebraic poset.
There is a well-known intrinsic characterization of kernel retracts: A subset C of a poset P is a kernel retract of P if and only if, for all x Î P, the set Cx = ¯ x ÇC has a largest element. In this case, the kernel operator is given by f(x) = max(Cx).
Lemma 13
If A is a coherent, algebraic poset, then the kernel retracts of A
are (up to isomorphism) precisely the ideal completions Idl(mc(S)), where
S is any subset of K(A).
Let S Í K(A) and consider Dir(mc(S)). Clearly C = Dir(mc(S)) is a pointed algebraic poset. Let x Î A and consider Cx = ¯ x ÇC. Let Dx = ¯ x Çmc(S). Note that Dx ¹ Æ. If F Í Dx is finite then there must exist a compact upper-bound k Î K(A) ǯ x for F. Since MUB(F) Í mc(S), it follows that there is some member of MUB(F) in Dx. Hence, Dx is directed; and ÚDx is the largest element of Cx.
Suppose instead that C is a kernel retract of A and let f denote the kernel operator x ® max(Cx), where Cx = ¯ x ÇC. Note that f(^) = ^; in particular, C is an algebraic poset with ^ as its least element. Since f preserves compact elements, we know K(C) Í K(A). It will suffice to prove that K(C) = mc(K(C)) in A. Certainly K(C) Í mc(K(C)). Let k Î mc(K(C)). We know f(k) Î K(C) and that f(k) £ k. We must prove that f(k) = k.
Suppose by way of contradiction that f(k) < k. We will prove that X = mc(K(C))\{k} is MUB-closed, contradicting the fact that mc(K(C)) is the MUB-closure of K(C). Let F Í X be finite and consider MUB(F). If F Ë eq Ck, then we know that k \not Î MUB(F). If F Í Ck, then any minimal upper-bound for F must be below max(Ck) - hence, we know that k Ï MUB(F) in this case either. Therefore, X is MUB-closed.
[¯]
Before continuing, we present a precise internal description of mc(S) for any subset S of K(A). Let A be a coherent, algebraic poset, and let S0 denote any subset of K(A). For each 0 < n < w, let Sn = È{MUB(F) : F Í Sn-1 is finite}. It is straightforward, albeit somewhat tedious, to prove that the set M = È{Sn : n < w} is mc(S).
We will call a kernel operator f:A ® A finite provided its range is finite. These maps are sometimes called deflations (see, for example, Abramsky [2]). The following result gives us a useful characterization of strongly coherent, algebraic posets.
Lemma 14
For a pointed algebraic poset P, the following statements are
equivalent.
|
where cx is the largest element of mc(S) below x.
Note that each fS so defined is finite and compact-valued (hence compact in [P ® P]). The set F of all such functions is easily seen to be directed. Indeed, if fS,fT Î F, then the function fSÈT is an upper-bound for {fS,fT} in F.
To complete the proof that Claim (1) implies Claim (2), let x Î P.
If k ΠK(P) ǯ x, then letting S = {k} gives us a function fS whose value
at x is k. Hence, (F)(x) ³ x. On the other hand, according to
the internal description of mc(S), fS(x) > ^ if and only if ¯ x ÇS contains an element exceeding ^. It follows that (F)(x) £ x.
To prove that Claim (2) implies Claim (3), let F denote the
set of all finite, compact-valued kernel operators on P. Let D Í F be directed
and such that D º Id. Let f,g Î F. Since f Id and g Id, and since both are compact in [P ® P] by
Lemma 6.4, there exist d1, d2 Î D such that f d1 and g d2. Any
upper-bound in D for d1 and d2 will serve as an upper-bound (in F) for {f,g}.
Hence, F is directed. It is easy to see that F º Id.
To prove that Claim (3) implies Claim (1), let F denote the family of all finite, compact-valued kernel operators on P. Note first that in any pointed poset, the MUB-closure of a singleton {x} always exists - indeed, it is simply {^, x}. One consequence of this fact is that, in a pointed poset, the MUB-closure of Æ exists and is finite. Let S = {s1, ..., sn} Í K(P) be finite and nonempty, and let Sj = {sj}. It follows that fSj can be defined, and is finite and compact-valued; hence, the set {fsj : 1 £ j £ n} has an upper bound f in F.
Let T = Im(f). Since T is a kernel retract of P, we
know that we may assume f(x) = max{t Î T : t £ x}. Since T is finite, it
follows that T is MUB-closed in P. Indeed, if F Í T, and x Î P is any
upper-bound for F, then there exists an upper-bound for F in T, namely f(x). Consequently,
MUB(F) is simply the set of minimal upper-bounds for F in T. Now, fSj f Û f(sj) = sj; thus, we know that S Í T. It follows that mc(S)
exists and is finite; in fact, it is a subset of T.
[¯]
With the previous lemma in hand, it is easy to prove that [A® B] is strongly coherent algebraic whenever both A and B are strongly coherent algebraic.
Lemma 15
If A and B are strongly coherent, algebraic posets, then [A® B] is a strongly coherent, algebraic poset.
|
is easily seen to be a directed family on [A ® B] whose join is the identity map (for [A ® B]).
[¯]
Strongly coherent, algebraic posets are often called bifinite domains. The term ``bifinite" comes from the fact that a strongly coherent, algebraic poset can be represented as a bilimit of a family of finite, pointed posets, namely the collection of its finite, compact-valued kernel retracts (see Abramsky [2] for details). The term ``domain," of course, comes from the fact that these objects form a cartesian-closed category. To make the latter precise, let BiFin denote the full subcategory of Coh whose object class consists of all strongly coherent, algebraic posets. It is routine to prove that this category is closed under the formation of finite cartesian products; hence, we have the following result.
Theorem 16
The category BiFin is cartesian-closed and therefore a category of
domains.
We wish to advise the reader that the kernel operator approach taken to
prove that [A ® B] is bifinite whenever both A and B are bifinite could also have
been used to prove Lemma 6.12 without appealing to the functions F. However, we
chose to describe these functions because their construction provides motivation for the otherwise
rather unnatural finite MUB-closure property.
We have carefully introduced two important categories of domains, namely the categories LDom of lattice-like domains and the category BiFin of bifinite domains. We now present some background information which hints at the richness these categories bring to the study of DCPOs.
Although the objects in these categories arose by taking ``the path of least resistance" for devising compact functions in function spaces, it turns out that the objects in these categories essentially determine all cartesian-closed full subcategories of Algpos . It can be shown that both categories are maximal among cartesian-closed categories of pointed algebraic posets; in fact, it can be proven that any cartesian-closed subcategory of pointed algebraic posets (viewed as a full subcategory of Algpos ) must either be a full subcategory of LDom or of BiFin . Remarkably, there are only four maximal full cartesian-closed subcategories of Algpos , and all four are constructed by taking disjoint unions or finite amalgamations of members of LDom or BiFin . For details on terminology and proofs, we refer the reader to Smyth [32] for the seminal work, and to Gunter [9,10,11] or Jung [14,,].
Often in denotational semantics, focus is placed on w-algebraic posets; that is, algebraic posets whose compact elements form a countable set. An w-algebraic, bifinite domain is called an SFP domain (SFP standing for ``sequence of finite posets"). The SFP domains are so named because their finite, compact-valued kernel retracts form a countable set. The full subcategory SFP whose object class consists of all SFP domains is readily seen to be cartesian-closed; futhermore, it is the largest cartesian-closed category of pointed w-algebraic posets which is also closed under important powerdomain constructions (see Plotkin [23,24] and Smyth [32]). An w-algebraic, coherent poset is often called a ``2/3-SFP" poset, because it satisfies two of the three criteria for being bifinite - namely
We end our exploration of domains by introducing a final important category of domains, one which is both a full subcategory of LDom and of BiFin - the so-called bounded-complete domains.
A DCPO is bounded-complete provided each of its upper-bounded subsets has a join in the DCPO. Nonempty, bounded-complete DCPOs necessarily have a least element. In order theory circles, bounded-complete, algebraic posets are called algebraic semilattices (see Davey and Priestley [6]).
The term ``bounded complete" appears in Abramsky [2]. Note that bounded-complete, algebraic posets are lattice-like domains and bifinite domains. It is therefore not surprising (and easy to prove) that the full subcateogy BCDom of Algpos whose object class consists of all bounded- complete, algebraic posets is cartesian-closed. An w-algebraic, bounded-complete domain is often called a Scott domain. Scott domains are among the most widely used of all denotational models. Indeed, Scott domains were among the first DCPOs to be studied in the context of denotational semantics (see Scott [26], Scott and Strachey [31], and Stoy [35]). The full subcategory SDom of Algpos whose object class consists of all Scott domains is also cartesian-closed.
We conclude this paper by introducing the categories of frames which are dual to the cartesian-closed categories LDom , BiFin , and BCDom . Unfortunately, none of these categories of frames has particularly appealing order-theoretic descriptions; hence, we will mention each only briefly.
In a bialgebraic frame L, we know every compact element is the join of a finite set of CJP elements. For each compact element k in L, we may consider this finite set of CJP elements to be an antichain, which we will call the irredundant CJP decomposition (or ICD) of k and denote by ICD(k). There is a simple connection between ICDs in a precoherent, bialgebraic frame and MUBs in its poset of points: Let L be a precoherent, bialgebraic frame and let pt(L) denote its poset of points. For any finite, nonempty set S Í K(pt(L)), F = MUB(S) if and only if { f : f Î F} is the ICD for Ç{ s : s Î S} (see Lemma 5.2).
Let L be a precoherent, bialgebraic frame. We know that K(L) is a sublattice of L. Let S be any sublattice of K(L). We will say that S is ICD-closed provided S contains the ICD of each of its elements. With this terminology in mind, it is easy to characterize those frames corresponding to bifinite domains. In what follows, we will refer to a sublattice of a bounded lattice B as a subposet of B closed under all finite meets and joins. If B is a bounded lattice, the sublattice generated by a subset S of B is defined to be the smallest sublattice of B containing S. If B is distributive, this sublattice is simply the set of all finite joins of finite meets of members of S.
Lemma 17
For an algebraic poset P, the following statements are equivalent.
|
and let F denote the set of all compact elements in P which correspond to members of S¢. The ICD-closed sublattice of K(L) we seek is simply the sublattice of K(L) generated by the set F¢ = { f : f Î mc(F)}.
On the other hand, suppose that L satisfies Claim (2), and let S Í K(P) be finite. Let S¢ denote the sublattice of K(L) generated by the set { s : s Î S}. Then mc(S) is simply the set F = {k Î K(P) : k Î JP (S¢)}.
[¯]
Of course, the corresponding statement for frames holds as well.
Lemma 18
For a bialgebraic frame L, the following statements are equivalent.
If we let ICD denote the full subcategory of CohFrm whose object class consists of all coherent, bialgebraic frames in which every finite subset of compact elements generates a finite, ICD-closed sublattice, we have the following categorical correspondence.
Theorem 19 labelt:Dueq4 The category BiFin is dually equivalent to the category ICD . The
duality is expressed via the appropriate restriction of the adjunction
(S,pt,l,r).
The frames corresponding to lattice-like domains have the property that their subposets of CJP elements behave something like meet-semilattices. The relevant description is presented below. In what follows, we will use a variation on the dual to MUB-sets. In particular, let P be an algebraic poset, and let X Í K(P). A subset M of K(P) will be called a complete set of maximal lower-bounds for X provided
In addition, we will say that M is locally unique, if whenever k is a compact lower-bound for X, then there is exactly one member of M above k.
Lemma 20
For an algebraic poset P, the following statements are equivalent.
Conversely, suppose that S(P) satisfies Claim (2), and let F Í K(P) have an upper-bound, u. Let F¢ = { f : f Î F}. It follows that u is a lower-bound for F¢ in S(P); hence, there is a unique maximal lower-bound k for F containing u. The compact element k is the join in ¯ u for F that we seek.
[¯]
Of course, we have the corresponding result for bialgebraic frames.
Lemma 21
For a bialgebraic frame L, the following statements are equivalent.
Consequently, if we let LFrm denote the full subcategory of BiAlgFrm whose object class consists of all bialgebraic frames satisfying Lemma 6.21, then we have the following result.
Theorem 22
The category LDom is dually equivalent to the category LFrm . The
duality is expressed via the appropriate restriction of the adjunction
(S,pt,l,r).
We conclude by turning our attention to bounded-complete domains. The frames corresponding to bounded-complete domains also have the property that their subposets of CJP elements behave like meet-semilattices, though the behavior is better controlled in this case. We begin with some simple results characterizing bounded-complete domains.
Lemma 23
For a DCPO P, the following are equivalent.
[¯]
Lemma 24
For an algebraic poset P, the following are equivalent.
[¯]
We will call a poset P a relative meet-semilattice provided every lower-bounded subposet of P is a meet-semilattice. (In this context, we require meet semilattices to possess all finite meets.) In light of Lemmas 4.1 and 4.7, we have the following result.
Lemma 25
For a bialgebraic frame L, the following statements are equivalent.
Let BCFrm denote the full subcategory of Coh whose object class consists of all bialgebraic frames satisfying Lemma 6.25. We have the following result.
Theorem 26
The category BCDom is dually equivalent to the category BCFrm . The
duality is expressed via the appropriate restriction of the adjunction
(S,pt,l,r).
At this point, we can present another result concerning the prime spectrum of lower-bounded, distributive lattices. This result is a direct consequence of Theorem 5.6 and Lemma 6.25.
Theorem 27
For a poset P, the following statements are equivalent.