182
Mathematical Aspects of Logic Programming Semantics
With the definition of the level mapping we are currently using and with
the conventions we have made regarding the stratification, we note first that
the equalities P [k] = ground(P 1 ∪P 2 ∪. . .∪P k ) and P (k−1) = ground(P k ) both
hold for k = 1, . . . , m, where P (k) is as defined in the proof of Lemma 6.3.4.
Now P [1] = ground(P 1 ) is definite, even if empty, and so it is immediate
that T P1 ⇑ i(M 0 ) = T P1 ↑ i(M 0 ) for all i and that I 1 = M 1 . So suppose
next that T P k+1 ⇑ i(M k ) =
↑ i(M k ) for all i and that I k+1 = M k+1 for
T P k+1
some k > 0. Then T P k+2 ⇑ 0(M k+1 ) = M k+1 = T P k+2 ↑ 0(M k+1 ) and also
I [k+2,0] = I k+1 = M k+1 = T P k+2 ↑ 0(M k+1 ). So now suppose that T P k+2 ⇑
m(M k+1 ) = T P k+2 ↑ m(M k+1 ) and that I [k+2,m] = T P k+2 ↑ m(M k+1 ) for some
m > 0. Then T P k+2 ⇑ (m + 1)(M k+1 ) = T P k+2 (T P k+2 ⇑ m(M k+1 )) ∪ M k+1
and T P k+2 ↑ (m + 1)(M k+1 ) =
↑ m(M k+1 )) ∪ T P k+2 ↑ m(M k+1 ),
T P k+2 (T P k+2
and it is clear that T P k+2 ⇑ (m + 1)(M k+1 ) ⊆ T P k+2 ↑ (m + 1)(M k+1 ). For
the reverse inclusion, we note that under our present hypotheses we have
↑ (m + 1)(M k+1 ) = T P k+2
⇑ m(M k+1 ), and so
T P k+2
(T P k+2 ⇑ m(M k+1 )) ∪ T P k+2
it suffices to show that T P k+2 ⇑ m(M k+1 ) ⊆ T P k+2
⇑ m(M k+1 ))∪M k+1 or,
(T P k+2
in other words, that I [k+2,m] ⊆ T P (k+1) (I [k+2,m] ) ∪ I k+1 . Since this latter set is
equal to I [k+2,m+1] by the recursion equations of Corollary 6.3.5, the inclusion
we want follows from the monotonicity of the sets I [k+2,m] relative to m. We
conclude, therefore, that T P k+2 ⇑ (m + 1)(M k+1 ) = T P k+2 ↑ (m + 1)(M k+1 ).
Finally, I [k+2,m+1] = I k+1 ∪ T P (k+1) (I [k+2,m] ) = M k+1 ∪ T P k+2 (T P k+2 ↑
=
=
⇑ (m + 1)(M k+1 ) =
m(M k+1 ))
M k+1 ∪ T P k+2 (T P k+2 ⇑ m(M k+1 ))
T P k+2
↑ (m + 1)(M k+1 ), by the conclusions of the previous paragraph. ThereT P k+2
fore, I [k+2,m+1] = T P k+2 ↑ (m + 1)(M k+1 ). From this we obtain, by induction,
the equality I [k+2,m] = T P k+2 ↑ m(M k+1 ) for all m and with it the equality
I k+2 = M k+2 , as required.
•
The details of the induction proof just given also establish the following
proposition.
6.3.10 Proposition Let P = P 1 ∪ . . . ∪ P m be a stratified normal logic
program. Then we have that T P k+1 ⇑ i(M k ) =
↑ i(M k ) for all i and
T P k+1
k = 0, . . . , m − 1.
Finally, we show that locally stratified programs have a unique perfect
model, which is also their total weakly perfect model.
6.3.11 Theorem Let P be locally stratified. Then P has a total weakly perfect model which is a perfect model for P . Furthermore, this model is independent of the choice of level mapping with respect to which P is locally
stratified.
9
Proof: We will employ Theorem 2.5.9 to establish the claim. Let P be locally stratified with respect to some level mapping l
' . Consider the equations
9 In fact, it is known that every locally stratified program has a unique perfect model,
see [Przymusinski, 1988].
Mathematical Aspects of Logic Programming Semantics
With the definition of the level mapping we are currently using and with
the conventions we have made regarding the stratification, we note first that
the equalities P [k] = ground(P 1 ∪P 2 ∪. . .∪P k ) and P (k−1) = ground(P k ) both
hold for k = 1, . . . , m, where P (k) is as defined in the proof of Lemma 6.3.4.
Now P [1] = ground(P 1 ) is definite, even if empty, and so it is immediate
that T P1 ⇑ i(M 0 ) = T P1 ↑ i(M 0 ) for all i and that I 1 = M 1 . So suppose
next that T P k+1 ⇑ i(M k ) =
↑ i(M k ) for all i and that I k+1 = M k+1 for
T P k+1
some k > 0. Then T P k+2 ⇑ 0(M k+1 ) = M k+1 = T P k+2 ↑ 0(M k+1 ) and also
I [k+2,0] = I k+1 = M k+1 = T P k+2 ↑ 0(M k+1 ). So now suppose that T P k+2 ⇑
m(M k+1 ) = T P k+2 ↑ m(M k+1 ) and that I [k+2,m] = T P k+2 ↑ m(M k+1 ) for some
m > 0. Then T P k+2 ⇑ (m + 1)(M k+1 ) = T P k+2 (T P k+2 ⇑ m(M k+1 )) ∪ M k+1
and T P k+2 ↑ (m + 1)(M k+1 ) =
↑ m(M k+1 )) ∪ T P k+2 ↑ m(M k+1 ),
T P k+2 (T P k+2
and it is clear that T P k+2 ⇑ (m + 1)(M k+1 ) ⊆ T P k+2 ↑ (m + 1)(M k+1 ). For
the reverse inclusion, we note that under our present hypotheses we have
↑ (m + 1)(M k+1 ) = T P k+2
⇑ m(M k+1 ), and so
T P k+2
(T P k+2 ⇑ m(M k+1 )) ∪ T P k+2
it suffices to show that T P k+2 ⇑ m(M k+1 ) ⊆ T P k+2
⇑ m(M k+1 ))∪M k+1 or,
(T P k+2
in other words, that I [k+2,m] ⊆ T P (k+1) (I [k+2,m] ) ∪ I k+1 . Since this latter set is
equal to I [k+2,m+1] by the recursion equations of Corollary 6.3.5, the inclusion
we want follows from the monotonicity of the sets I [k+2,m] relative to m. We
conclude, therefore, that T P k+2 ⇑ (m + 1)(M k+1 ) = T P k+2 ↑ (m + 1)(M k+1 ).
Finally, I [k+2,m+1] = I k+1 ∪ T P (k+1) (I [k+2,m] ) = M k+1 ∪ T P k+2 (T P k+2 ↑
=
=
⇑ (m + 1)(M k+1 ) =
m(M k+1 ))
M k+1 ∪ T P k+2 (T P k+2 ⇑ m(M k+1 ))
T P k+2
↑ (m + 1)(M k+1 ), by the conclusions of the previous paragraph. ThereT P k+2
fore, I [k+2,m+1] = T P k+2 ↑ (m + 1)(M k+1 ). From this we obtain, by induction,
the equality I [k+2,m] = T P k+2 ↑ m(M k+1 ) for all m and with it the equality
I k+2 = M k+2 , as required.
•
The details of the induction proof just given also establish the following
proposition.
6.3.10 Proposition Let P = P 1 ∪ . . . ∪ P m be a stratified normal logic
program. Then we have that T P k+1 ⇑ i(M k ) =
↑ i(M k ) for all i and
T P k+1
k = 0, . . . , m − 1.
Finally, we show that locally stratified programs have a unique perfect
model, which is also their total weakly perfect model.
6.3.11 Theorem Let P be locally stratified. Then P has a total weakly perfect model which is a perfect model for P . Furthermore, this model is independent of the choice of level mapping with respect to which P is locally
stratified.
9
Proof: We will employ Theorem 2.5.9 to establish the claim. Let P be locally stratified with respect to some level mapping l
' . Consider the equations
9 In fact, it is known that every locally stratified program has a unique perfect model,
see [Przymusinski, 1988].