210
Mathematical Aspects of Logic Programming Semantics
Claim. Suppose that A ∈ T P ↑ k. Then there is a clause A ← body in
ground(P ) such that A does not occur in body and T P ↑ (k − 1) |= body.
To establish this claim, we first note that it is clear that k ≥ 1. Suppose
that A ∈ T P ↑ k 0 = T P (T P ↑ (k 0 − 1)) and that k 0 is the smallest natural
number with this property. Then there is a clause A ← body in ground(P )
such that T P ↑ (k 0 −1) |= body. By definition of k 0 , we have A ∈ T P ↑ (k 0 −1),
and hence A does not occur in body. Finally, by monotonicity, we obtain that
T P ↑ (k − 1) |= body, as required.
Since P is definite, we have
∞
T P ↑ 0 ⊆ T P ↑ 1 ⊆ · · · ⊆ T P ↑ n ⊆ · · · ⊆ I =
T P ↑ n,
n=1
where T P ↑ n denotes the n-th upward power T
n (∅) of T P , as usual.
P
Given n ∈ N, there are only finitely many atoms A 1 , A 2 , . . . , A m ∈ I
with l(A i ) ≤ n for i = 1, . . . , m, and, by directedness, there is (a smallest)
39
k = k n ∈ N such that A 1 , A 2 , . . . , A m ∈ T P ↑ k n . Consider the atom A i ,
where 1 ≤ i ≤ m, and the following three steps.
(1) We have A i ∈ T P ↑ k n = T P (T P ↑ (k n − 1)). Therefore, there is a
clause
A i ← A
1 (1), . . . , A
m(i) (1)
i
i
in ground(P ) such that A
1 (1), . . . , A
m(i) (1) ∈ T P ↑ (k n − 1). Note that this
i
i
clause may be a unit clause, that is, m(i) ≥ 0, and there may be many such
clauses with head A i ; we choose one of them.
(2) Because A
1 (1), . . . , A
m(i) (1) ∈ T P ↑ (k n − 1) = T P (T P ↑ (k n − 2)),
i
i
there are clauses in ground(P ) as follows.
m(i,1)
A
1 (1) ← A
1 (2), . . . , A
(2)
i
i,1
i,1
m(i,2)
A
2
i (1) ← A i,
1
2 (2), . . . , A i,2 (2)
.
.
.
.
. ←
.
m(i)
m(i,m(i))
A
(1) ← A
1
(2), . . . , A
(2),
i
i,m(i)
i,m(i)
where each of the atoms A
r (2) in each of the bodies belongs to T P
− 2).
i,j
↑ (k n
(3) Because each of the A
r (2) in Step (2) belongs to T P ↑ (k n − 2) =
i,j
T P (T P ↑ (k n − 3)), we have a finite collection of ground clauses (one for each
39 Notice that, depending on l, there may be no atoms A with l(A) ≤ n; this case is
handled by the abuse of notation obtained by allowing m to be 0.
Mathematical Aspects of Logic Programming Semantics
Claim. Suppose that A ∈ T P ↑ k. Then there is a clause A ← body in
ground(P ) such that A does not occur in body and T P ↑ (k − 1) |= body.
To establish this claim, we first note that it is clear that k ≥ 1. Suppose
that A ∈ T P ↑ k 0 = T P (T P ↑ (k 0 − 1)) and that k 0 is the smallest natural
number with this property. Then there is a clause A ← body in ground(P )
such that T P ↑ (k 0 −1) |= body. By definition of k 0 , we have A ∈ T P ↑ (k 0 −1),
and hence A does not occur in body. Finally, by monotonicity, we obtain that
T P ↑ (k − 1) |= body, as required.
Since P is definite, we have
∞
T P ↑ 0 ⊆ T P ↑ 1 ⊆ · · · ⊆ T P ↑ n ⊆ · · · ⊆ I =
T P ↑ n,
n=1
where T P ↑ n denotes the n-th upward power T
n (∅) of T P , as usual.
P
Given n ∈ N, there are only finitely many atoms A 1 , A 2 , . . . , A m ∈ I
with l(A i ) ≤ n for i = 1, . . . , m, and, by directedness, there is (a smallest)
39
k = k n ∈ N such that A 1 , A 2 , . . . , A m ∈ T P ↑ k n . Consider the atom A i ,
where 1 ≤ i ≤ m, and the following three steps.
(1) We have A i ∈ T P ↑ k n = T P (T P ↑ (k n − 1)). Therefore, there is a
clause
A i ← A
1 (1), . . . , A
m(i) (1)
i
i
in ground(P ) such that A
1 (1), . . . , A
m(i) (1) ∈ T P ↑ (k n − 1). Note that this
i
i
clause may be a unit clause, that is, m(i) ≥ 0, and there may be many such
clauses with head A i ; we choose one of them.
(2) Because A
1 (1), . . . , A
m(i) (1) ∈ T P ↑ (k n − 1) = T P (T P ↑ (k n − 2)),
i
i
there are clauses in ground(P ) as follows.
m(i,1)
A
1 (1) ← A
1 (2), . . . , A
(2)
i
i,1
i,1
m(i,2)
A
2
i (1) ← A i,
1
2 (2), . . . , A i,2 (2)
.
.
.
.
. ←
.
m(i)
m(i,m(i))
A
(1) ← A
1
(2), . . . , A
(2),
i
i,m(i)
i,m(i)
where each of the atoms A
r (2) in each of the bodies belongs to T P
− 2).
i,j
↑ (k n
(3) Because each of the A
r (2) in Step (2) belongs to T P ↑ (k n − 2) =
i,j
T P (T P ↑ (k n − 3)), we have a finite collection of ground clauses (one for each
39 Notice that, depending on l, there may be no atoms A with l(A) ≤ n; this case is
handled by the abuse of notation obtained by allowing m to be 0.