40
Mathematical Aspects of Logic Programming Semantics
continuous, indeed not even ω-continuous, relative to [ k , and so Kleene’s
theorem, Theorem 1.1.9, is not generally applicable to Φ P .
2.4.6 Proposition Let P be a program. Then every fixed point M of Φ P is a
model for P with the following properties. (a) If A ∈ B P is such that M (A) =
t, then there exists a clause A ← body in ground(P ) with M (body) = t.
(b) If A ∈ B P is such that for all clauses A ← body in ground(P ) we have
M (body) = f , then M (A) = f .
Proof: Let A ← body be a clause in ground(P ). If M (body) = t, then M (A) =
Φ P (M )(A) = M (body) = t. If M (A) = f , then Φ P (M )(A) = M (A) = f , and
hence M (body) = f . Finally, if M (A) = u, then Φ P (M )(A) = M (A) = u,
and therefore M (body) = f or M (body) = u. By definition of the truth value
given to ←, we see that this suffices to show that M is a model for P .
In order to show (a), let A ∈ B P , and suppose that M (A) = t. Then
Φ P (M )(A) = M (A) = t, and there is a clause A ← body in ground(P ) with
M (body) = t by definition of Φ P .
To show (b), let A ∈ B P , and assume that for all clauses A ← body in
ground(P ) we have M (body) = f . Then M (A) = Φ P (M )(A) = f , again by
definition of Φ P .
•
Proposition 2.4.6 shows that fixed points of Φ P are three-valued supported
models for P , meaning that they satisfy (a) and (b) of Proposition 2.4.6. Note
that a total three-valued supported model is a supported model in the sense
of Definition 2.2.5.
2.4.7 Proposition Let P be a program. Then the fixed points of Φ P are
exactly the three-valued supported models for P .
Proof: Certainly, every fixed point of Φ P is a three-valued supported model
for P by Proposition 2.4.6. Conversely, let M be a three-valued supported
model for P , and let A ∈ B P . If M (A) = t, then, by definition of a three-valued
supported model, there exists a clause A ← body in ground(P ) such that
M (body) = t, and hence Φ P (M )(A) = M (body) = t = M (A). If M (A) = f ,
then for all clauses A ← body in ground(P ) we have that M (body) = f , since
M is a model for P . Hence, Φ P (M )(A) = M (body) = f = M (A). It follows
that M is a fixed point of Φ P , as required.
•
Before discussing further properties of the Fitting model, we give an alternative characterization of it.
For a program P and a three-valued interpretation I ∈ I P,3 , an I-partial
level mapping for P is a partial mapping l : B P → α with domain dom(l) =
{A | A ∈ I or ¬A ∈ I}, where α is some ordinal. Again, we extend every such
mapping to literals by setting l(¬A) = l(A) for all A ∈ dom(l).
Mathematical Aspects of Logic Programming Semantics
continuous, indeed not even ω-continuous, relative to [ k , and so Kleene’s
theorem, Theorem 1.1.9, is not generally applicable to Φ P .
2.4.6 Proposition Let P be a program. Then every fixed point M of Φ P is a
model for P with the following properties. (a) If A ∈ B P is such that M (A) =
t, then there exists a clause A ← body in ground(P ) with M (body) = t.
(b) If A ∈ B P is such that for all clauses A ← body in ground(P ) we have
M (body) = f , then M (A) = f .
Proof: Let A ← body be a clause in ground(P ). If M (body) = t, then M (A) =
Φ P (M )(A) = M (body) = t. If M (A) = f , then Φ P (M )(A) = M (A) = f , and
hence M (body) = f . Finally, if M (A) = u, then Φ P (M )(A) = M (A) = u,
and therefore M (body) = f or M (body) = u. By definition of the truth value
given to ←, we see that this suffices to show that M is a model for P .
In order to show (a), let A ∈ B P , and suppose that M (A) = t. Then
Φ P (M )(A) = M (A) = t, and there is a clause A ← body in ground(P ) with
M (body) = t by definition of Φ P .
To show (b), let A ∈ B P , and assume that for all clauses A ← body in
ground(P ) we have M (body) = f . Then M (A) = Φ P (M )(A) = f , again by
definition of Φ P .
•
Proposition 2.4.6 shows that fixed points of Φ P are three-valued supported
models for P , meaning that they satisfy (a) and (b) of Proposition 2.4.6. Note
that a total three-valued supported model is a supported model in the sense
of Definition 2.2.5.
2.4.7 Proposition Let P be a program. Then the fixed points of Φ P are
exactly the three-valued supported models for P .
Proof: Certainly, every fixed point of Φ P is a three-valued supported model
for P by Proposition 2.4.6. Conversely, let M be a three-valued supported
model for P , and let A ∈ B P . If M (A) = t, then, by definition of a three-valued
supported model, there exists a clause A ← body in ground(P ) such that
M (body) = t, and hence Φ P (M )(A) = M (body) = t = M (A). If M (A) = f ,
then for all clauses A ← body in ground(P ) we have that M (body) = f , since
M is a model for P . Hence, Φ P (M )(A) = M (body) = f = M (A). It follows
that M is a fixed point of Φ P , as required.
•
Before discussing further properties of the Fitting model, we give an alternative characterization of it.
For a program P and a three-valued interpretation I ∈ I P,3 , an I-partial
level mapping for P is a partial mapping l : B P → α with domain dom(l) =
{A | A ∈ I or ¬A ∈ I}, where α is some ordinal. Again, we extend every such
mapping to literals by setting l(¬A) = l(A) for all A ∈ dom(l).