# OnF

Authors: Yayan Yuan; Jibo Li
Journal: Abstract and Applied Analysis
 (2014)

---

## Abstract

We introduce a new construction—F
S
+-domain—and prove that the category with F
S
+-domains as objects and Scott continuous functions as morphisms is a Cartesian closed category. We obtain that the Plotkin powerdomain P
P
(
L
) over an F
S-domain L is an F
S
+-domain.


---

## Body

## 1. Introduction

Powerdomains are very important structures in Domain theory, which play an important role in modeling the semantics of nondeterministic programming languages. Three classical powerdomains are the Hoare or lower powerdomain [1], the Smyth or upper powerdomain [2], and the Plotkin or convex powerdomain [3]. They are all free dcpo-algebras over (continuous) dcpos with special binary operators satisfying some equations and inequalities (see [4–12]).In [13], Huth et al. concluded that the Hoare powerdomain P
H
(
L
) over a pointed domain L is a distributive F
S
∨-lattice. In [14], Meng and Kou obtained that the Smyth powerdomain P
S
(
L
) of a Lawson compact domain L is an F
S
∧-domain. Then we have a problem whether the Plotkin powerdomain can be characterized by some special F
S-domain. In this paper, we will introduce a new domain construction called the F
S
+-domain which is a +-semilattice and there exists a directed family of finitely separated Scott continuous and +-semilattice homomorphisms which can approximate i
d
L, where the operation + is Scott continuous which it satisfied the commutative, associative, and idempotency laws. And the category with F
S
+-domains as objects and Scott continuous functions as morphisms is a Cartesian closed category. We will show that the Plotkin powerdomain P
P
(
L
) over an F
S-domain L is an F
S
+-domain, where the Plotkin powerdomain is the free dcpo-semilattice over a continuous dcpo.Next, we collect some basic notions needed in this paper. The reader can also consult [4, 5, 15, 16]. A poset L is called a directed complete poset (a dcpo, for short) if any nonempty directed subset of L has a sup in L. For x
,
y
∈
L, x is way below y (denoted by x
≪
y) if and only if, for all directed subsets D
⊆
L for which sup
⁡
D exists, the relation y
≤
sup
⁡
D implies the existence of a d
∈
D with x
≤
d. A dcpo L is called a continuous domain if, for all x
∈
L, x
=
⋁
↑
↡
x; that is, the set ↡
x
=
{
a
∈
L
:
a
≪
x
} is directed and x
=
⋁
{
a
∈
L
:
a
≪
x
}. For a subset A of L, let ↑
A
=
{
x
∈
L
:
∃
a
∈
A
,
a
≤
x
}, ↓
A
=
{
x
∈
L
:
∃
a
∈
A
,
x
≤
a
}. We use ↑
a (resp., ↓
a) instead of ↑
{
a
} (resp., ↓
{
a
}) when A
=
{
a
}. A is called an upper (resp., a lower) set if A
=
↑
A (resp., A
=
↓
A). If (
L
,
≤
) is a dcpo, we define the Scott topology, denoted by σ
(
L
), which has as its topology of closed sets all directed complete lower subsets, that is, lower sets closed under directed sups. A function f from a dcpo L into a dcpo P is continuous with respect to the Scott topologies if f preserves suprema of directed subsets.Recall the definition ofF
S-domain: a dcpo L is called an F
S-domain if i
d
L is approximated directly by a family of finitely separated Scott continuous functions. A Scott continuous function f
:
L
→
L is called finitely separated if there exists a finite set M
f such that, for each x
∈
L, there exists m
∈
M
f such that f
(
x
)
≤
m
≤
x.


## 2.F
S
+-Domains

### 2.1. Categories ofF
S
+-Domains

