58
Mathematical Aspects of Logic Programming Semantics
2.6.5 Program Let P be the following program.
p(0) ←
p(s(X)) ← p(X)
q(s(X)) ← ¬p(X)
r ← ¬q(s(X))
Then W P ↑ n = {p(s
k (0)) | k < n} ∪ {¬q(s
k (0)) | 0 < k < n}, and
W P ↑ ω = {p(s
n (0)) | n ∈ N} ∪ {¬q(s
n (0)) | n ∈ N, n > 0}
= {p(s
n (0)) | n ∈ N} ∪ {¬q(s
n (0)) | n ∈ N, n > 0} ∪ {¬r}
= W P ↑ (ω + 1).
2.6.6 Theorem Let P be a program. Then W P ↑ α ∈ I P,3 for all ordinals α.
In particular, the well-founded model for P is in I P,3 .
Proof: We first need some notation. Let M denote the least fixed point of
W P , and for each atom A ∈ M
+ let l(A) be the least ordinal β such that
A ∈ W P ↑ (β + 1).
Now assume that there is an ordinal γ which is least under the condition
that W P ↑ γ ∈ I P,3 . Then γ must be a successor ordinal, since I P,3 is a
complete partial order; so let I = W P ↑ (γ − 1) ∈ I P,3 . Now consider the set
'
U = T (I) ∩ U P (I). Then for each A ∈ U and each clause A ← body in
P
ground(P ) such that body is true in I, we have that some (non-negated) atom
'
B in body occurs in U P (I). We obtain B ∈ U P (I) ∩ I, and since I ⊆ T (I)
P
we get B ∈ U . Now let A ∈ U be chosen such that it is minimal with respect
to l(A) = β, and notice that necessarily β < γ. Then there exists a clause
A ← body in ground(P ) with body true in W P ↑ β ⊆ I, and in particular
B ∈ I and l(B) < l(A) for all (non-negated) atoms B which occur in body.
But now we have just shown that B ∈ U , contradicting minimality of l(A). •
2.6.7 Proposition Let P be a program, and let I ∈ I P,3 . Then Φ P (I) ⊆
W P (I). Furthermore, the three-valued fixed points of W P are three-valued
supported models for P with respect to Kleene’s strong three-valued logic.
Proof: Let A ∈ F P (I). Then for each clause A ← body in ground(P ), we have
that I(body) = f , and so there is a literal L ∈ body with I(L) = f . But then
A is in the greatest unfounded set of P with respect to I, and so A ∈ U P (I).
This shows that Φ P (I) ⊆ W P (I).
'
Now let M = W P (M ) = T (M ) ∪ ¬U P (M ). We show that M = Φ P (M ) =
P
'
T (M ) ∪ ¬F P (M ). For this it suffices to show that U P (M ) ⊆ F P (M ). Let
P
A ∈ U P (M ), and let A ← body be an arbitrary clause in ground(P ) with
head A. Noting that U P (M ) is an unfounded set of P with respect to M , if
condition (US1) in the definition of an unfounded set holds, then body is false
Mathematical Aspects of Logic Programming Semantics
2.6.5 Program Let P be the following program.
p(0) ←
p(s(X)) ← p(X)
q(s(X)) ← ¬p(X)
r ← ¬q(s(X))
Then W P ↑ n = {p(s
k (0)) | k < n} ∪ {¬q(s
k (0)) | 0 < k < n}, and
W P ↑ ω = {p(s
n (0)) | n ∈ N} ∪ {¬q(s
n (0)) | n ∈ N, n > 0}
= {p(s
n (0)) | n ∈ N} ∪ {¬q(s
n (0)) | n ∈ N, n > 0} ∪ {¬r}
= W P ↑ (ω + 1).
2.6.6 Theorem Let P be a program. Then W P ↑ α ∈ I P,3 for all ordinals α.
In particular, the well-founded model for P is in I P,3 .
Proof: We first need some notation. Let M denote the least fixed point of
W P , and for each atom A ∈ M
+ let l(A) be the least ordinal β such that
A ∈ W P ↑ (β + 1).
Now assume that there is an ordinal γ which is least under the condition
that W P ↑ γ ∈ I P,3 . Then γ must be a successor ordinal, since I P,3 is a
complete partial order; so let I = W P ↑ (γ − 1) ∈ I P,3 . Now consider the set
'
U = T (I) ∩ U P (I). Then for each A ∈ U and each clause A ← body in
P
ground(P ) such that body is true in I, we have that some (non-negated) atom
'
B in body occurs in U P (I). We obtain B ∈ U P (I) ∩ I, and since I ⊆ T (I)
P
we get B ∈ U . Now let A ∈ U be chosen such that it is minimal with respect
to l(A) = β, and notice that necessarily β < γ. Then there exists a clause
A ← body in ground(P ) with body true in W P ↑ β ⊆ I, and in particular
B ∈ I and l(B) < l(A) for all (non-negated) atoms B which occur in body.
But now we have just shown that B ∈ U , contradicting minimality of l(A). •
2.6.7 Proposition Let P be a program, and let I ∈ I P,3 . Then Φ P (I) ⊆
W P (I). Furthermore, the three-valued fixed points of W P are three-valued
supported models for P with respect to Kleene’s strong three-valued logic.
Proof: Let A ∈ F P (I). Then for each clause A ← body in ground(P ), we have
that I(body) = f , and so there is a literal L ∈ body with I(L) = f . But then
A is in the greatest unfounded set of P with respect to I, and so A ∈ U P (I).
This shows that Φ P (I) ⊆ W P (I).
'
Now let M = W P (M ) = T (M ) ∪ ¬U P (M ). We show that M = Φ P (M ) =
P
'
T (M ) ∪ ¬F P (M ). For this it suffices to show that U P (M ) ⊆ F P (M ). Let
P
A ∈ U P (M ), and let A ← body be an arbitrary clause in ground(P ) with
head A. Noting that U P (M ) is an unfounded set of P with respect to M , if
condition (US1) in the definition of an unfounded set holds, then body is false