178
Mathematical Aspects of Logic Programming Semantics
B j ∈ I [k+1,m0] , we now see from the recursion equations that B j ∈ I k . From
the result in Step (3) we now deduce that, for each j, B j ∈ I k+1 . Since it is
obvious that each A i belongs to I k+1 , we obtain that A ∈ T [k+1] (I k+1 ). Thus,
I k+1 ⊆ T [k+1] (I k+1 ), and therefore I k+1 is a supported model for P [k+1] , or a
fixed point of T [k+1] , as required.
Thus, P(α) holds when α is a successor ordinal.
Case ii. α is a limit ordinal.
In this case, it is trivial that (I [α,m] ) is monotonic increasing in m.
Thus, we have only to show that I α is a fixed point of T [α] , that is, a supported model for P [α] , and we show first that I α is a model for P [α] . Let
A ∈ T [α] (I α ). Then there is a clause A ← A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 in
P [α] such that A 1 , . . . , A k1 ∈ I α and B 1 , . . . , B l1 ∈ I α . Indeed, by the definition of P [α] and the hypothesis concerning P , there is n 0 < α such that the
clause A ← A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 belongs to P [n0] . Since the sequence
(I n ) n∈γ is monotone increasing and I α =
, there is
< α such
n<α I n
n 1
that A 1 , . . . , A k1 ∈ I n1 and B 1 , . . . , B l1 ∈ I n1 . Choosing n 2 = max{n 0 , n 1 },
we have A ← A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 ∈ P [n2] and also A 1 , . . . , A k1 ∈ I n2
and B 1 , . . . , B l1 ∈ I n2 . Therefore, on using the induction hypothesis, we have
A ∈ T [n2] (I n2 ) = I n2 ⊆ I α . Hence, T [α] (I α ) ⊆ I α , as required.
To see that I α is supported, let A ∈ I α . By monotonicity of (I n ) n∈γ
again and the identity I α =
, there is a successor ordinal n 0 ≥ 1
n<α I n
such that A ∈ I n for all n such that n 0 ≤ n < α. In particular, we
∞
have A ∈ I n0 =
I [n0,m] . Therefore, there is m 1 ∈ N such that
m=0
A ∈ I [n0 ,m1+1] = T [n0 ] (T
m1 (I n0−1 )). Consequently, there is a clause A ←
[n0 ]
∈ T
m1
A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 in P [n0] such that A 1 , . . . , A k1
[n0] (I n0 −1 ) =
I [n0,m1] ⊆ I n0 ⊆ I α and B 1 , . . . , B k1 ∈ I [n0,m1] . But l(B j ) < n 0 − 1 for each
j, and so no B j belongs to I n0 −1 by Step (3) of the previous case. Therefore,
by this step, no B j belongs to I n0 , and by iterating this we see that, for every m ∈ N, no B j belongs to I n0 +m . Therefore, no B j belongs to I α . Hence,
we have A ∈ T [n0] (I α ) ⊆ T [α] (I α ) or, in other words, that I α ⊆ T [α] (I α ), as
required.
It now follows that P(n) holds for all ordinals n, and this completes the
proof of (b) and (c). In particular, we see that the recursion equations obtained
in Step (1) hold for all ordinals k, and we record this fact in the corollary below.
Indeed, all that is needed to establish these equations is the fact that each I k
is a fixed point of T [k] and to note that the proof just given shows also that
I [P ] is a fixed point of T P . In turn, (d) of the lemma now follows from this
observation by iterating Step (3).
The proof of the lemma is therefore complete.
•
It can be seen here, and it will be seen again later, that the importance of
(d) is the control it gives over negation in the manner illustrated in the proof
just given that I k+1 is a supported model for P [k+1] . It is also worth noting
Mathematical Aspects of Logic Programming Semantics
B j ∈ I [k+1,m0] , we now see from the recursion equations that B j ∈ I k . From
the result in Step (3) we now deduce that, for each j, B j ∈ I k+1 . Since it is
obvious that each A i belongs to I k+1 , we obtain that A ∈ T [k+1] (I k+1 ). Thus,
I k+1 ⊆ T [k+1] (I k+1 ), and therefore I k+1 is a supported model for P [k+1] , or a
fixed point of T [k+1] , as required.
Thus, P(α) holds when α is a successor ordinal.
Case ii. α is a limit ordinal.
In this case, it is trivial that (I [α,m] ) is monotonic increasing in m.
Thus, we have only to show that I α is a fixed point of T [α] , that is, a supported model for P [α] , and we show first that I α is a model for P [α] . Let
A ∈ T [α] (I α ). Then there is a clause A ← A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 in
P [α] such that A 1 , . . . , A k1 ∈ I α and B 1 , . . . , B l1 ∈ I α . Indeed, by the definition of P [α] and the hypothesis concerning P , there is n 0 < α such that the
clause A ← A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 belongs to P [n0] . Since the sequence
(I n ) n∈γ is monotone increasing and I α =
, there is
< α such
n<α I n
n 1
that A 1 , . . . , A k1 ∈ I n1 and B 1 , . . . , B l1 ∈ I n1 . Choosing n 2 = max{n 0 , n 1 },
we have A ← A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 ∈ P [n2] and also A 1 , . . . , A k1 ∈ I n2
and B 1 , . . . , B l1 ∈ I n2 . Therefore, on using the induction hypothesis, we have
A ∈ T [n2] (I n2 ) = I n2 ⊆ I α . Hence, T [α] (I α ) ⊆ I α , as required.
To see that I α is supported, let A ∈ I α . By monotonicity of (I n ) n∈γ
again and the identity I α =
, there is a successor ordinal n 0 ≥ 1
n<α I n
such that A ∈ I n for all n such that n 0 ≤ n < α. In particular, we
∞
have A ∈ I n0 =
I [n0,m] . Therefore, there is m 1 ∈ N such that
m=0
A ∈ I [n0 ,m1+1] = T [n0 ] (T
m1 (I n0−1 )). Consequently, there is a clause A ←
[n0 ]
∈ T
m1
A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 in P [n0] such that A 1 , . . . , A k1
[n0] (I n0 −1 ) =
I [n0,m1] ⊆ I n0 ⊆ I α and B 1 , . . . , B k1 ∈ I [n0,m1] . But l(B j ) < n 0 − 1 for each
j, and so no B j belongs to I n0 −1 by Step (3) of the previous case. Therefore,
by this step, no B j belongs to I n0 , and by iterating this we see that, for every m ∈ N, no B j belongs to I n0 +m . Therefore, no B j belongs to I α . Hence,
we have A ∈ T [n0] (I α ) ⊆ T [α] (I α ) or, in other words, that I α ⊆ T [α] (I α ), as
required.
It now follows that P(n) holds for all ordinals n, and this completes the
proof of (b) and (c). In particular, we see that the recursion equations obtained
in Step (1) hold for all ordinals k, and we record this fact in the corollary below.
Indeed, all that is needed to establish these equations is the fact that each I k
is a fixed point of T [k] and to note that the proof just given shows also that
I [P ] is a fixed point of T P . In turn, (d) of the lemma now follows from this
observation by iterating Step (3).
The proof of the lemma is therefore complete.
•
It can be seen here, and it will be seen again later, that the importance of
(d) is the control it gives over negation in the manner illustrated in the proof
just given that I k+1 is a supported model for P [k+1] . It is also worth noting