179
Stable and Perfect Model Semantics
that the construction produces a monotonic increasing sequence by means of
a non-monotonic operator.
7
6.3.5 Corollary Suppose the hypothesis of Lemma 6.3.4 holds. Then the
following statements hold.
(a) For all ordinals n and all m ∈ N, we have the recursion equations
I [n+1,0] = I n , and
I [n+1,m+1] = I n ∪ T P (n) (I [n+1,m] ).
(b) If P is, in fact, locally hierarchical, then for every ordinal n ≥ 1 we have
I [n+1,m] = I n ∪ T P (n) (I n ) for all m ∈ N, where P (n) is defined as in the
proof of Lemma 6.3.4, and therefore the iterates stabilize after one step.
Proof: That (a) holds has already been noted in the proof of Lemma 6.3.4.
For (b), it suffices to prove that T P (n) (I n ) = T P (n) (I n ∪ T P (n) (I n )). So
suppose therefore that A ∈ T P (n) (I n ∪ T P (n) (I n )). Then there is a clause A ←
A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 in P (n) such that A 1 , . . . , A k1 ∈ I n ∪ T P (n) (I n )
and B 1 , . . . , B k1 ∈ I n ∪ T P (n) (I n ). From these statements and by level considerations, we have A 1 , . . . , A k1 ∈ I n and B 1 , . . . , B k1 ∈ I n . Therefore,
A ∈ T P (n) (I n ), so that T P (n) (I n ∪ T P (n) (I n )) ⊆ T P (n) (I n ). The reverse inclusion is established similarly to complete the proof.
•
Statement (b) of this corollary makes the calculation of iterates very easy
to perform in the case of locally hierarchical programs.
6.3.6 Theorem Suppose that P is a normal logic program which is locally
stratified with respect to the level mapping l : B P → γ. Then I [P ] is a minimal
supported model for P .
Proof: That I [P ] is a supported model for P follows from the proof of
Lemma 6.3.4, and so it remains to show that I [P ] is minimal. To do this,
we establish by transfinite induction the following proposition: “if J ⊆ I [P ]
and T P (J) ⊆ J, then I n ⊆ J for all n ∈ γ, where n ≥ 1”, and this clearly
suffices. Indeed, T [1] (J) ⊆ T P (J) ⊆ J, and therefore J is a model for P [1] .
But, as already noted in proving Lemma 6.3.4, I 1 is the least model for P [1]
by construction, since P [1] is definite. Therefore, I 1 ⊆ J, and the proposition
holds with n = 1.
Now assume that the proposition holds for all ordinals n < α for some
ordinal α ∈ γ, where α > 1; we show that it holds with n = α.
Case i. α = k + 1 is a successor ordinal, where k > 0. We have I k ⊆
J. We show by induction on m that I [k+1,m] ⊆ J for all m. Indeed, with
m = 0, we have I [k+1,0] = I k ⊆ J. Suppose, therefore, that I [k+1,m0] ⊆ J
7 Lemma 6.3.4 plays a role here similar to that played by [Apt et al., 1988, Lemma 10].
Stable and Perfect Model Semantics
that the construction produces a monotonic increasing sequence by means of
a non-monotonic operator.
7
6.3.5 Corollary Suppose the hypothesis of Lemma 6.3.4 holds. Then the
following statements hold.
(a) For all ordinals n and all m ∈ N, we have the recursion equations
I [n+1,0] = I n , and
I [n+1,m+1] = I n ∪ T P (n) (I [n+1,m] ).
(b) If P is, in fact, locally hierarchical, then for every ordinal n ≥ 1 we have
I [n+1,m] = I n ∪ T P (n) (I n ) for all m ∈ N, where P (n) is defined as in the
proof of Lemma 6.3.4, and therefore the iterates stabilize after one step.
Proof: That (a) holds has already been noted in the proof of Lemma 6.3.4.
For (b), it suffices to prove that T P (n) (I n ) = T P (n) (I n ∪ T P (n) (I n )). So
suppose therefore that A ∈ T P (n) (I n ∪ T P (n) (I n )). Then there is a clause A ←
A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 in P (n) such that A 1 , . . . , A k1 ∈ I n ∪ T P (n) (I n )
and B 1 , . . . , B k1 ∈ I n ∪ T P (n) (I n ). From these statements and by level considerations, we have A 1 , . . . , A k1 ∈ I n and B 1 , . . . , B k1 ∈ I n . Therefore,
A ∈ T P (n) (I n ), so that T P (n) (I n ∪ T P (n) (I n )) ⊆ T P (n) (I n ). The reverse inclusion is established similarly to complete the proof.
•
Statement (b) of this corollary makes the calculation of iterates very easy
to perform in the case of locally hierarchical programs.
6.3.6 Theorem Suppose that P is a normal logic program which is locally
stratified with respect to the level mapping l : B P → γ. Then I [P ] is a minimal
supported model for P .
Proof: That I [P ] is a supported model for P follows from the proof of
Lemma 6.3.4, and so it remains to show that I [P ] is minimal. To do this,
we establish by transfinite induction the following proposition: “if J ⊆ I [P ]
and T P (J) ⊆ J, then I n ⊆ J for all n ∈ γ, where n ≥ 1”, and this clearly
suffices. Indeed, T [1] (J) ⊆ T P (J) ⊆ J, and therefore J is a model for P [1] .
But, as already noted in proving Lemma 6.3.4, I 1 is the least model for P [1]
by construction, since P [1] is definite. Therefore, I 1 ⊆ J, and the proposition
holds with n = 1.
Now assume that the proposition holds for all ordinals n < α for some
ordinal α ∈ γ, where α > 1; we show that it holds with n = α.
Case i. α = k + 1 is a successor ordinal, where k > 0. We have I k ⊆
J. We show by induction on m that I [k+1,m] ⊆ J for all m. Indeed, with
m = 0, we have I [k+1,0] = I k ⊆ J. Suppose, therefore, that I [k+1,m0] ⊆ J
7 Lemma 6.3.4 plays a role here similar to that played by [Apt et al., 1988, Lemma 10].