110
Mathematical Aspects of Logic Programming Semantics
4.6.10 Proposition With the notation established above, (I P , d r ) is a totally
bounded quasi-ultrametric space.
Proof: Choose ε = 2
−n , where n ∈ N, and let E be the set of all subsets
of B P , the atoms of which are all of level less than or equal to n. Then E is
finite by our assumption on l. For every I ∈ I P , let e be the restriction of I to
atoms of level less than or equal to n. Then d
∗ (e, I) < ε, as is easily verified.
r
•
We have the following characterization of Cauchy sequences in I P .
4.6.11 Proposition A sequence (I n ) in (I P , d r ) is a Cauchy sequence if and
only if for every n ∈ N there exists k n ∈ N such that for all l, m ≥ k n we have
that I l and I m agree on all atoms of level less than n.
Proof: Let (I n ) be a Cauchy sequence in I P . Choose n ∈ N, and let ε = 2
−n .
Since I P is totally bounded, there exists k n ∈ N such that for all l, m ≥ k n ,
d
∗ (I l , I m ) ≤ 2
−n . By definition of d r , we obtain that I l and I m agree on all
r
atoms of level less than n. The converse follows since the argument above
clearly reverses.
•
4.6.12 Corollary Let (I n ) be a sequence in (I P , d r ). Then (I n ) is a Cauchy
sequence if and only if (I n ) converges in Q to some I. Moreover, lim I n = I,
so (I P , d r ) is complete.
Proof: By Proposition 3.3.5 and the previous proposition, (I n ) is a Cauchy
sequence if and only if (I n ) converges in Q to some I. It is easily verified that
lim I n = I by noting that I = {A ∈ B P | A ∈ I n eventually}. It follows that
(I P , d r ) is complete.
•
The previous result allows us to characterize CS-continuity in terms of Q.
4.6.13 Proposition Suppose that l : B P → N is a level mapping such that
l
−1 (n) is finite for all n. Then the immediate consequence operator T P is
CS-continuous if and only if it is continuous in Q.
Proof: Suppose that T P is CS-continuous and that (I n ) is an arbitrary sequence in I P which converges in Q to some I ∈ I P . Then (I n ) is a Cauchy
sequence, and by Corollary 4.6.12, lim I n = I. By CS-continuity of T P , we have
lim T P (I n ) = T P (I), and again by Corollary 4.6.12, we have T P (I n ) → T P (I)
in Q, as required.
Conversely, suppose T P is continuous in Q and that (I n ) is a Cauchy
sequence with lim I n = I, say. By Corollary 4.6.12, I n → I in Q, and, by
continuity of T P in Q, we get T P (I n ) → T P (I), which yields lim T P (I n ) =
T P (I), again by Corollary 4.6.12.
•
Our next observation shows that non-expansiveness implies CS-continuity.
Mathematical Aspects of Logic Programming Semantics
4.6.10 Proposition With the notation established above, (I P , d r ) is a totally
bounded quasi-ultrametric space.
Proof: Choose ε = 2
−n , where n ∈ N, and let E be the set of all subsets
of B P , the atoms of which are all of level less than or equal to n. Then E is
finite by our assumption on l. For every I ∈ I P , let e be the restriction of I to
atoms of level less than or equal to n. Then d
∗ (e, I) < ε, as is easily verified.
r
•
We have the following characterization of Cauchy sequences in I P .
4.6.11 Proposition A sequence (I n ) in (I P , d r ) is a Cauchy sequence if and
only if for every n ∈ N there exists k n ∈ N such that for all l, m ≥ k n we have
that I l and I m agree on all atoms of level less than n.
Proof: Let (I n ) be a Cauchy sequence in I P . Choose n ∈ N, and let ε = 2
−n .
Since I P is totally bounded, there exists k n ∈ N such that for all l, m ≥ k n ,
d
∗ (I l , I m ) ≤ 2
−n . By definition of d r , we obtain that I l and I m agree on all
r
atoms of level less than n. The converse follows since the argument above
clearly reverses.
•
4.6.12 Corollary Let (I n ) be a sequence in (I P , d r ). Then (I n ) is a Cauchy
sequence if and only if (I n ) converges in Q to some I. Moreover, lim I n = I,
so (I P , d r ) is complete.
Proof: By Proposition 3.3.5 and the previous proposition, (I n ) is a Cauchy
sequence if and only if (I n ) converges in Q to some I. It is easily verified that
lim I n = I by noting that I = {A ∈ B P | A ∈ I n eventually}. It follows that
(I P , d r ) is complete.
•
The previous result allows us to characterize CS-continuity in terms of Q.
4.6.13 Proposition Suppose that l : B P → N is a level mapping such that
l
−1 (n) is finite for all n. Then the immediate consequence operator T P is
CS-continuous if and only if it is continuous in Q.
Proof: Suppose that T P is CS-continuous and that (I n ) is an arbitrary sequence in I P which converges in Q to some I ∈ I P . Then (I n ) is a Cauchy
sequence, and by Corollary 4.6.12, lim I n = I. By CS-continuity of T P , we have
lim T P (I n ) = T P (I), and again by Corollary 4.6.12, we have T P (I n ) → T P (I)
in Q, as required.
Conversely, suppose T P is continuous in Q and that (I n ) is a Cauchy
sequence with lim I n = I, say. By Corollary 4.6.12, I n → I in Q, and, by
continuity of T P in Q, we get T P (I n ) → T P (I), which yields lim T P (I n ) =
T P (I), again by Corollary 4.6.12.
•
Our next observation shows that non-expansiveness implies CS-continuity.