177
Stable and Perfect Model Semantics
(1) We establish the recursion equations
6 :
I [k+1,0] = I k
I [k+1,m+1] = I k ∪ T P (k) (I [k+1,m] )
and the first is immediate. Putting m = 0, we have I [k+1,1] = T [k+1] (I k ) =
T [k] (I k ) ∪ T P (k) (I k ) = I k ∪ T P (k) (I k ) = I k ∪ T P (k) (I [k+1,0] ), using the fact that
I k is a fixed point of T [k] . Now suppose that the second of these equations
holds for some m > 0. Then
I [k+1,(m+1)+1] = T [k+1] (I [k+1,m+1] )
= T [k] (I [k+1,m+1] ) ∪ T P (k) (I [k+1,m+1] )
= T [k] (I k ∪ T P (k) (I [k+1,m] )) ∪ T P (k) (I [k+1,m+1] ),
and it suffices to show that T [k] (I k ∪ T P (k) (I [k+1,m] )) = I k . So suppose that
A ∈ T [k] (I k ∪ T P (k) (I [k+1,m] )). Thus, there is a clause in P [k] of the form
A ← A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 , where A 1 , . . . , A k1 ∈ I k ∪ T P (k) (I [k+1,m] )
and B 1 , . . . , B l1 ∈ I k ∪ T P (k) (I [k+1,m] ). But then level considerations and the
hypothesis concerning P imply that A 1 , . . . , A k1 ∈ I k and B 1 , . . . , B l1 ∈ I k .
Therefore, A ∈ T [k] (I k ) = I k , and the inclusion T [k] (I k ∪ T P (k) (I [k+1,m] )) ⊆ I k
holds. The reverse inclusion is demonstrated in like fashion, showing that the
second of the recursion equations holds with m replaced by m + 1 and, hence,
by induction on m
m
(2) We have the inclusions T P (k) (I k ) ⊆ T P (k) (I k ∪ T P (k) (I k )) ⊆ T P (k) (I k ∪
T P (k) (I k ∪ T P (k) (I k ))) . . .. These inclusions are established by methods similar
to those we have just employed, and we omit the details.
It is now clear from this fact and the recursion equations in Step (1)
that (I [k+1,m] ), or (I [α,m] ), is monotonic increasing in m. Since monotonic
increasing sequences converge to their union in Q, and I [k+1,m] is an iterate
of I k , it now follows by Theorem 5.4.2 that I k+1 is a model for P [k+1] .
(3) If B ∈ B P and l(B) < k, then B ∈ I k+1 if and only if B ∈ I k .
Indeed, if B ∈ I k , then it is clear from the recursion equations of Step (1)
that B ∈ I k+1 . On the other hand, if B ∈ I k , then it is equally clear from
the recursion equations and level considerations that, for every m ∈ N, B ∈
I [k+1,m] and, hence, that B ∈ I k+1 , as required.
(4) I k+1 is a supported model for P [k+1] .
To see that this claim holds, suppose that A ∈ I k+1 =
∞
m=0 I [k+1,m] . Then
there is m 0 ∈ N such that A ∈ I
T
m+1
[k+1,m+1] =
(I
[k+1]
Thus, A
T
(T
m0 (I )) = T
(I
). Hence,
k ) for all m ≥ m 0 .
∈ [k+1]
k
[k+1] [k+1,m0 ]
there is
[k+1]
a clause
A ← A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 in P [k+1] such that each A i ∈ I [k+1,m0 ] and
no B j ∈ I [k+1,m0] . But l(B j ) < k for each j since P is locally stratified. Since
6 As shown here, it results from these equations that the process of constructing
I [k+1,m+1] in terms of I [k+1,m] is inflationary, where, formally, an operator G defined on
a collection of sets is said to be inflationary if X ⊆ G(X) for each set X in the given
collection; see also the corresponding recursion equations in Corollary 6.3.5.
, that it holds for all .
Précédent

- 208/305

Suivant