170
Mathematical Aspects of Logic Programming Semantics
Note that the set of all quasi-interpretations is a complete partial order
with respect to set-inclusion.
'
6.1.2 Proposition Given a normal logic program P , the operator T is Scott
P
continuous on the set of all quasi-interpretations.
'
Proof: We show first that T is monotonic. So let Q ⊆ R be quasiP
'
interpretations, and let A ← body be in T (Q). If A ← body results from
P
the unfolding of some clause A ← body 0 in P with some clauses B i ← body i
in Q, then B i ← body i is contained in R for all i by assumption, and by the
'
existence of the clause A ← body 0 in P we obtain A ← body in T (R) by
P
'
unfolding. If A ← body ∈ T (Q) does not result from some unfolding, then it
P
'
'
is already contained in P and, hence, in T (R). Thus, T is monotonic.
P
P
Now let Q = {Q λ | λ ∈ Λ} be an indexed directed family of quasi-interpretations, and let Q = Q = Q. Since the order under consideration is set'
'
inclusion and T is monotonic, we immediately have that T (Q) is directed.
P
P
By the remarks following Definition 1.1.7, it therefore remains to show that
'
'
'
T (Q) ⊆ T (Q). So suppose that A ← body belongs to T (Q). If A ← body
P
P
P
does not result from an unfolding, then it is already contained in P , hence also
'
in T (Q). Otherwise, A ← body results from the unfolding of some A ← body 0
P
in P with some B i ← body i in Q. But then there is λ such that all B i ← body i
'
'
are contained in Q λ ; hence, A ← body is contained in T (Q λ ) ⊆ T (Q), as
P
P
required.
•
Given a normal logic program P , we define the fixpoint completion fix(P )
'
of P by fix(P ) = T ↑ ω.
P
6.1.3 Example Consider again the example program Tweety2, see Program
2.3.9. We obtain the following.
'
T Tweety2 ↑ 0 = ∅
'
T Tweety2 ↑ 1 = {penguin(tweety) ←, bird(bob) ←}
'
'
T Tweety2 ↑ 2 = T Tweety2 ↑ 1 ∪ {bird(tweety), flies(bob) ← ¬penguin(bob)}
'
'
T Tweety2 ↑ 3 = T Tweety2 ↑ 2 ∪ {flies(tweety) ← ¬penguin(tweety)}
'
fix(Tweety2) = T Tweety2 ↑ 3.
The importance of the fixpoint completion lies in the fact that the stable
models of a given program P are exactly the supported models of fix(P ). We
can prove an even stronger result.
3
3 The proof of Theorem 6.1.4 is taken directly from [Wendt, 2002a], which appeared in
compressed form as [Wendt, 2002b]. This correspondence can also be carried over to the
Fitting/well-founded semantics. More precisely, it was shown in [Wendt, 2002b] that for any
normal logic program P and any three-valued interpretation I, we have Ψ P (I) = Φ fix(P ) (I),
where Ψ P is the operator due to [Bonnier et al., 1991] used for characterizing three-valued
stable models, but is not treated here. A corollary of the result just mentioned is that the
well-founded model for a given program P coincides with the Fitting model for fix(P ).
Mathematical Aspects of Logic Programming Semantics
Note that the set of all quasi-interpretations is a complete partial order
with respect to set-inclusion.
'
6.1.2 Proposition Given a normal logic program P , the operator T is Scott
P
continuous on the set of all quasi-interpretations.
'
Proof: We show first that T is monotonic. So let Q ⊆ R be quasiP
'
interpretations, and let A ← body be in T (Q). If A ← body results from
P
the unfolding of some clause A ← body 0 in P with some clauses B i ← body i
in Q, then B i ← body i is contained in R for all i by assumption, and by the
'
existence of the clause A ← body 0 in P we obtain A ← body in T (R) by
P
'
unfolding. If A ← body ∈ T (Q) does not result from some unfolding, then it
P
'
'
is already contained in P and, hence, in T (R). Thus, T is monotonic.
P
P
Now let Q = {Q λ | λ ∈ Λ} be an indexed directed family of quasi-interpretations, and let Q = Q = Q. Since the order under consideration is set'
'
inclusion and T is monotonic, we immediately have that T (Q) is directed.
P
P
By the remarks following Definition 1.1.7, it therefore remains to show that
'
'
'
T (Q) ⊆ T (Q). So suppose that A ← body belongs to T (Q). If A ← body
P
P
P
does not result from an unfolding, then it is already contained in P , hence also
'
in T (Q). Otherwise, A ← body results from the unfolding of some A ← body 0
P
in P with some B i ← body i in Q. But then there is λ such that all B i ← body i
'
'
are contained in Q λ ; hence, A ← body is contained in T (Q λ ) ⊆ T (Q), as
P
P
required.
•
Given a normal logic program P , we define the fixpoint completion fix(P )
'
of P by fix(P ) = T ↑ ω.
P
6.1.3 Example Consider again the example program Tweety2, see Program
2.3.9. We obtain the following.
'
T Tweety2 ↑ 0 = ∅
'
T Tweety2 ↑ 1 = {penguin(tweety) ←, bird(bob) ←}
'
'
T Tweety2 ↑ 2 = T Tweety2 ↑ 1 ∪ {bird(tweety), flies(bob) ← ¬penguin(bob)}
'
'
T Tweety2 ↑ 3 = T Tweety2 ↑ 2 ∪ {flies(tweety) ← ¬penguin(tweety)}
'
fix(Tweety2) = T Tweety2 ↑ 3.
The importance of the fixpoint completion lies in the fact that the stable
models of a given program P are exactly the supported models of fix(P ). We
can prove an even stronger result.
3
3 The proof of Theorem 6.1.4 is taken directly from [Wendt, 2002a], which appeared in
compressed form as [Wendt, 2002b]. This correspondence can also be carried over to the
Fitting/well-founded semantics. More precisely, it was shown in [Wendt, 2002b] that for any
normal logic program P and any three-valued interpretation I, we have Ψ P (I) = Φ fix(P ) (I),
where Ψ P is the operator due to [Bonnier et al., 1991] used for characterizing three-valued
stable models, but is not treated here. A corollary of the result just mentioned is that the
well-founded model for a given program P coincides with the Fitting model for fix(P ).