14
Mathematical Aspects of Logic Programming Semantics
a compact element in (T , ≤) for each x ∈ X, and the set {x ∈ X | v(x) = ⊥}
is finite.
The structural properties of I(X, T ) may be summarized in the following
result.
20
1.3.2 Theorem Let X be a non-empty set, let (T , ≤) be an ordered set of
truth values with bottom element ⊥, and let I(X, T ) be endowed with the
pointwise ordering and bottom element just defined.
(a) If (T , ≤) is a partially ordered set, then so is I(X, T ).
(b) If (T , ≤) is an ω-complete partial order, then so is I(X, T ).
(c) If (T , ≤) is a complete partial order, then so is I(X, T ).
(d) If (T , ≤) is a complete upper semi-lattice, then so is I(X, T ).
(e) If (T , ≤) is a complete lattice, then so is I(X, T ).
(f) If (T , ≤) is a Scott domain, then so is I(X, T ). In this case, the compact
elements of I(X, T ) are the finite valuations.
Proof: (a) As already noted, it is routine in this case to verify that the ordering
on I(X, T ) is a partial ordering, with bottom element as already specified.
(b) The argument in this case is similar to the next and is omitted.
(c) If M ⊆ I(X, T ) is directed, then it is easy to check that, for each
x ∈ X, the set {v(x) | v ∈ M } is directed and hence has a supremum in T .
It is now clear that the valuation
v defined on X by v (x) =
v(x)
M
M
{
|
v ∈ M } is the suprem
um, M , of M in I(X, T ). Indeed, for any directed
subset M ⊆ I(X, T ), M satisfies the following relationship: for eac
h x ∈ X,
( M )(x) = (M (x)), where M (x) denotes the set {v(x) | v ∈ M }.
(d) By the argument used in (c), the supremum M exists for any directed
subset M of I(X, T ). Also,
n for any subset M of I
(X, T ), we have that
n
M
exists and is defined by ( M )(x) = (M (x)) for each x ∈ X, where again
M (x) denotes the set {v(x) | v ∈ M }.
(e) It is clear from the argument in
n
(c) that any subset M of I(X, T ) has
a supremum in I(X, T ), and, from (d), M has an infimum in I(X, T ).
(f) We begin by showing that the finite valuations are compact elements.
Suppose that v is a finite valuation and that {x ∈ X | v(x) = ⊥} =
{x 1 , . . . , x n }. Suppose that
M = {u k | k ∈ K} is a directed set of valuations
in I(X, T ) such that v [ M
. Let x i be an arbitrary element of {x 1 , . . . , x
n }.
Then we have that v(x i ) ≤ M (x i ) = (M (x i )), that v(x i ) is a compact
element, and that {u k (x i ); k ∈ K} is directed. Therefore, there is u ki ∈ M
such that v(x i ) ≤ u ki (x i ), and we obtain such u ki for i = 1, . . . , n. Since M is
directed, there is u ∈ M such that u ki [ u for i = 1, . . . , n, and it now clearly
follows that v [ u. Hence, v is compact.
20 For further details here and in the next three subsections, see [Seda, 2002].
Mathematical Aspects of Logic Programming Semantics
a compact element in (T , ≤) for each x ∈ X, and the set {x ∈ X | v(x) = ⊥}
is finite.
The structural properties of I(X, T ) may be summarized in the following
result.
20
1.3.2 Theorem Let X be a non-empty set, let (T , ≤) be an ordered set of
truth values with bottom element ⊥, and let I(X, T ) be endowed with the
pointwise ordering and bottom element just defined.
(a) If (T , ≤) is a partially ordered set, then so is I(X, T ).
(b) If (T , ≤) is an ω-complete partial order, then so is I(X, T ).
(c) If (T , ≤) is a complete partial order, then so is I(X, T ).
(d) If (T , ≤) is a complete upper semi-lattice, then so is I(X, T ).
(e) If (T , ≤) is a complete lattice, then so is I(X, T ).
(f) If (T , ≤) is a Scott domain, then so is I(X, T ). In this case, the compact
elements of I(X, T ) are the finite valuations.
Proof: (a) As already noted, it is routine in this case to verify that the ordering
on I(X, T ) is a partial ordering, with bottom element as already specified.
(b) The argument in this case is similar to the next and is omitted.
(c) If M ⊆ I(X, T ) is directed, then it is easy to check that, for each
x ∈ X, the set {v(x) | v ∈ M } is directed and hence has a supremum in T .
It is now clear that the valuation
v defined on X by v (x) =
v(x)
M
M
{
|
v ∈ M } is the suprem
um, M , of M in I(X, T ). Indeed, for any directed
subset M ⊆ I(X, T ), M satisfies the following relationship: for eac
h x ∈ X,
( M )(x) = (M (x)), where M (x) denotes the set {v(x) | v ∈ M }.
(d) By the argument used in (c), the supremum M exists for any directed
subset M of I(X, T ). Also,
n for any subset M of I
(X, T ), we have that
n
M
exists and is defined by ( M )(x) = (M (x)) for each x ∈ X, where again
M (x) denotes the set {v(x) | v ∈ M }.
(e) It is clear from the argument in
n
(c) that any subset M of I(X, T ) has
a supremum in I(X, T ), and, from (d), M has an infimum in I(X, T ).
(f) We begin by showing that the finite valuations are compact elements.
Suppose that v is a finite valuation and that {x ∈ X | v(x) = ⊥} =
{x 1 , . . . , x n }. Suppose that
M = {u k | k ∈ K} is a directed set of valuations
in I(X, T ) such that v [ M
. Let x i be an arbitrary element of {x 1 , . . . , x
n }.
Then we have that v(x i ) ≤ M (x i ) = (M (x i )), that v(x i ) is a compact
element, and that {u k (x i ); k ∈ K} is directed. Therefore, there is u ki ∈ M
such that v(x i ) ≤ u ki (x i ), and we obtain such u ki for i = 1, . . . , n. Since M is
directed, there is u ∈ M such that u ki [ u for i = 1, . . . , n, and it now clearly
follows that v [ u. Hence, v is compact.
20 For further details here and in the next three subsections, see [Seda, 2002].