162
Mathematical Aspects of Logic Programming Semantics
It turns out that this notion of consequence operator relates nicely to Q,
yielding the following result.
5.4.2 Theorem If T is a consequence operator for P and if for any I ∈ I P
we have that the sequence of iterates T
m (I) converges in Q to some M ∈ I P ,
then M is a model for P in the sense that every clause in ground(P ) evaluates
to t n under M . Furthermore, continuity of T yields that M is a fixed point of
T .
Proof: Suppose that A ∈ B P and that M (A) = t i , and let A ← body belong
to ground(P ), where body has the form A 1 , . . . , A m , ¬B 1 , . . . , ¬B m / . Then
eventually T (T
k (I))(A) = t i . Suppose M (A 1 ∧ . . . ∧ A m ∧ ¬B 1 ∧ . . . ∧ ¬B m / ) =
t j , say. Taking the sequence T
k (I), we have, by the property stated in the
hypothesis (applied to each literal in the conjunction under consideration),
that eventually T
k (I)(A 1 ∧ . . . ∧ A m ∧ ¬B 1 ∧ . . . ∧ ¬B m / ) = M (A 1 ∧ . . . ∧ A m ∧
¬B 1 ∧ . . . ∧ ¬B m / ) = t j . Since T (T
k (I))(A) ← T
k (I)(A 1 ∧ . . . ∧ A m ∧ ¬B 1 ∧
. . . ∧ ¬B m / ) is t n by the fact that T is a consequence operator, we obtain that
M (A ← A 1 ∧. . .∧A m ∧¬B 1 ∧. . .∧¬B m / ) = t n , as required. If T is continuous,
then M = lim T
n+1 (I) = T (lim T
n (I)) = T (M ).
•
Intuitively, consequence operators propagate “truth” along the implication
symbols occurring in the program. From this point of view, we would like the
outcome of the truth value of such a propagation to be dependent only on the
relevant clause bodies. The next definition captures this intuition.
5.4.3 Definition Let A ∈ B P , and denote by B A the set of all body atoms
of clauses with head A which occur in ground(P ). A consequence operator T
is called (P -)local if for every A ∈ B P and any two interpretations I, K ∈ I P
which agree on all atoms in B A , we have T (I)(A) = T (K)(A).
It is our desire to study continuity in Q of local consequence operators.
Since Q is a product topology, it is reasonable to expect that finiteness conditions will play a role in this context, as already observed in Section 3.3.
5.4.4 Definition Let C be a clause in P , and let A ∈ B P be such that A
coincides with the head of C. The clause C is said to be of finite type relative
to A if C has only finitely many different ground instances with head A. The
program P will be said to be of finite type relative to A if each clause in P is
of finite type relative to A, that is, if the set of all clauses in ground(P ) with
head A is finite. Finally, P will be said to be of finite type if P is of finite type
relative to A for every A ∈ B P .
A local variable is a variable which appears in a clause body, but not in
the corresponding head.
12 It is easy to see that in the context of Herbrand
12 Local variables appear naturally in implementations, but their occurrence is awkward
from the point of view of semantics, especially if they occur in negated body literals since
this leads to the so-called floundering problem, see [Lloyd, 1987, Apt and Pedreschi, 1994].
Mathematical Aspects of Logic Programming Semantics
It turns out that this notion of consequence operator relates nicely to Q,
yielding the following result.
5.4.2 Theorem If T is a consequence operator for P and if for any I ∈ I P
we have that the sequence of iterates T
m (I) converges in Q to some M ∈ I P ,
then M is a model for P in the sense that every clause in ground(P ) evaluates
to t n under M . Furthermore, continuity of T yields that M is a fixed point of
T .
Proof: Suppose that A ∈ B P and that M (A) = t i , and let A ← body belong
to ground(P ), where body has the form A 1 , . . . , A m , ¬B 1 , . . . , ¬B m / . Then
eventually T (T
k (I))(A) = t i . Suppose M (A 1 ∧ . . . ∧ A m ∧ ¬B 1 ∧ . . . ∧ ¬B m / ) =
t j , say. Taking the sequence T
k (I), we have, by the property stated in the
hypothesis (applied to each literal in the conjunction under consideration),
that eventually T
k (I)(A 1 ∧ . . . ∧ A m ∧ ¬B 1 ∧ . . . ∧ ¬B m / ) = M (A 1 ∧ . . . ∧ A m ∧
¬B 1 ∧ . . . ∧ ¬B m / ) = t j . Since T (T
k (I))(A) ← T
k (I)(A 1 ∧ . . . ∧ A m ∧ ¬B 1 ∧
. . . ∧ ¬B m / ) is t n by the fact that T is a consequence operator, we obtain that
M (A ← A 1 ∧. . .∧A m ∧¬B 1 ∧. . .∧¬B m / ) = t n , as required. If T is continuous,
then M = lim T
n+1 (I) = T (lim T
n (I)) = T (M ).
•
Intuitively, consequence operators propagate “truth” along the implication
symbols occurring in the program. From this point of view, we would like the
outcome of the truth value of such a propagation to be dependent only on the
relevant clause bodies. The next definition captures this intuition.
5.4.3 Definition Let A ∈ B P , and denote by B A the set of all body atoms
of clauses with head A which occur in ground(P ). A consequence operator T
is called (P -)local if for every A ∈ B P and any two interpretations I, K ∈ I P
which agree on all atoms in B A , we have T (I)(A) = T (K)(A).
It is our desire to study continuity in Q of local consequence operators.
Since Q is a product topology, it is reasonable to expect that finiteness conditions will play a role in this context, as already observed in Section 3.3.
5.4.4 Definition Let C be a clause in P , and let A ∈ B P be such that A
coincides with the head of C. The clause C is said to be of finite type relative
to A if C has only finitely many different ground instances with head A. The
program P will be said to be of finite type relative to A if each clause in P is
of finite type relative to A, that is, if the set of all clauses in ground(P ) with
head A is finite. Finally, P will be said to be of finite type if P is of finite type
relative to A for every A ∈ B P .
A local variable is a variable which appears in a clause body, but not in
the corresponding head.
12 It is easy to see that in the context of Herbrand
12 Local variables appear naturally in implementations, but their occurrence is awkward
from the point of view of semantics, especially if they occur in negated body literals since
this leads to the so-called floundering problem, see [Lloyd, 1987, Apt and Pedreschi, 1994].