174
Mathematical Aspects of Logic Programming Semantics
Proof: By Theorem 5.5.1 we obtain that T fix(P ) is measurable with respect
to σ(Q), and by Theorem 6.1.4 we know that T fix(P ) = GL P .
•
The following variant of Theorem 5.4.2 can be proven directly.
6.2.5 Theorem Let P be a normal logic program, and let GL P be continuous
and such that the sequence of iterates GL
n (I) converges in Q to some M ∈ I P .
P
Then M is a stable model for P .
Proof: By continuity we obtain M = lim GL
n (I) = GL P (lim GL
n (I)) =
P
P
GL P (M ).
•
We can also exploit our knowledge about the relationships between the
single-step operator and the Fitting operator.
6.2.6 Proposition Let P be a normal logic program, and assume that M =
Φ fix(P ) ↑ ω is total.
4 Then GL
n (∅) converges in Q to M
+ , and M
+ is the
P
unique stable model for P .
Proof: This follows immediately from Proposition 5.2.7 and Theorem 6.1.4.
•
Metric-based approaches also carry over to our present context; we restrict
our discussion to the following corollary of Theorem 5.1.6.
6.2.7 Theorem Let P be a locally stratified normal logic program with corresponding level mapping l. Then GL P is strictly contracting with respect to
d l . If the codomain of l is ω, then GL P is a contraction with respect to d l .
Furthermore, in both cases, GL P has a unique fixed point, and therefore P
has a unique stable model.
Proof: If P is locally stratified with respect to l, then fix(P ) is locally hierarchical with respect to l. It thus suffices to apply Theorem 5.1.6 in conjunction
with Theorem 6.1.4.
•
6.2.8 Remark With the comments already made concerning the fact that
the well-founded model for a given program P coincides with the Fitting
model for fix(P ), for any normal program P , we can also derive the following
result.
4 We mentioned earlier in this chapter that Φ fix(P ) coincides with the operator Ψ P from
[Bonnier et al., 1991] for characterizing three-valued stable models.
Mathematical Aspects of Logic Programming Semantics
Proof: By Theorem 5.5.1 we obtain that T fix(P ) is measurable with respect
to σ(Q), and by Theorem 6.1.4 we know that T fix(P ) = GL P .
•
The following variant of Theorem 5.4.2 can be proven directly.
6.2.5 Theorem Let P be a normal logic program, and let GL P be continuous
and such that the sequence of iterates GL
n (I) converges in Q to some M ∈ I P .
P
Then M is a stable model for P .
Proof: By continuity we obtain M = lim GL
n (I) = GL P (lim GL
n (I)) =
P
P
GL P (M ).
•
We can also exploit our knowledge about the relationships between the
single-step operator and the Fitting operator.
6.2.6 Proposition Let P be a normal logic program, and assume that M =
Φ fix(P ) ↑ ω is total.
4 Then GL
n (∅) converges in Q to M
+ , and M
+ is the
P
unique stable model for P .
Proof: This follows immediately from Proposition 5.2.7 and Theorem 6.1.4.
•
Metric-based approaches also carry over to our present context; we restrict
our discussion to the following corollary of Theorem 5.1.6.
6.2.7 Theorem Let P be a locally stratified normal logic program with corresponding level mapping l. Then GL P is strictly contracting with respect to
d l . If the codomain of l is ω, then GL P is a contraction with respect to d l .
Furthermore, in both cases, GL P has a unique fixed point, and therefore P
has a unique stable model.
Proof: If P is locally stratified with respect to l, then fix(P ) is locally hierarchical with respect to l. It thus suffices to apply Theorem 5.1.6 in conjunction
with Theorem 6.1.4.
•
6.2.8 Remark With the comments already made concerning the fact that
the well-founded model for a given program P coincides with the Fitting
model for fix(P ), for any normal program P , we can also derive the following
result.
4 We mentioned earlier in this chapter that Φ fix(P ) coincides with the operator Ψ P from
[Bonnier et al., 1991] for characterizing three-valued stable models.