For dcposL and P, the function space [
L
→
P
] of all Scott continuous functions from L to P with the pointwise order is a dcpo. Then for dcpo +-semilattices D and E, we conclude that the function space [
D
→
+
E
] of all the Scott continuous and +-semilattice homomorphisms from D to E with the pointwise order is a dcpo +-semilattice from the following theorem, where the operation + satisfies the commutative, associative, and idempotency laws.Theorem 1.
LetD and E be dcpo +-semilattices; then [
D
→
+
E
] is a dcpo +-semilattice.Proof.
For any directed family{
f
j
∈
[
D
→
+
E
]
:
j
∈
J
} and x
∈
D, set f
(
x
)
=
⋁
j
∈
J
f
j
(
x
). It is obvious that f is Scott continuous. Then
(1)
f
(
x
+
y
)
=
⋁
j
∈
J
f
j
(
x
+
y
)
=
⋁
j
∈
J
(
f
j
(
x
)
+
f
j
(
y
)
)
=
(
⋁
j
∈
J
f
j
(
x
)
)
+
(
⋁
j
∈
J
f
j
(
y
)
)
=
f
(
x
)
+
f
(
y
)
.
Sof is also a Scott continuous and +-semilattice homomorphism. Hence [
D
→
+
E
] is a dcpo.
For anyx
∈
D, f
,
g
∈
[
D
→
+
E
], we define (
f
+
g
)
(
x
)
=
f
(
x
)
+
g
(
x
). For a directed set {
x
k
∈
D
:
k
∈
K
}, we have
(2)
(
f
+
g
)
(
⋁
k
∈
K
(
x
k
)
)
=
f
(
⋁
k
∈
K
(
x
k
)
)
+
g
(
⋁
k
∈
K
(
x
k
)
)
=
⋁
k
∈
K
f
(
x
k
)
+
⋁
k
∈
K
g
(
x
k
)
=
⋁
k
∈
K
⋁
k
′
∈
K
[
f
(
x
k
)
+
g
(
x
k
′
)
]
=
⋁
k
∈
K
[
f
(
x
k
)
+
g
(
x
k
)
]
=
⋁
k
∈
K
[
(
f
+
g
)
(
x
k
)
]
.
Thenf
+
g is Scott continuous.
For a pair of pointsx
,
y in D,
(3)
(
f
+
g
)
(
x
+
y
)
=
f
(
x
+
y
)
+
g
(
x
+
y
)
=
(
f
(
x
)
+
f
(
y
)
)
+
(
g
(
x
)
+
g
(
y
)
)
=
(
f
(
x
)
+
g
(
x
)
)
+
(
f
(
y
)
+
g
(
y
)
)
=
(
f
+
g
)
(
x
)
+
(
f
+
g
)
(
y
)
.
That is,f
+
g is a +-semilattice homomorphism. So [
D
→
+
E
] is a +-semilattice.
Finally, by the Scott continuity of the operation +, we obtain the following conclusion. For the sup of the directed set{
f
j
∈
[
D
→
+
E
]
:
j
∈
J
} and g
∈
[
D
→
+
E
], if x
∈
D, then
(4)
[
g
+
(
⋁
j
∈
J
f
j
)
]
(
x
)
=
g
(
x
)
+
(
⋁
j
∈
J
f
j
(
x
)
)
=
⋁
j
∈
J
[
g
(
x
)
+
f
j
(
x
)
]
=
⋁
j
∈
J
[
(
g
+
f
j
)
(
x
)
]
=
[
⋁
j
∈
J
(
g
+
f
j
)
]
(
x
)
.
So+
:
[
D
→
+
E
]
×
[
D
→
+
E
]
→
[
D
→
+
E
] is Scott continuous.
We have obtained that[
D
→
+
E
] is a dcpo +-semilattice.With respect to these special Scott continuous functions, we will introduce some new order structures.Definition 2.
A dcpoL is called an F
S
+-domain if it is a +-semilattice and there exists a directed family of finitely separated Scott continuous and +-semilattice homomorphisms which can approximate i
d
L.For example, anF
S
∧-domain is a continuous dcpo ∧-semilattice where i
d is approximated by a directed family of finitely separated Scott continuous functions preserving finite infs.We know that anF
S
+-domain is an F
S-domain.Theorem 3.
LetD and E be F
S
+-domains; then [
D
→
+
E
] and [
D
→
E
] are F
S
+-domains.Proof.
Suppose that𝒟 and ℰ are approximate identities for D and E, respectively. Then we claim that the family
(5)
𝒟
⊗
ℰ
=
{
δ
⊗
ϵ
:
δ
∈
𝒟
,
ϵ
∈
ℰ
}
,
defined by
(6)
f
⟼
ϵ
2
f
δ
2
,
for f
∈
[
D
→
+
E
] is an approximate identity for [
D
→
+
E
]  where  δ
⊗
ϵ is finitely separated. The proof is similar to the case of F
S-domains.
It suffices to show thatδ
⊗
ϵ
∈
[
D
→
+
E
]
→
+
[
D
→
+
E
]. Firstly, it is obvious that δ
⊗
ϵ is Scott continuous. Secondly, for a pair of points f
,
g
∈
[
D
→
+
E
], we have for any x
∈
D
(7)
[
(
δ
⊗
ϵ
)
(
f
+
g
)
]
(
x
)
=
[
ϵ
2
(
f
+
g
)
δ
2
]
(
x
)
=
ϵ
2
[
f
δ
2
(
x
)
+
g
δ
2
(
x
)
]
=
ϵ
[
ϵ
(
f
δ
2
(
x
)
+
g
δ
2
(
x
)
)
]
=
ϵ
2
f
δ
2
(
x
)
+
ϵ
2
g
δ
2
(
x
)
=
[
ϵ
2
f
δ
2
+
ϵ
2
g
δ
2
]
(
x
)
=
[
(
δ
⊗
ϵ
)
(
f
)
+
(
δ
⊗
ϵ
)
(
g
)
]
(
x
)
.
So we conclude thatδ
⊗
ϵ is a +-semilattice homomorphism. Then [
D
→
+
E
] is an F
S
+-domain. Similarly, [
D
→
E
] is also an F
S
+-domain.Theorem 4.
The category withF
S
+-domains as objects and Scott continuous functions as morphisms is a Cartesian closed category.Note that the category withF
S
+-domains as objects and Scott continuous and +-semilattice homomorphisms as morphisms is not a Cartesian closed category generally, because the evaluation maps do not preserve the finite +-operation.


