176
Mathematical Aspects of Logic Programming Semantics
following.
I 1 = {penguin(tweety)}
I 2 = I 1 ∪ {bird(bob), bird(tweety)}
I 3 = I 2 ∪ {flies(bob)}
I [Tweety2] = I 3 .
The main technical lemma we need is as follows. For its proof, which is by
transfinite induction, it will be convenient to put I [n,m] = I n for all m ∈ N
whenever n is a limit ordinal; thus, statement (b) in the lemma makes sense
for all ordinals n.
6.3.4 Lemma Let P be a normal logic program which is locally stratified
with respect to the level mapping l : B P → γ, where γ > 1. Then the following
statements hold.
(a) The sequence (I n ) n∈γ is monotonic increasing in n.
(b) For every n ∈ γ, where n ≥ 1, the sequence (I [n,m] ) is monotonic increasing
in m.
(c) For every n ∈ γ, where n ≥ 1, I n is a fixed point of T [n] .
(d) If l(B) < n and B ∈ I n , where B ∈ B P , then for every m ∈ γ with n < m
we have B ∈ I m and, hence, B ∈ I [P ] . In particular, if l(B) < n and
B ∈ I [n+1,m] for some m ∈ N, then B ∈ I n and, hence, B ∈ I [P ] .
Proof: It is immediate from the construction that the sequence (I n ) n∈γ is
monotonic increasing in n, and this establishes (a).
The main work is in proving (b) and (c), which we treat simultaneously. To
do this, we need to note the technical fact that, for each n ∈ γ, we can partition
P [n+1] as P [n] ∪ P (n), where P (n) denotes the subset of ground(P ) consisting
of those clauses whose head has level n. Thus, T [n+1] (I) = T [n] (I) ∪ T P (n) (I)
for any I ∈ I P ; note that if A ∈ T P (n) (I), then l(A) = n.
Let P(n) be the proposition, depending on the ordinal n, that (I [n,m] )
is monotonic increasing in m and that I n is a fixed point of T [n] . Suppose
that P(n) holds for all n < α, where α ≤ γ is some ordinal. We must show
that P(α) holds. Indeed, P(1) holds since P [1] is a definite program and the
construction of I 1 is simply the classical construction of the least fixed point
of T [1] . Therefore, we may assume that α > 2. It will be convenient to break
up the details of the case when α is a successor ordinal into the four steps (1)
to (4) below.
Case i. α = k + 1 is a successor ordinal. Thus, P(k) holds.
Mathematical Aspects of Logic Programming Semantics
following.
I 1 = {penguin(tweety)}
I 2 = I 1 ∪ {bird(bob), bird(tweety)}
I 3 = I 2 ∪ {flies(bob)}
I [Tweety2] = I 3 .
The main technical lemma we need is as follows. For its proof, which is by
transfinite induction, it will be convenient to put I [n,m] = I n for all m ∈ N
whenever n is a limit ordinal; thus, statement (b) in the lemma makes sense
for all ordinals n.
6.3.4 Lemma Let P be a normal logic program which is locally stratified
with respect to the level mapping l : B P → γ, where γ > 1. Then the following
statements hold.
(a) The sequence (I n ) n∈γ is monotonic increasing in n.
(b) For every n ∈ γ, where n ≥ 1, the sequence (I [n,m] ) is monotonic increasing
in m.
(c) For every n ∈ γ, where n ≥ 1, I n is a fixed point of T [n] .
(d) If l(B) < n and B ∈ I n , where B ∈ B P , then for every m ∈ γ with n < m
we have B ∈ I m and, hence, B ∈ I [P ] . In particular, if l(B) < n and
B ∈ I [n+1,m] for some m ∈ N, then B ∈ I n and, hence, B ∈ I [P ] .
Proof: It is immediate from the construction that the sequence (I n ) n∈γ is
monotonic increasing in n, and this establishes (a).
The main work is in proving (b) and (c), which we treat simultaneously. To
do this, we need to note the technical fact that, for each n ∈ γ, we can partition
P [n+1] as P [n] ∪ P (n), where P (n) denotes the subset of ground(P ) consisting
of those clauses whose head has level n. Thus, T [n+1] (I) = T [n] (I) ∪ T P (n) (I)
for any I ∈ I P ; note that if A ∈ T P (n) (I), then l(A) = n.
Let P(n) be the proposition, depending on the ordinal n, that (I [n,m] )
is monotonic increasing in m and that I n is a fixed point of T [n] . Suppose
that P(n) holds for all n < α, where α ≤ γ is some ordinal. We must show
that P(α) holds. Indeed, P(1) holds since P [1] is a definite program and the
construction of I 1 is simply the classical construction of the least fixed point
of T [1] . Therefore, we may assume that α > 2. It will be convenient to break
up the details of the case when α is a successor ordinal into the four steps (1)
to (4) below.
Case i. α = k + 1 is a successor ordinal. Thus, P(k) holds.