180
Mathematical Aspects of Logic Programming Semantics
for some m 0 > 0. Let A ∈ I [k+1,m0+1] = T [k+1] (T
m0 (I k )). Then there is
[k+1]
a clause A ← A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 in P [k+1] such that A 1 , . . . , A k1 ∈
T
m0 (I k ) = I [k+1,m0] and B 1 , . . . , B l1 ∈ I [k+1,m0] . But l(B j ) < k for each j.
[k+1]
Applying Lemma 6.3.4 (d) we see that no B j belongs to I [P ] , and consequently
no B j belongs to J because J ⊆ I [P ] . Since I [k+1,m0] ⊆ J by assumption, we
have A 1 , . . . , A k1 ∈ J. Therefore, A ∈ T [k+1] (J) ⊆ T P (J) ⊆ J, and from this
we obtain that I [k+1,m0+1] ⊆ J, as required to complete the proof in this case.
Case ii. α is a limit ordinal. In this case, I α =
I n and I n ⊆ J for all
n<α
n < α by hypothesis. Therefore, I α ⊆ J, as required.
Thus, the result follows by transfinite induction.
•
We can strengthen Theorem 6.3.6.
6.3.7 Theorem Suppose that P is a normal logic program which is locally
stratified with respect to a level mapping l : B P → γ, where γ is a countable
ordinal. Then I [P ] is a perfect model for P .
Proof: Suppose that there is a model N for P which is preferable to I [P ] (and
therefore distinct from I [P ] ); we will derive a contradiction.
First note that N \ I [P ] must be non-empty; otherwise, we have N ⊆ I [P ] .
But this inclusion forces equality of N and I [P ] since I [P ] is a minimal model
for P , and therefore N and I [P ] are not distinct. This means that there is a
ground atom A in N \ I [P ] , which can be chosen so that l(A) has minimum
value; let B be a ground atom in I [P ] \ N corresponding to A in accordance
with Definition 2.5.2 and satisfying l(A) > l(B).
Next we note that T [1] (N ) ⊆ T P (N ) ⊆ N , since N is a model for P . Hence,
N is a model for P [1] , which implies that I 1 ⊆ N since I 1 is the least model for
the definite program P [1] . Therefore, B can be chosen so that B ∈ I n0 \N , with
minimal
n 0 > 1. Now n 0 cannot be a limit ordinal; otherwise, we would have
I n0 =
I m , from which we would conclude that B ∈ I m \ N for some
m
and therefore B can be chosen so that B ∈ I [n0,m0] \ N , where m 0 is such that
I [n0,m1] \ N = ∅ whenever m 1 < m 0 , ; indeed, since I 1 ⊆ N , we must have
n 0 > 1 and m 0 ≥ 1 also. Consequently, B ∈ T [n0] (I [n0,m0−1] )\N , showing that
there is a clause B ← C 1 , . . . , C k1 , ¬D 1 , . . . , ¬D l1 in P [n0 ] with the property
that each C i ∈ I [n0,m0−1] and no D j ∈ I [n0,m0−1] . Since l(D j ) < n 0 − 1 for
each j, we see that none of the D j belong to I [P ] by Lemma 6.3.4 (d). But
all the C i , if there are any, must belong to N by the choice of the numbers
n 0 and m 0 . Moreover, there must be at least one D j and indeed at least one
belonging to N . For if there were no D j or we had each D j ∈ N , then we
would have B ∈ T Pn 0 (N ) ⊆ T P (N ) ⊆ N , using again the fact that N is a
model for P . But this leads to the conclusion that B ∈ N , which is contrary
to B ∈ I [P ] \ N . Thus, there is a D = D j ∈ N \ I [P ] , for some j, satisfying
l(D) < l(B) < l(A). Since A was chosen in N \ I [P ] to have smallest level, we
have a contradiction.
Mathematical Aspects of Logic Programming Semantics
for some m 0 > 0. Let A ∈ I [k+1,m0+1] = T [k+1] (T
m0 (I k )). Then there is
[k+1]
a clause A ← A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 in P [k+1] such that A 1 , . . . , A k1 ∈
T
m0 (I k ) = I [k+1,m0] and B 1 , . . . , B l1 ∈ I [k+1,m0] . But l(B j ) < k for each j.
[k+1]
Applying Lemma 6.3.4 (d) we see that no B j belongs to I [P ] , and consequently
no B j belongs to J because J ⊆ I [P ] . Since I [k+1,m0] ⊆ J by assumption, we
have A 1 , . . . , A k1 ∈ J. Therefore, A ∈ T [k+1] (J) ⊆ T P (J) ⊆ J, and from this
we obtain that I [k+1,m0+1] ⊆ J, as required to complete the proof in this case.
Case ii. α is a limit ordinal. In this case, I α =
I n and I n ⊆ J for all
n<α
n < α by hypothesis. Therefore, I α ⊆ J, as required.
Thus, the result follows by transfinite induction.
•
We can strengthen Theorem 6.3.6.
6.3.7 Theorem Suppose that P is a normal logic program which is locally
stratified with respect to a level mapping l : B P → γ, where γ is a countable
ordinal. Then I [P ] is a perfect model for P .
Proof: Suppose that there is a model N for P which is preferable to I [P ] (and
therefore distinct from I [P ] ); we will derive a contradiction.
First note that N \ I [P ] must be non-empty; otherwise, we have N ⊆ I [P ] .
But this inclusion forces equality of N and I [P ] since I [P ] is a minimal model
for P , and therefore N and I [P ] are not distinct. This means that there is a
ground atom A in N \ I [P ] , which can be chosen so that l(A) has minimum
value; let B be a ground atom in I [P ] \ N corresponding to A in accordance
with Definition 2.5.2 and satisfying l(A) > l(B).
Next we note that T [1] (N ) ⊆ T P (N ) ⊆ N , since N is a model for P . Hence,
N is a model for P [1] , which implies that I 1 ⊆ N since I 1 is the least model for
the definite program P [1] . Therefore, B can be chosen so that B ∈ I n0 \N , with
minimal
n 0 > 1. Now n 0 cannot be a limit ordinal; otherwise, we would have
I n0 =
I m , from which we would conclude that B ∈ I m \ N for some
m
and therefore B can be chosen so that B ∈ I [n0,m0] \ N , where m 0 is such that
I [n0,m1] \ N = ∅ whenever m 1 < m 0 , ; indeed, since I 1 ⊆ N , we must have
n 0 > 1 and m 0 ≥ 1 also. Consequently, B ∈ T [n0] (I [n0,m0−1] )\N , showing that
there is a clause B ← C 1 , . . . , C k1 , ¬D 1 , . . . , ¬D l1 in P [n0 ] with the property
that each C i ∈ I [n0,m0−1] and no D j ∈ I [n0,m0−1] . Since l(D j ) < n 0 − 1 for
each j, we see that none of the D j belong to I [P ] by Lemma 6.3.4 (d). But
all the C i , if there are any, must belong to N by the choice of the numbers
n 0 and m 0 . Moreover, there must be at least one D j and indeed at least one
belonging to N . For if there were no D j or we had each D j ∈ N , then we
would have B ∈ T Pn 0 (N ) ⊆ T P (N ) ⊆ N , using again the fact that N is a
model for P . But this leads to the conclusion that B ∈ N , which is contrary
to B ∈ I [P ] \ N . Thus, there is a D = D j ∈ N \ I [P ] , for some j, satisfying
l(D) < l(B) < l(A). Since A was chosen in N \ I [P ] to have smallest level, we
have a contradiction.