56
Mathematical Aspects of Logic Programming Semantics
2.6 Well-Founded Models
If we compare Definitions 2.4.8 and 2.5.8 and keep in mind that the main
idea underlying stratification is to restrict recursion through negation, one
may be led to ask whether Definition 2.5.8 is the most natural way to achieve
this in a three-valued setting. Indeed, one may be led to propose the following
definition.
2.6.1 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
(WF) with respect to I and l if each A ∈ dom(l) satisfies one of the following
conditions.
(WFi) 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.
(WFii) ¬A ∈ I, and for each clause A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in
ground(P ) one (at least) of the following conditions holds.
(WFiia) There exists i with ¬A i ∈ I and l(A) ≥ l(A i ).
(WFiib) There exists j with B j ∈ I and l(A) > l(B j ).
If A ∈ dom(l) satisfies (WFi), then we say that A satisfies (WFi) with respect
to I and l, and similarly if A ∈ dom(l) satisfies (WFii).
We note that conditions (Fi), (WSi), and (WFi) are identical, and, furthermore, if P satisfies (WS) with respect to I and l, then it satisfies (WF)
with respect to I and l. However, replacing (WFi) by a “stratified version”
such as the following is not satisfactory.
(SFi) A ∈ I, and there is a clause A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in
ground(P ) such that A i , ¬B j ∈ I, l(A) ≥ l(A i ), and l(A) > l(B j )
for all i and j.
Indeed, if we do replace condition (WFi) by condition (SFi), then it is not
guaranteed that, for a given program, there is a greatest model satisfying the
desired properties. Consider the program consisting of the two clauses p ← p
and q ← ¬p, the two (total) models {p, ¬q} and {¬p, q}, and the level mapping
l with l(p) = 0 and l(q) = 1. These models are incomparable, yet in both cases
the conditions obtained by replacing (WFi) by (SFi) in (WF) are satisfied.
So, in the light of Theorem 2.4.9, Definition 2.6.1 should provide a natural
stratified version of the Fitting semantics, and indeed it does, see Program
2.6.12 for an instructive example. Furthermore, the resulting semantics coincides with another well-known semantics, called the well-founded semantics,
which is a very satisfactory result. To establish this claim, we need to introduce
well-founded models, and this we do next.
Mathematical Aspects of Logic Programming Semantics
2.6 Well-Founded Models
If we compare Definitions 2.4.8 and 2.5.8 and keep in mind that the main
idea underlying stratification is to restrict recursion through negation, one
may be led to ask whether Definition 2.5.8 is the most natural way to achieve
this in a three-valued setting. Indeed, one may be led to propose the following
definition.
2.6.1 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
(WF) with respect to I and l if each A ∈ dom(l) satisfies one of the following
conditions.
(WFi) 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.
(WFii) ¬A ∈ I, and for each clause A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in
ground(P ) one (at least) of the following conditions holds.
(WFiia) There exists i with ¬A i ∈ I and l(A) ≥ l(A i ).
(WFiib) There exists j with B j ∈ I and l(A) > l(B j ).
If A ∈ dom(l) satisfies (WFi), then we say that A satisfies (WFi) with respect
to I and l, and similarly if A ∈ dom(l) satisfies (WFii).
We note that conditions (Fi), (WSi), and (WFi) are identical, and, furthermore, if P satisfies (WS) with respect to I and l, then it satisfies (WF)
with respect to I and l. However, replacing (WFi) by a “stratified version”
such as the following is not satisfactory.
(SFi) A ∈ I, and there is a clause A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in
ground(P ) such that A i , ¬B j ∈ I, l(A) ≥ l(A i ), and l(A) > l(B j )
for all i and j.
Indeed, if we do replace condition (WFi) by condition (SFi), then it is not
guaranteed that, for a given program, there is a greatest model satisfying the
desired properties. Consider the program consisting of the two clauses p ← p
and q ← ¬p, the two (total) models {p, ¬q} and {¬p, q}, and the level mapping
l with l(p) = 0 and l(q) = 1. These models are incomparable, yet in both cases
the conditions obtained by replacing (WFi) by (SFi) in (WF) are satisfied.
So, in the light of Theorem 2.4.9, Definition 2.6.1 should provide a natural
stratified version of the Fitting semantics, and indeed it does, see Program
2.6.12 for an instructive example. Furthermore, the resulting semantics coincides with another well-known semantics, called the well-founded semantics,
which is a very satisfactory result. To establish this claim, we need to introduce
well-founded models, and this we do next.