### 2.2. Classify the Powerdomains

Definition 5 (see [5]).
LetL be a dcpo-algebra equipped with a Scott continuous binary operation + that satisfies the following equations: for any a
,
b
,
c
,
∈
L
(1)
a
+
a
=
a (idempotency law);
(2)
a
+
b
=
b
+
a (commutative law);
(3)
a
+
(
b
+
c
)
=
(
a
+
b
)
+
c (associative law).Then the dcpo-algebra is a commutative idempotent semigroup, called a dcpo-semilattice. The free dcpo-semilattice over a dcpo L is called the convex or Plotkin powerdomain of L and it is denoted by P
P
(
L
).
If the binary operation + satisfies the inequalitya
+
b
≤
a, then we obtain the upper or Smyth powerdomain, and it is denoted by P
S
(
L
), where a
+
b
=
a
∧
b.
Similarly, if the binary operation + satisfiesa
+
b
≥
a, then it is called the lower or Hoare powerdomain, denoted by P
H
(
L
), where a
+
b
=
a
∨
b.Proposition 6 (see [5]).
For subsetsC and D of a preordered set (
L
,
≤
) one has (1)
C
=
H
↓
C;
(2)
C
≤
H
D iff ↓
C
⊆
↓
D;
(3)
C
≪
H
D iff there exists a finite subset F
⊆
L such that C
⊆
↓
F
⊆
↡
D;
(4)
C
=
S
↑
C;
(5)
C
≤
S
D iff ↑
D
⊆
↑
C;
(6)
C
≪
S
D iff D
⊆
int
σ
(
↑
C
) iff D
⊆
↟
C;
(7)
C
=
P
↓
C
∩
↑
C
=
sup
⁡
{
↓
F
∩
↑
F
:
F
≺
C
,
F
⊆
f
in
L
}, where F
≺
C iff F
⊆
↡
C and C
⊆
↟
F;
(8)
C
≤
P
D iff ↓
C
⊆
↓
D and ↑
D
⊆
↑
C;
(9)
C
≪
P
D iff C
≪
H
D and C
≪
S
D.Next, we draw the conclusion that some specialF
S-domain categories concerning the operation + can be used to classify the powerdomains.Theorem 7.
IfL is an F
S-domain, then the convex powerdomain P
P
(
L
) is an F
S
+-domain.Proof.
Suppose thatL is an F
S-domain; then L is a Lawson compact domain. Thus, P
P
(
L
) is also a domain. Assume that ℱ
=
{
f
i
:
L
→
L
}
i
∈
I is the approximate identity for L, where ℱ is a family of finitely separated Scott continuous functions; that is, for any f
i, there exists a finite set M
i
⊆
L such that, for any x
∈
L, there exists some m
∈
M
i such that f
i
(
x
)
≤
m
≤
x. We claim that {
P
(
f
i
)
:
P
P
(
L
)
→
P
P
(
L
)
}
i
∈
I is the approximate identity for P
P
(
L
). It suffices to consider four steps as follows.(1)
P
(
f
i
)
≤
P
(
i
d
). For A
∈
P
P
(
L
), define P
(
f
i
)
(
A
)
=
P
(
f
i
(
A
)
)
=
↓
f
i
(
A
)
∩
↑
f
i
(
A
). By Proposition 6, ↓
f
i
(
A
)
∩
↑
f
i
(
A
)
∈
P
P
(
L
). For any x
∈
A, let M
i
(
A
)
=
{
m
∈
M
i
:
∃
x
∈
A
,
f
i
(
x
)
≤
m
≤
x
}; then f
i
(
x
)
≤
x implies ↓
f
i
(
A
)
⊆
↓
M
i
(
A
)
⊆
↓
A and ↑
A
⊆
↑
M
i
(
A
)
⊆
↑
f
i
(
A
). Hence P
(
f
i
)
(
A
)
=
P
(
f
i
(
A
)
)
≤
P
A.
(2)
sup
⁡
{
P
(
f
i
)
:
i
∈
I
}
=
P
(
i
d
). For any A
∈
P
P
(
L
), it is obvious that sup
⁡
{
P
(
f
i
)
(
A
)
:
i
∈
I
}
≤
A. Suppose A
≰
sup
⁡
{
P
(
f
i
)
(
A
)
:
i
∈
I
}. There is B
∈
P
P
(
L
) such that B
≪
P
A and B
≰
sup
⁡
{
P
(
f
i
)
(
A
)
:
i
∈
I
}. By B
≪
P
A and A
=
sup
⁡
{
↓
F
∩
↑
F
:
F
≺
A
,
F
⊆
f
in
L
}, there is some finite set F
≺
A such that B
≤
↓
F
∩
↑
F. But for any finite set F
≺
A, we have F
=
sup
⁡
{
f
i
(
F
)
:
i
∈
I
}, where F
≺
A iff F
⊆
↡
A and A
⊆
↟
F. Then ↓
F
∩
↑
F
=
sup
⁡
{
↓
f
i
(
F
)
∩
↑
f
i
(
F
)
:
i
∈
I
}
≤
sup
⁡
{
↓
f
i
(
A
)
∩
↑
f
i
(
A
)
:
i
∈
I
}. This is a contradiction. Then we conclude that sup
⁡
{
P
(
f
i
)
:
i
∈
I
}
=
P
(
i
d
).
(3)
P
(
f
i
) is Scott continuous and finitely separated. For a directed family 𝒟 in P
P
(
L
), we have
(8)
P
(
f
i
)
(
sup
⁡
𝒟
)
=
P
(
f
i
(
sup
⁡
𝒟
)
)
=
P
(
sup
⁡
{
f
i
(
D
)
:
D
∈
𝒟
}
)
=
sup
⁡
{
P
(
f
i
(
D
)
)
:
D
∈
𝒟
}
.
ThenP
(
f
i
) is Scott continuous.
For anyA
∈
P
P
(
L
), M
i
(
A
) is a finite set. By ↓
f
i
(
A
)
⊆
↓
M
i
(
A
)
⊆
↓
A and ↑
A
⊆
↑
M
i
(
A
)
⊆
↑
f
i
(
A
), it follows that ↓
M
i
(
A
)
∩
↑
M
i
(
A
)
∈
P
P
(
L
). Let ℳ
i
=
{
↓
M
i
(
A
)
∩
↑
M
i
(
A
)
:
A
∈
P
P
(
L
)
}. Since M
i
(
A
)
⊆
M
i and M
i is finite, it follows that ℳ
i is a finite family of P
P
(
L
). And we have that, for any A, there exists ↓
M
i
(
A
)
∩
↑
M
i
(
A
)
∈
ℳ
i such that P
(
f
i
)
(
A
)
≤
P
↓
M
i
(
A
)
∩
↑
M
i
(
A
)
≤
P
A; that is, P
(
f
i
) is finitely separated.
(4)
P
(
f
i
) is a +-semilattice homomorphism. For A
,
B
∈
P
P
(
L
), since P
P
(
L
) is a +-semilattice, A
+
B
=
↓
(
A
∪
B
)
∩
↑
(
A
∪
B
)
∈
P
P
(
L
):
(9)
P
(
f
i
)
(
A
+
B
)
=
P
(
f
i
)
[
↓
(
A
∪
B
)
∩
↑
(
A
∪
B
)
]
=
↓
f
i
[
↓
(
A
∪
B
)
∩
↑
(
A
∪
B
)
]
∩
↑
f
i
[
↓
(
A
∪
B
)
∩
↑
(
A
∪
B
)
]
=
↓
f
i
(
A
∪
B
)
∩
↑
f
i
(
A
∪
B
)
=
↓
[
(
↓
f
i
(
A
)
∩
↑
f
i
(
A
)
)
ml
∪
(
↓
f
i
(
B
)
∩
↑
f
i
(
B
)
)
]
∩
↑
[
(
↓
f
i
(
A
)
∩
↑
f
i
(
A
)
)
mm
∪
(
↓
f
i
(
B
)
∩
↑
f
i
(
B
)
)
]
=
P
(
f
i
)
(
A
)
+
P
(
f
i
)
(
B
)
.
Then we conclude that {
P
(
f
i
)
:
i
∈
I
} is the approximate identity for P
P
(
L
). Thus the convex powerdomain P
P
(
L
) is an F
S
+-domain.Combined with the work of Huth et al. [13] and Meng and Kou [14], we conclude the following theorem.Theorem 8.
LetL be a domain. Then the following statements hold:(1)
ifL is Lawson compact, then the Smyth powerdomain P
S
(
L
) is an F
S
⋀-domain (in [14]);
(2)
ifL has a least point, then the Hoare powerdomain P
H
(
L
) is a distributive F
S
⋁-lattice (in [13]);
(3)
ifL is an F
S-domain, then the Plotkin powerdomain P
P
(
L
) is an F
S
+-domain.


