156
Mathematical Aspects of Logic Programming Semantics
Proposition 5.2.7 allows us to apply Theorem 4.2.5 in the following way.
Let P be a normal logic program such that Φ P ↑ ω is total. Then T
n (I)
P
converges in Q to Φ P ↑ ω for every I, and Φ P ↑ ω is the unique fixed point of
T P . By Theorem 4.2.5, we can therefore find a metric with respect to which
T P is a contraction. However, this metric does not in general coincide with
the metric associated with the dislocated ultrametric � from Theorem 5.1.17,
with respect to which T P is also a contraction under the given condition on
P .
The following result is even stronger than Proposition 5.2.7.
5.2.8 Theorem Let P be a normal logic program, let j ∈ {1, 2, 3}, let k ∈
{1, 2}, and assume that M = Φ P,j,k ↑ α is total for some α. Then M
+ is
the unique two-valued supported model for P . Furthermore, the transfinite
sequence (Φ P,j,k ↑ β) β converges in the Cantor topology to M
+ .
Proof: By totality of M , Propositions 5.2.3 and 5.2.6, we obtain M
+ as a
fixed point of T P . The convergence results follow as in Proposition 5.2.7. •
We can extend the treatment of the Fitting operator from Section 2.4 to
the operators Φ P,j,k introduced in Definition 5.2.2. This will, in turn, lead
us back to the program classes from Section 5.1. We begin with the Φ P,3,2
operator in the next section.
5.2.2 Acyclic and Locally Hierarchical Programs
We first present conditions analogous to Definition 2.4.8, which was used to
characterize the Fitting semantics, beginning with condition (F 32 ) as defined
next.
5.2.9 Definition Let P be a normal logic program, let I be a model for P ,
and let l be an I-partial level mapping for P . We say that P satisfies (F 32 ) with
respect to I and l if for each A ∈ dom(l) and for all clauses A ← L 1 , . . . , L n
in ground(P ) we have L i ∈ dom(l) and l(A) > l(L i ) for all i = 1, . . . , n, and
furthermore each A ∈ dom(l) satisfies one of the following conditions.
(Fi) A ∈ I, and there is a clause A ← L 1 , . . . , L n in ground(P ) such that
L i ∈ I and l(A) > l(L i ) for all i.
(Fii) ¬A ∈ I, and for each clause A ← L 1 , . . . , L n in ground(P ) there exists
i with ¬L i ∈ I and l(A) > l(L i ).
Conditions (Fi) and (Fii) are identical to those in Definition 2.4.8. The difference between Definitions 2.4.8 and 5.2.9 lies in the additional very strong
condition “for each A ∈ dom(l) and for all clauses A ← L 1 , . . . , L n in
ground(P ) we have L i ∈ dom(l) and l(A) > l(L i ) for all i = 1, . . . , n”. The
proof of the following theorem is very similar to the proof of Theorem 2.4.9
and is therefore only sketched.
Mathematical Aspects of Logic Programming Semantics
Proposition 5.2.7 allows us to apply Theorem 4.2.5 in the following way.
Let P be a normal logic program such that Φ P ↑ ω is total. Then T
n (I)
P
converges in Q to Φ P ↑ ω for every I, and Φ P ↑ ω is the unique fixed point of
T P . By Theorem 4.2.5, we can therefore find a metric with respect to which
T P is a contraction. However, this metric does not in general coincide with
the metric associated with the dislocated ultrametric � from Theorem 5.1.17,
with respect to which T P is also a contraction under the given condition on
P .
The following result is even stronger than Proposition 5.2.7.
5.2.8 Theorem Let P be a normal logic program, let j ∈ {1, 2, 3}, let k ∈
{1, 2}, and assume that M = Φ P,j,k ↑ α is total for some α. Then M
+ is
the unique two-valued supported model for P . Furthermore, the transfinite
sequence (Φ P,j,k ↑ β) β converges in the Cantor topology to M
+ .
Proof: By totality of M , Propositions 5.2.3 and 5.2.6, we obtain M
+ as a
fixed point of T P . The convergence results follow as in Proposition 5.2.7. •
We can extend the treatment of the Fitting operator from Section 2.4 to
the operators Φ P,j,k introduced in Definition 5.2.2. This will, in turn, lead
us back to the program classes from Section 5.1. We begin with the Φ P,3,2
operator in the next section.
5.2.2 Acyclic and Locally Hierarchical Programs
We first present conditions analogous to Definition 2.4.8, which was used to
characterize the Fitting semantics, beginning with condition (F 32 ) as defined
next.
5.2.9 Definition Let P be a normal logic program, let I be a model for P ,
and let l be an I-partial level mapping for P . We say that P satisfies (F 32 ) with
respect to I and l if for each A ∈ dom(l) and for all clauses A ← L 1 , . . . , L n
in ground(P ) we have L i ∈ dom(l) and l(A) > l(L i ) for all i = 1, . . . , n, and
furthermore each A ∈ dom(l) satisfies one of the following conditions.
(Fi) A ∈ I, and there is a clause A ← L 1 , . . . , L n in ground(P ) such that
L i ∈ I and l(A) > l(L i ) for all i.
(Fii) ¬A ∈ I, and for each clause A ← L 1 , . . . , L n in ground(P ) there exists
i with ¬L i ∈ I and l(A) > l(L i ).
Conditions (Fi) and (Fii) are identical to those in Definition 2.4.8. The difference between Definitions 2.4.8 and 5.2.9 lies in the additional very strong
condition “for each A ∈ dom(l) and for all clauses A ← L 1 , . . . , L n in
ground(P ) we have L i ∈ dom(l) and l(A) > l(L i ) for all i = 1, . . . , n”. The
proof of the following theorem is very similar to the proof of Theorem 2.4.9
and is therefore only sketched.