108
Mathematical Aspects of Logic Programming Semantics
in the discrete quasimetric simply because it is not eventually increasing.
Thus, it appears not to be possible to directly characterize the property of
being forward Cauchy relative to the discrete quasimetric in terms of convergence in the Scott topology. This contrasts with the situation where the
(forward) Cauchy sequences relative to the quasimetric determined by a level
mapping, see Definition 4.6.9, can be described in terms of convergence in Q,
see Proposition 4.6.8 and Corollary 4.6.12.
•
Using the observations made thus far, it is straightforward to recover the
usual fixed-point semantics of definite logic programs, namely, to recover Theorem 2.2.3 Part (b) in terms of quasimetrics, by employing Theorem 4.6.3 Part
(a) and the discrete quasimetric on (I P , ⊆). We briefly sketch this next and
refer the reader to [Seda, 1997] for full details.
4.6.6 Example Let P denote an arbitrary definite logic program, and let d
denote the discrete quasimetric defined on the partially ordered set (I P,2 , ⊆).
Then it is shown in [Seda, 1997] that (I P,2 , d) is a CS-complete quasimetric
space and that T P is CS-continuous. We show here that, in fact, T P is nonexpansive and hence that Theorem 4.6.3 is applicable.
Suppose first that d(I 1 , I 2 ) = 0. Then I 1 ⊆ I 2 so that T P (I 1 ) ⊆ T P (I 2 ),
and hence d(T P (I 1 ), T P (I 2 )) = 0, as required. Next suppose that d(I 1 , I 2 )
takes value 1. Then immediately d(I 1 , I 2 ) ≥ d(T P (I 1 ), T P (I 2 )), as required.
Thus, T P is indeed non-expansive relative to d. We note that, in contrast, T P
is not usually a contraction relative to any metric or quasimetric, since fixed
points of T P are not usually unique. In any event, we are now in a position to
apply Theorem 4.6.3 since we have the following facts.
(1) (I P , d) is a CS-complete quasimetric space.
(2) T P : I P,2 → I P,2 is non-expansive and CS-continuous.
(3) The empty set ∅ is a point in I P,2 such that d(∅, T P (∅)) = 0.
Thus, on applying Theorem 4.6.3 and examining its proof, we conclude that
T P has a fixed
point equal to the greatest limit gl(T
n
P (∅)), and this, in turn,
is equal to T
n
P (∅) = T P ↑ ω, as shown in Chapter 3. Thus, we recover the
classical least fixed point of T P , as required.
We will now use quasimetrics to characterize continuity in the Cantor
topology of the immediate consequence operator for normal logic programs.
20
4.6.7 Definition Let (D, [) be a domain, and let r : D c → N be a function,
20 For more details of the results presented in this section, see [Seda, 1997].
Mathematical Aspects of Logic Programming Semantics
in the discrete quasimetric simply because it is not eventually increasing.
Thus, it appears not to be possible to directly characterize the property of
being forward Cauchy relative to the discrete quasimetric in terms of convergence in the Scott topology. This contrasts with the situation where the
(forward) Cauchy sequences relative to the quasimetric determined by a level
mapping, see Definition 4.6.9, can be described in terms of convergence in Q,
see Proposition 4.6.8 and Corollary 4.6.12.
•
Using the observations made thus far, it is straightforward to recover the
usual fixed-point semantics of definite logic programs, namely, to recover Theorem 2.2.3 Part (b) in terms of quasimetrics, by employing Theorem 4.6.3 Part
(a) and the discrete quasimetric on (I P , ⊆). We briefly sketch this next and
refer the reader to [Seda, 1997] for full details.
4.6.6 Example Let P denote an arbitrary definite logic program, and let d
denote the discrete quasimetric defined on the partially ordered set (I P,2 , ⊆).
Then it is shown in [Seda, 1997] that (I P,2 , d) is a CS-complete quasimetric
space and that T P is CS-continuous. We show here that, in fact, T P is nonexpansive and hence that Theorem 4.6.3 is applicable.
Suppose first that d(I 1 , I 2 ) = 0. Then I 1 ⊆ I 2 so that T P (I 1 ) ⊆ T P (I 2 ),
and hence d(T P (I 1 ), T P (I 2 )) = 0, as required. Next suppose that d(I 1 , I 2 )
takes value 1. Then immediately d(I 1 , I 2 ) ≥ d(T P (I 1 ), T P (I 2 )), as required.
Thus, T P is indeed non-expansive relative to d. We note that, in contrast, T P
is not usually a contraction relative to any metric or quasimetric, since fixed
points of T P are not usually unique. In any event, we are now in a position to
apply Theorem 4.6.3 since we have the following facts.
(1) (I P , d) is a CS-complete quasimetric space.
(2) T P : I P,2 → I P,2 is non-expansive and CS-continuous.
(3) The empty set ∅ is a point in I P,2 such that d(∅, T P (∅)) = 0.
Thus, on applying Theorem 4.6.3 and examining its proof, we conclude that
T P has a fixed
point equal to the greatest limit gl(T
n
P (∅)), and this, in turn,
is equal to T
n
P (∅) = T P ↑ ω, as shown in Chapter 3. Thus, we recover the
classical least fixed point of T P , as required.
We will now use quasimetrics to characterize continuity in the Cantor
topology of the immediate consequence operator for normal logic programs.
20
4.6.7 Definition Let (D, [) be a domain, and let r : D c → N be a function,
20 For more details of the results presented in this section, see [Seda, 1997].