## 2.1. Categories ofF
S
+-Domains

For dcposL and P, the function space [
L
→
P
] of all Scott continuous functions from L to P with the pointwise order is a dcpo. Then for dcpo +-semilattices D and E, we conclude that the function space [
D
→
+
E
] of all the Scott continuous and +-semilattice homomorphisms from D to E with the pointwise order is a dcpo +-semilattice from the following theorem, where the operation + satisfies the commutative, associative, and idempotency laws.Theorem 1.
LetD and E be dcpo +-semilattices; then [
D
→
+
E
] is a dcpo +-semilattice.Proof.
For any directed family{
f
j
∈
[
D
→
+
E
]
:
j
∈
J
} and x
∈
D, set f
(
x
)
=
⋁
j
∈
J
f
j
(
x
). It is obvious that f is Scott continuous. Then
(1)
f
(
x
+
y
)
=
⋁
j
∈
J
f
j
(
x
+
y
)
=
⋁
j
∈
J
(
f
j
(
x
)
+
f
j
(
y
)
)
=
(
⋁
j
∈
J
f
j
(
x
)
)
+
(
⋁
j
∈
J
f
j
(
y
)
)
=
f
(
x
)
+
f
(
y
)
.
Sof is also a Scott continuous and +-semilattice homomorphism. Hence [
D
→
+
E
] is a dcpo.
For anyx
∈
D, f
,
g
∈
[
D
→
+
E
], we define (
f
+
g
)
(
x
)
=
f
(
x
)
+
g
(
x
). For a directed set {
x
k
∈
D
:
k
∈
K
}, we have
(2)
(
f
+
g
)
(
⋁
k
∈
K
(
x
k
)
)
=
f
(
⋁
k
∈
K
(
x
k
)
)
+
g
(
⋁
k
∈
K
(
x
k
)
)
=
⋁
k
∈
K
f
(
x
k
)
+
⋁
k
∈
K
g
(
x
k
)
=
⋁
k
∈
K
⋁
k
′
∈
K
[
f
(
x
k
)
+
g
(
x
k
′
)
]
=
⋁
k
∈
K
[
f
(
x
k
)
+
g
(
x
k
)
]
=
⋁
k
∈
K
[
(
f
+
g
)
(
x
k
)
]
.
Thenf
+
g is Scott continuous.
For a pair of pointsx
,
y in D,
(3)
(
f
+
g
)
(
x
+
y
)
=
f
(
x
+
y
)
+
g
(
x
+
y
)
=
(
f
(
x
)
+
f
(
y
)
)
+
(
g
(
x
)
+
g
(
y
)
)
=
(
f
(
x
)
+
g
(
x
)
)
+
(
f
(
y
)
+
g
(
y
)
)
=
(
f
+
g
)
(
x
)
+
(
f
+
g
)
(
y
)
.
That is,f
+
g is a +-semilattice homomorphism. So [
D
→
+
E
] is a +-semilattice.
Finally, by the Scott continuity of the operation +, we obtain the following conclusion. For the sup of the directed set{
f
j
∈
[
D
→
+
E
]
:
j
∈
J
} and g
∈
[
D
→
+
E
], if x
∈
D, then
(4)
[
g
+
(
⋁
j
∈
J
f
j
)
]
(
x
)
=
g
(
x
)
+
(
⋁
j
∈
J
f
j
(
x
)
)
=
⋁
j
∈
J
[
g
(
x
)
+
f
j
(
x
)
]
=
⋁
j
∈
J
[
(
g
+
f
j
)
(
x
)
]
=
[
⋁
j
∈
J
(
g
+
f
j
)
]
(
x
)
.
So+
:
[
D
→
+
E
]
×
[
D
→
+
E
]
→
[
D
→
+
E
] is Scott continuous.
We have obtained that[
D
→
+
E
] is a dcpo +-semilattice.With respect to these special Scott continuous functions, we will introduce some new order structures.Definition 2.
A dcpoL is called an F
S
+-domain if it is a +-semilattice and there exists a directed family of finitely separated Scott continuous and +-semilattice homomorphisms which can approximate i
d
L.For example, anF
S
∧-domain is a continuous dcpo ∧-semilattice where i
d is approximated by a directed family of finitely separated Scott continuous functions preserving finite infs.We know that anF
S
+-domain is an F
S-domain.Theorem 3.
LetD and E be F
S
+-domains; then [
D
→
+
E
] and [
D
→
E
] are F
S
+-domains.Proof.
Suppose that𝒟 and ℰ are approximate identities for D and E, respectively. Then we claim that the family
(5)
𝒟
⊗
ℰ
=
{
δ
⊗
ϵ
:
δ
∈
𝒟
,
ϵ
∈
ℰ
}
,
defined by
(6)
f
⟼
ϵ
2
f
δ
2
,
for f
∈
[
D
→
+
E
] is an approximate identity for [
D
→
+
E
]  where  δ
⊗
ϵ is finitely separated. The proof is similar to the case of F
S-domains.
It suffices to show thatδ
⊗
ϵ
∈
[
D
→
+
E
]
→
+
[
D
→
+
E
]. Firstly, it is obvious that δ
⊗
ϵ is Scott continuous. Secondly, for a pair of points f
,
g
∈
[
D
→
+
E
], we have for any x
∈
D
(7)
[
(
δ
⊗
ϵ
)
(
f
+
g
)
]
(
x
)
=
[
ϵ
2
(
f
+
g
)
δ
2
]
(
x
)
=
ϵ
2
[
f
δ
2
(
x
)
+
g
δ
2
(
x
)
]
=
ϵ
[
ϵ
(
f
δ
2
(
x
)
+
g
δ
2
(
x
)
)
]
=
ϵ
2
f
δ
2
(
x
)
+
ϵ
2
g
δ
2
(
x
)
=
[
ϵ
2
f
δ
2
+
ϵ
2
g
δ
2
]
(
x
)
=
[
(
δ
⊗
ϵ
)
(
f
)
+
(
δ
⊗
ϵ
)
(
g
)
]
(
x
)
.
So we conclude thatδ
⊗
ϵ is a +-semilattice homomorphism. Then [
D
→
+
E
] is an F
S
+-domain. Similarly, [
D
→
E
] is also an F
S
+-domain.Theorem 4.
The category withF
S
+-domains as objects and Scott continuous functions as morphisms is a Cartesian closed category.Note that the category withF
S
+-domains as objects and Scott continuous and +-semilattice homomorphisms as morphisms is not a Cartesian closed category generally, because the evaluation maps do not preserve the finite +-operation.


