155
Supported Model Semantics
5.2.4 Lemma Let P be a normal logic program, let I ∈ I P,2 , and let K ∈ I P,3
be such that K
+ ⊆ I ⊆ B P \ K
− . Then Φ P (K)
+ ⊆ T P (I) ⊆ B P Φ P (K)
− .
Furthermore, if K
+
\
= I = B P \ K
− , so that K is total, then Φ
+
P (K) =
T P (I) = B P \ Φ P (K)
− .
Proof: Suppose that A ∈ Φ P (K)
+ . Then A must be the head of a clause
A ← A , . . . , A , ¬B , . . . , ¬B in ground(P ) with A ∈ K
+
1
k1
1
k2
i
and B j ∈ K
−
for all i = 1, . . . , k 1 and j = 1, . . . , k 2 . By assumption, it follows that for these
values of i and j, A i ∈ I and B j ∈ I, and hence A ∈ T P (I).
For the second inclusion, it suffices to show that Φ P (K)
− ⊆ B P \
T P (I). Let A ∈ Φ P (K)
− . Then, for every clause of the form A ←
A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B k2 in ground(P ), we have some A i ∈ K
− or some
B
+
j ∈ K . Hence, for every such clause, we have some A i ∈ I or some B j ∈ I,
which implies that A ∈ T P (I).
The final statement was established in Proposition 2.4.13.
•
The following straightforward corollary provides the essential link between
the Φ-operator, the single-step operator T P , and convergence in Q.
5.2.5 Corollary Let I n = T
n
P (I) for some I ∈ I P,2 , and let K n = Φ P ↑ n.
Then, for all n N, we obtain K
+
I n B P K
−
n
n .
∈
⊆
⊆
\
The following is a direct consequence of Lemma 5.2.4.
5.2.6 Proposition Let P be a normal logic program, and let (I
+ , I
− ) be a
total three-valued interpretation I for P . Then I is a fixed point of Φ P if and
only if I
+ is a fixed point of T P . Furthermore, if Φ P has exactly one total
fixed point M , then M
+ is the unique fixed point of T P .
Proof: Let I be a fixed point of Φ P . Then I
+ ⊆ I
+ ⊆ B P \ I
− , and by
Lemma 5.2.4 we obtain I
+ = Φ P (I)
+ ⊆ T P (I
+ ) ⊆ B P \ Φ P (I)
− = B P \ I
− =
I
+ . Conversely, let I
+ be a fixed point of T P . By Lemma 5.2.4, we obtain
Φ P (I)
+ = T P (I
+ ) = I
+ = B P \ I
− = B P \ Φ P (I)
− , and therefore Φ P (I)
+ =
I
+ and Φ P (I)
− = I
− . The last statement now follows immediately.
•
Convergence of iterates with respect to the Cantor topology can now be
described, as follows.
5.2.7 Proposition Let P be a normal logic program, and assume that M =
Φ P ↑ ω is total. Then T
n (∅) converges in Q to M
+ , and M
+ is the unique
P
supported model M P for P .
Proof:
Using the notation from Corollary 5.2.5, we obtain M
+ = K
+ and
n
M
− = K
− . Since M is total, we obtain from Propositions 3.3.5 and 5.2.6
n
that M
+ is the limit in Q of the sequence I n . Since totality of Φ P ↑ ω implies
that it is the unique fixed point of Φ P , it therefore equals (M
+ , M
− ), so that
M
+ is the unique fixed point of T P by Proposition 5.2.6.
•
Supported Model Semantics
5.2.4 Lemma Let P be a normal logic program, let I ∈ I P,2 , and let K ∈ I P,3
be such that K
+ ⊆ I ⊆ B P \ K
− . Then Φ P (K)
+ ⊆ T P (I) ⊆ B P Φ P (K)
− .
Furthermore, if K
+
\
= I = B P \ K
− , so that K is total, then Φ
+
P (K) =
T P (I) = B P \ Φ P (K)
− .
Proof: Suppose that A ∈ Φ P (K)
+ . Then A must be the head of a clause
A ← A , . . . , A , ¬B , . . . , ¬B in ground(P ) with A ∈ K
+
1
k1
1
k2
i
and B j ∈ K
−
for all i = 1, . . . , k 1 and j = 1, . . . , k 2 . By assumption, it follows that for these
values of i and j, A i ∈ I and B j ∈ I, and hence A ∈ T P (I).
For the second inclusion, it suffices to show that Φ P (K)
− ⊆ B P \
T P (I). Let A ∈ Φ P (K)
− . Then, for every clause of the form A ←
A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B k2 in ground(P ), we have some A i ∈ K
− or some
B
+
j ∈ K . Hence, for every such clause, we have some A i ∈ I or some B j ∈ I,
which implies that A ∈ T P (I).
The final statement was established in Proposition 2.4.13.
•
The following straightforward corollary provides the essential link between
the Φ-operator, the single-step operator T P , and convergence in Q.
5.2.5 Corollary Let I n = T
n
P (I) for some I ∈ I P,2 , and let K n = Φ P ↑ n.
Then, for all n N, we obtain K
+
I n B P K
−
n
n .
∈
⊆
⊆
\
The following is a direct consequence of Lemma 5.2.4.
5.2.6 Proposition Let P be a normal logic program, and let (I
+ , I
− ) be a
total three-valued interpretation I for P . Then I is a fixed point of Φ P if and
only if I
+ is a fixed point of T P . Furthermore, if Φ P has exactly one total
fixed point M , then M
+ is the unique fixed point of T P .
Proof: Let I be a fixed point of Φ P . Then I
+ ⊆ I
+ ⊆ B P \ I
− , and by
Lemma 5.2.4 we obtain I
+ = Φ P (I)
+ ⊆ T P (I
+ ) ⊆ B P \ Φ P (I)
− = B P \ I
− =
I
+ . Conversely, let I
+ be a fixed point of T P . By Lemma 5.2.4, we obtain
Φ P (I)
+ = T P (I
+ ) = I
+ = B P \ I
− = B P \ Φ P (I)
− , and therefore Φ P (I)
+ =
I
+ and Φ P (I)
− = I
− . The last statement now follows immediately.
•
Convergence of iterates with respect to the Cantor topology can now be
described, as follows.
5.2.7 Proposition Let P be a normal logic program, and assume that M =
Φ P ↑ ω is total. Then T
n (∅) converges in Q to M
+ , and M
+ is the unique
P
supported model M P for P .
Proof:
Using the notation from Corollary 5.2.5, we obtain M
+ = K
+ and
n
M
− = K
− . Since M is total, we obtain from Propositions 3.3.5 and 5.2.6
n
that M
+ is the limit in Q of the sequence I n . Since totality of Φ P ↑ ω implies
that it is the unique fixed point of Φ P , it therefore equals (M
+ , M
− ), so that
M
+ is the unique fixed point of T P by Proposition 5.2.6.
•