75
Topology and Logic Programming
It is not difficult to see that the converse of the previous result fails. For
example, the program P 1 with clauses p(a) ← p(a), p(a) ← ¬p(a), and p(b) ←
p(a) and the program P 2 with clauses p(a) ← and p(b) ← p(a) have the same
(Scott continuous) immediate consequence operator.
By contrast, recall that Program 2.4.12 showed that the Fitting operator
is not order continuous, and hence not Scott continuous, for definite programs. Nevertheless, Theorem 3.2.9 justifies our earlier statement that the
Scott topology naturally underpins definite programs.
A theme which is important in this chapter and in later ones concerns the
convergence to some interpretation I of sequences T
n (M ) of iterates of T P
P
on an interpretation M , and under what conditions I is a model for P . We
discuss this briefly now for definite programs and take it up in more detail in
the next section for normal programs.
In general, if (v i ) is a net converging to v in the Scott topology on I(X, T ),
then it is clear from Theorem 3.2.4, see also Example 3.2.7, that (v i ) converges
to u whenever u [ v and, hence, that the set of limits of (v i ) is downwards
closed.
11 Indeed, since (v i ) always converges to ⊥, this latter set is always
non-empty also. Furthermore, when T denotes the complete lattice T W O, we
have by Theorem 1.3.4 that I(X, T ) is itself a complete lattice. Thus, in this
case, the supremum of the set of all limits, in the Scott topology, of a net (v i )
exists and is easily seen to be a limit of (v i ) also, by Theorem 3.2.6. We refer
to this limit as the greatest limit of (v i ) and denote it by gl(v i ). In fact, it
is readily checked that gl(v i ) takes value t precisely on the set of all x ∈ X
at which eventually v i takes value t, and this property completely determines
gl(v i ), see [Seda, 1995] for more details.
Of course, a sequence T
n (M ) always converges to the empty interpretation
P
∅, as already noted, but the interpretation ∅ need not be a model for P .
However, we do have the following result.
3.2.10 Proposition Let P be a definite logic program, and let M be an interpretation for P . Then the greatest limit gl(T
n (M )) of the sequence (T
n (M ))
P
P
is a model for P .
Proof: Let I denote gl(T
n (M )). Then the sequence (T
n (M )) converges to
P
P
I in the Scott topology. Hence, by the Scott continuity of T P , the sequence
(T P (T
n (M ))) converges to T P (I). Thus, (T
n (M )) converges to T P (I), and we
P
P
obtain, by definition of the greatest limit, that T P (I) ⊆ I, as required.
•
Finally, we note that if we take M to be the bottom element in I(X, T ),
then gl(T
n (M )) coincides with the least fixed point of T P and, hence, is the
P
least model for the definite logic program P , see [Seda, 1995]. Thus, the usual
two-valued semantics for definite programs can be expressed entirely in terms
of convergence in the Scott topology.
11 A subset O of a partially ordered set (D, r) is called downwards closed if, whenever
x ∈ O and y r x, we have y ∈ O.
Topology and Logic Programming
It is not difficult to see that the converse of the previous result fails. For
example, the program P 1 with clauses p(a) ← p(a), p(a) ← ¬p(a), and p(b) ←
p(a) and the program P 2 with clauses p(a) ← and p(b) ← p(a) have the same
(Scott continuous) immediate consequence operator.
By contrast, recall that Program 2.4.12 showed that the Fitting operator
is not order continuous, and hence not Scott continuous, for definite programs. Nevertheless, Theorem 3.2.9 justifies our earlier statement that the
Scott topology naturally underpins definite programs.
A theme which is important in this chapter and in later ones concerns the
convergence to some interpretation I of sequences T
n (M ) of iterates of T P
P
on an interpretation M , and under what conditions I is a model for P . We
discuss this briefly now for definite programs and take it up in more detail in
the next section for normal programs.
In general, if (v i ) is a net converging to v in the Scott topology on I(X, T ),
then it is clear from Theorem 3.2.4, see also Example 3.2.7, that (v i ) converges
to u whenever u [ v and, hence, that the set of limits of (v i ) is downwards
closed.
11 Indeed, since (v i ) always converges to ⊥, this latter set is always
non-empty also. Furthermore, when T denotes the complete lattice T W O, we
have by Theorem 1.3.4 that I(X, T ) is itself a complete lattice. Thus, in this
case, the supremum of the set of all limits, in the Scott topology, of a net (v i )
exists and is easily seen to be a limit of (v i ) also, by Theorem 3.2.6. We refer
to this limit as the greatest limit of (v i ) and denote it by gl(v i ). In fact, it
is readily checked that gl(v i ) takes value t precisely on the set of all x ∈ X
at which eventually v i takes value t, and this property completely determines
gl(v i ), see [Seda, 1995] for more details.
Of course, a sequence T
n (M ) always converges to the empty interpretation
P
∅, as already noted, but the interpretation ∅ need not be a model for P .
However, we do have the following result.
3.2.10 Proposition Let P be a definite logic program, and let M be an interpretation for P . Then the greatest limit gl(T
n (M )) of the sequence (T
n (M ))
P
P
is a model for P .
Proof: Let I denote gl(T
n (M )). Then the sequence (T
n (M )) converges to
P
P
I in the Scott topology. Hence, by the Scott continuity of T P , the sequence
(T P (T
n (M ))) converges to T P (I). Thus, (T
n (M )) converges to T P (I), and we
P
P
obtain, by definition of the greatest limit, that T P (I) ⊆ I, as required.
•
Finally, we note that if we take M to be the bottom element in I(X, T ),
then gl(T
n (M )) coincides with the least fixed point of T P and, hence, is the
P
least model for the definite logic program P , see [Seda, 1995]. Thus, the usual
two-valued semantics for definite programs can be expressed entirely in terms
of convergence in the Scott topology.
11 A subset O of a partially ordered set (D, r) is called downwards closed if, whenever
x ∈ O and y r x, we have y ∈ O.