## 2.2. Classify the Powerdomains

Definition 5 (see [5]).
LetL be a dcpo-algebra equipped with a Scott continuous binary operation + that satisfies the following equations: for any a
,
b
,
c
,
∈
L
(1)
a
+
a
=
a (idempotency law);
(2)
a
+
b
=
b
+
a (commutative law);
(3)
a
+
(
b
+
c
)
=
(
a
+
b
)
+
c (associative law).Then the dcpo-algebra is a commutative idempotent semigroup, called a dcpo-semilattice. The free dcpo-semilattice over a dcpo L is called the convex or Plotkin powerdomain of L and it is denoted by P
P
(
L
).
If the binary operation + satisfies the inequalitya
+
b
≤
a, then we obtain the upper or Smyth powerdomain, and it is denoted by P
S
(
L
), where a
+
b
=
a
∧
b.
Similarly, if the binary operation + satisfiesa
+
b
≥
a, then it is called the lower or Hoare powerdomain, denoted by P
H
(
L
), where a
+
b
=
a
∨
b.Proposition 6 (see [5]).
For subsetsC and D of a preordered set (
L
,
≤
) one has (1)
C
=
H
↓
C;
(2)
C
≤
H
D iff ↓
C
⊆
↓
D;
(3)
C
≪
H
D iff there exists a finite subset F
⊆
L such that C
⊆
↓
F
⊆
↡
D;
(4)
C
=
S
↑
C;
(5)
C
≤
S
D iff ↑
D
⊆
↑
C;
(6)
C
≪
S
D iff D
⊆
int
σ
(
↑
C
) iff D
⊆
↟
C;
(7)
C
=
P
↓
C
∩
↑
C
=
sup
⁡
{
↓
F
∩
↑
F
:
F
≺
C
,
F
⊆
f
in
L
}, where F
≺
C iff F
⊆
↡
C and C
⊆
↟
F;
(8)
C
≤
P
D iff ↓
C
⊆
↓
D and ↑
D
⊆
↑
C;
(9)
C
≪
P
D iff C
≪
H
D and C
≪
S
D.Next, we draw the conclusion that some specialF
S-domain categories concerning the operation + can be used to classify the powerdomains.Theorem 7.
IfL is an F
S-domain, then the convex powerdomain P
P
(
L
) is an F
S
+-domain.Proof.
Suppose thatL is an F
S-domain; then L is a Lawson compact domain. Thus, P
P
(
L
) is also a domain. Assume that ℱ
=
{
f
i
:
L
→
L
}
i
∈
I is the approximate identity for L, where ℱ is a family of finitely separated Scott continuous functions; that is, for any f
i, there exists a finite set M
i
⊆
L such that, for any x
∈
L, there exists some m
∈
M
i such that f
i
(
x
)
≤
m
≤
x. We claim that {
P
(
f
i
)
:
P
P
(
L
)
→
P
P
(
L
)
}
i
∈
I is the approximate identity for P
P
(
L
). It suffices to consider four steps as follows.(1)
P
(
f
i
)
≤
P
(
i
d
). For A
∈
P
P
(
L
), define P
(
f
i
)
(
A
)
=
P
(
f
i
(
A
)
)
=
↓
f
i
(
A
)
∩
↑
f
i
(
A
). By Proposition 6, ↓
f
i
(
A
)
∩
↑
f
i
(
A
)
∈
P
P
(
L
). For any x
∈
A, let M
i
(
A
)
=
{
m
∈
M
i
:
∃
x
∈
A
,
f
i
(
x
)
≤
m
≤
x
}; then f
i
(
x
)
≤
x implies ↓
f
i
(
A
)
⊆
↓
M
i
(
A
)
⊆
↓
A and ↑
A
⊆
↑
M
i
(
A
)
⊆
↑
f
i
(
A
). Hence P
(
f
i
)
(
A
)
=
P
(
f
i
(
A
)
)
≤
P
A.
(2)
sup
⁡
{
P
(
f
i
)
:
i
∈
I
}
=
P
(
i
d
). For any A
∈
P
P
(
L
), it is obvious that sup
⁡
{
P
(
f
i
)
(
A
)
:
i
∈
I
}
≤
A. Suppose A
≰
sup
⁡
{
P
(
f
i
)
(
A
)
:
i
∈
I
}. There is B
∈
P
P
(
L
) such that B
≪
P
A and B
≰
sup
⁡
{
P
(
f
i
)
(
A
)
:
i
∈
I
}. By B
≪
P
A and A
=
sup
⁡
{
↓
F
∩
↑
F
:
F
≺
A
,
F
⊆
f
in
L
}, there is some finite set F
≺
A such that B
≤
↓
F
∩
↑
F. But for any finite set F
≺
A, we have F
=
sup
⁡
{
f
i
(
F
)
:
i
∈
I
}, where F
≺
A iff F
⊆
↡
A and A
⊆
↟
F. Then ↓
F
∩
↑
F
=
sup
⁡
{
↓
f
i
(
F
)
∩
↑
f
i
(
F
)
:
i
∈
I
}
≤
sup
⁡
{
↓
f
i
(
A
)
∩
↑
f
i
(
A
)
:
i
∈
I
}. This is a contradiction. Then we conclude that sup
⁡
{
P
(
f
i
)
:
i
∈
I
}
=
P
(
i
d
).
(3)
P
(
f
i
) is Scott continuous and finitely separated. For a directed family 𝒟 in P
P
(
L
), we have
(8)
P
(
f
i
)
(
sup
⁡
𝒟
)
=
P
(
f
i
(
sup
⁡
𝒟
)
)
=
P
(
sup
⁡
{
f
i
(
D
)
:
D
∈
𝒟
}
)
=
sup
⁡
{
P
(
f
i
(
D
)
)
:
D
∈
𝒟
}
.
ThenP
(
f
i
) is Scott continuous.
For anyA
∈
P
P
(
L
), M
i
(
A
) is a finite set. By ↓
f
i
(
A
)
⊆
↓
M
i
(
A
)
⊆
↓
A and ↑
A
⊆
↑
M
i
(
A
)
⊆
↑
f
i
(
A
), it follows that ↓
M
i
(
A
)
∩
↑
M
i
(
A
)
∈
P
P
(
L
). Let ℳ
i
=
{
↓
M
i
(
A
)
∩
↑
M
i
(
A
)
:
A
∈
P
P
(
L
)
}. Since M
i
(
A
)
⊆
M
i and M
i is finite, it follows that ℳ
i is a finite family of P
P
(
L
). And we have that, for any A, there exists ↓
M
i
(
A
)
∩
↑
M
i
(
A
)
∈
ℳ
i such that P
(
f
i
)
(
A
)
≤
P
↓
M
i
(
A
)
∩
↑
M
i
(
A
)
≤
P
A; that is, P
(
f
i
) is finitely separated.
(4)
P
(
f
i
) is a +-semilattice homomorphism. For A
,
B
∈
P
P
(
L
), since P
P
(
L
) is a +-semilattice, A
+
B
=
↓
(
A
∪
B
)
∩
↑
(
A
∪
B
)
∈
P
P
(
L
):
(9)
P
(
f
i
)
(
A
+
B
)
=
P
(
f
i
)
[
↓
(
A
∪
B
)
∩
↑
(
A
∪
B
)
]
=
↓
f
i
[
↓
(
A
∪
B
)
∩
↑
(
A
∪
B
)
]
∩
↑
f
i
[
↓
(
A
∪
B
)
∩
↑
(
A
∪
B
)
]
=
↓
f
i
(
A
∪
B
)
∩
↑
f
i
(
A
∪
B
)
=
↓
[
(
↓
f
i
(
A
)
∩
↑
f
i
(
A
)
)
ml
∪
(
↓
f
i
(
B
)
∩
↑
f
i
(
B
)
)
]
∩
↑
[
(
↓
f
i
(
A
)
∩
↑
f
i
(
A
)
)
mm
∪
(
↓
f
i
(
B
)
∩
↑
f
i
(
B
)
)
]
=
P
(
f
i
)
(
A
)
+
P
(
f
i
)
(
B
)
.
Then we conclude that {
P
(
f
i
)
:
i
∈
I
} is the approximate identity for P
P
(
L
). Thus the convex powerdomain P
P
(
L
) is an F
S
+-domain.Combined with the work of Huth et al. [13] and Meng and Kou [14], we conclude the following theorem.Theorem 8.
LetL be a domain. Then the following statements hold:(1)
ifL is Lawson compact, then the Smyth powerdomain P
S
(
L
) is an F
S
⋀-domain (in [14]);
(2)
ifL has a least point, then the Hoare powerdomain P
H
(
L
) is a distributive F
S
⋁-lattice (in [13]);
(3)
ifL is an F
S-domain, then the Plotkin powerdomain P
P
(
L
) is an F
S
+-domain.



---

*Source: 850298-2014-05-14.xml*