30
Mathematical Aspects of Logic Programming Semantics
semantics therefore involve the imposition of certain additional conditions
which models must satisfy in order to qualify as intended models. However,
just what conditions it is reasonable to choose in this context depends on one’s
particular understanding of what “intended” could mean, and the remainder
of this chapter will be devoted, in the main, to the presentation and study of
different conditions which have been proposed in the literature to solve this
problem.
The observation that B P is too large, as a two-valued model, suggests the
selection of minimal models. Of particular interest are the cases when there
exists a least model.
2.2.3 Theorem Let P be a definite program, and let J denote a fixed preinterpretation for L P . Then the following statements hold.
(a) T P is order continuous on I P .
(b) P has a least (J-)model, which coincides with the least fixed point of T P
and is equal to T P ↑ ω.
(c) The intersection of any non-empty collection of (J-)models for P is itself a
model for P . Therefore, a definite program cannot have two distinct minimal models. Furthermore, the intersection of the collection of all models
for P coincides with the least model for P .
Proof: (a) We first show that T P is monotonic. Let I, K ∈ I P with I ⊆ K,
and suppose A ∈ T P (I). Then there is a clause A ← body in ground(P ) with
body ⊆ I. Hence, body ⊆ K, and so A ∈ T P (K), as required.
Now let I = {I λ |
λ ∈ Λ } be a directed family of two-valued interpretations, and let I = I = I. Since the order under consideration is
set-inclusion and T P is monotonic, we immediately have that T P (I) is directed. By the remarks following
Definition 1.1.7, it remains to show that
T P (I) ⊆
T P (I). So suppose that A belongs to T P (I). Then there is a
(definite) clause C of the form A ← A 1 , . . . , A n in ground(P ) satisfying
A 1 , . . . , A n ∈ I. Therefore, there exist I λ1 , . . . , I λn in I with A i ∈ I λi for
i = 1, . . . , n. Since I is directed, there is I λ ∈ I with I λi ⊆ I λ for i = 1, . . . , n.
Hence, the body of C is true in I λ , and we obtain that A ∈ T P (I λ ) and,
consequently, that A ∈
T P (I), as required.
(b) By (a), we can apply Kleene’s theorem, Theorem 1.1.9, to see that
T P has a least pre-fixed point, that this least pre-fixed point is in fact the
least fixed point of T P , and that it coincides with T P ↑ ω. Hence, by Proposition 2.2.2, T P ↑ ω is the least model for P .
(c) The details of the proof of this claim are straightforward and therefore
are omitted.
•
It can be shown, furthermore, that the least model for definite programs
corresponds rather well with the procedural behaviour of logic programming
Mathematical Aspects of Logic Programming Semantics
semantics therefore involve the imposition of certain additional conditions
which models must satisfy in order to qualify as intended models. However,
just what conditions it is reasonable to choose in this context depends on one’s
particular understanding of what “intended” could mean, and the remainder
of this chapter will be devoted, in the main, to the presentation and study of
different conditions which have been proposed in the literature to solve this
problem.
The observation that B P is too large, as a two-valued model, suggests the
selection of minimal models. Of particular interest are the cases when there
exists a least model.
2.2.3 Theorem Let P be a definite program, and let J denote a fixed preinterpretation for L P . Then the following statements hold.
(a) T P is order continuous on I P .
(b) P has a least (J-)model, which coincides with the least fixed point of T P
and is equal to T P ↑ ω.
(c) The intersection of any non-empty collection of (J-)models for P is itself a
model for P . Therefore, a definite program cannot have two distinct minimal models. Furthermore, the intersection of the collection of all models
for P coincides with the least model for P .
Proof: (a) We first show that T P is monotonic. Let I, K ∈ I P with I ⊆ K,
and suppose A ∈ T P (I). Then there is a clause A ← body in ground(P ) with
body ⊆ I. Hence, body ⊆ K, and so A ∈ T P (K), as required.
Now let I = {I λ |
λ ∈ Λ } be a directed family of two-valued interpretations, and let I = I = I. Since the order under consideration is
set-inclusion and T P is monotonic, we immediately have that T P (I) is directed. By the remarks following
Definition 1.1.7, it remains to show that
T P (I) ⊆
T P (I). So suppose that A belongs to T P (I). Then there is a
(definite) clause C of the form A ← A 1 , . . . , A n in ground(P ) satisfying
A 1 , . . . , A n ∈ I. Therefore, there exist I λ1 , . . . , I λn in I with A i ∈ I λi for
i = 1, . . . , n. Since I is directed, there is I λ ∈ I with I λi ⊆ I λ for i = 1, . . . , n.
Hence, the body of C is true in I λ , and we obtain that A ∈ T P (I λ ) and,
consequently, that A ∈
T P (I), as required.
(b) By (a), we can apply Kleene’s theorem, Theorem 1.1.9, to see that
T P has a least pre-fixed point, that this least pre-fixed point is in fact the
least fixed point of T P , and that it coincides with T P ↑ ω. Hence, by Proposition 2.2.2, T P ↑ ω is the least model for P .
(c) The details of the proof of this claim are straightforward and therefore
are omitted.
•
It can be shown, furthermore, that the least model for definite programs
corresponds rather well with the procedural behaviour of logic programming