62
Mathematical Aspects of Logic Programming Semantics
Since ∅ ⊆ B P , we obtain L 0 ⊆ L 1 ⊆ G 1 ⊆ G 0 , and, by transfinite induction, it can easily be shown that L α ⊆ L β ⊆ G β ⊆ G α whenever α ≤ β.
2.6.13 Theorem Let P be a program. Then the following hold.
(a) L P = GL P (G P ) and G P = GL P (L P ).
(b) For every stable model S for P , we have L P ⊆ S ⊆ G P .
(c) M = L P ∪ ¬(B P \ G P ) is the well-founded model for P .
Proof: (a) We obtain GL
2 (GL P (L P )) = GL P (GL
2
P
P (L P )) = GL P (L P ), so
GL P (L
2
P ) is a fixed point of GL P , and hence L P ⊆ GL P (L P ) ⊆ G P . Similarly,
L P ⊆ GL P (G P ) ⊆ G P . Since L P ⊆ G P , we get from the antitonicity of GL P
that L P ⊆ GL P (G P ) ⊆ GL P (L P ) ⊆ G P . Similarly, since GL P (L P ) G P , we
obtain GL
2
⊆
P (G P ) ⊆ GL P (L P ) = L P ⊆ GL P (G P ), so GL P (G P ) = L P , and
hence G P = GL
2
P (G P ) = GL P (L P ).
(b) It suffices to note that S is a fixed point of GL P , by Theorem 2.3.7,
and, hence, is a fixed point of GL
2
P .
(c) We prove this statement by applying Theorem 2.6.8. First, we define
an M -partial level mapping l. For convenience, we will take as image set of l,
pairs (α, n) of ordinals, where n ≤ ω, with the lexicographic ordering. This can
be done without loss of generality because any set of pairs of ordinals, lexicographically ordered, is certainly well-ordered and therefore order-isomorphic
to an ordinal, as noted earlier. For A ∈ L P , let l(A) be the pair (α, n), where
α is the least ordinal such that A ∈ L α+1 , and n is the least ordinal such that
A ∈ T P/Gα ↑ (n + 1). For B ∈ G P , let l(B) be the pair (β, ω), where β is the
least ordinal such that B ∈ G β+1 . We show next by transfinite induction that
P satisfies (WF) with respect to M and l.
Let A ∈ L 1 = T P/B P ↑ ω. Since P/B P consists of exactly all clauses from
ground(P ) which contain no negation, we have that A is contained in the least
two-valued model for a definite subprogram of P , namely, P/B P , and (WFi)
is satisfied, by Proposition 2.3.2. Now let ¬B ∈ ¬(B P \ G P ) be such that
B ∈ (B P \ G 1 ) = B P \ T P/ ↑ ω. Since P/∅ contains all clauses from ground(P )
∅
with all negative literals removed, we obtain that each clause in ground(P )
with head B must contain a positive body literal C ∈ G 1 , which, by definition
of l, must have the same level as B; hence, (WFiia) is satisfied.
Assume now that, for some ordinal α, we have shown that A satisfies (WF)
with respect to M and l for all n ≤ ω and all A ∈ B P with l(A) ≤ (α, n).
Let A ∈ L α+1 \ L α = T P/Gα ↑ ω \ L α . Then A ∈ T P/Gα ↑ n \ L α for some
n ∈ N; note that all (negative) literals which were removed by the Gelfond–
Lifschitz transformation from clauses with head A have level less than (α, 0).
Then the assertion that A satisfies (WF) with respect to M and l follows
again by Proposition 2.3.2.
Let A ∈ (B P \ G α+1 ) ∩ G α . Then we have A ∈ T P/Lα ↑ ω. Let A ←
A 1 , . . . , A k , ¬B 1 , . . . , ¬B m be a clause in ground(P ). If B j ∈ L α for some j,
Mathematical Aspects of Logic Programming Semantics
Since ∅ ⊆ B P , we obtain L 0 ⊆ L 1 ⊆ G 1 ⊆ G 0 , and, by transfinite induction, it can easily be shown that L α ⊆ L β ⊆ G β ⊆ G α whenever α ≤ β.
2.6.13 Theorem Let P be a program. Then the following hold.
(a) L P = GL P (G P ) and G P = GL P (L P ).
(b) For every stable model S for P , we have L P ⊆ S ⊆ G P .
(c) M = L P ∪ ¬(B P \ G P ) is the well-founded model for P .
Proof: (a) We obtain GL
2 (GL P (L P )) = GL P (GL
2
P
P (L P )) = GL P (L P ), so
GL P (L
2
P ) is a fixed point of GL P , and hence L P ⊆ GL P (L P ) ⊆ G P . Similarly,
L P ⊆ GL P (G P ) ⊆ G P . Since L P ⊆ G P , we get from the antitonicity of GL P
that L P ⊆ GL P (G P ) ⊆ GL P (L P ) ⊆ G P . Similarly, since GL P (L P ) G P , we
obtain GL
2
⊆
P (G P ) ⊆ GL P (L P ) = L P ⊆ GL P (G P ), so GL P (G P ) = L P , and
hence G P = GL
2
P (G P ) = GL P (L P ).
(b) It suffices to note that S is a fixed point of GL P , by Theorem 2.3.7,
and, hence, is a fixed point of GL
2
P .
(c) We prove this statement by applying Theorem 2.6.8. First, we define
an M -partial level mapping l. For convenience, we will take as image set of l,
pairs (α, n) of ordinals, where n ≤ ω, with the lexicographic ordering. This can
be done without loss of generality because any set of pairs of ordinals, lexicographically ordered, is certainly well-ordered and therefore order-isomorphic
to an ordinal, as noted earlier. For A ∈ L P , let l(A) be the pair (α, n), where
α is the least ordinal such that A ∈ L α+1 , and n is the least ordinal such that
A ∈ T P/Gα ↑ (n + 1). For B ∈ G P , let l(B) be the pair (β, ω), where β is the
least ordinal such that B ∈ G β+1 . We show next by transfinite induction that
P satisfies (WF) with respect to M and l.
Let A ∈ L 1 = T P/B P ↑ ω. Since P/B P consists of exactly all clauses from
ground(P ) which contain no negation, we have that A is contained in the least
two-valued model for a definite subprogram of P , namely, P/B P , and (WFi)
is satisfied, by Proposition 2.3.2. Now let ¬B ∈ ¬(B P \ G P ) be such that
B ∈ (B P \ G 1 ) = B P \ T P/ ↑ ω. Since P/∅ contains all clauses from ground(P )
∅
with all negative literals removed, we obtain that each clause in ground(P )
with head B must contain a positive body literal C ∈ G 1 , which, by definition
of l, must have the same level as B; hence, (WFiia) is satisfied.
Assume now that, for some ordinal α, we have shown that A satisfies (WF)
with respect to M and l for all n ≤ ω and all A ∈ B P with l(A) ≤ (α, n).
Let A ∈ L α+1 \ L α = T P/Gα ↑ ω \ L α . Then A ∈ T P/Gα ↑ n \ L α for some
n ∈ N; note that all (negative) literals which were removed by the Gelfond–
Lifschitz transformation from clauses with head A have level less than (α, 0).
Then the assertion that A satisfies (WF) with respect to M and l follows
again by Proposition 2.3.2.
Let A ∈ (B P \ G α+1 ) ∩ G α . Then we have A ∈ T P/Lα ↑ ω. Let A ←
A 1 , . . . , A k , ¬B 1 , . . . , ¬B m be a clause in ground(P ). If B j ∈ L α for some j,