71
Topology and Logic Programming
(1) Suppose that s i = s for all i ∈ I is a constant net, and let a ∈
approx(s). Thus, a is a compact element satisfying a [ s. Therefore, we have
a [ s i for all i. So, ((s i ), s) ∈ C.
(2) Suppose that ((s i ), s) ∈ C and that (t j ) j∈J is a subnet of (s i ) i∈I . Thus,
there is a function φ : J → I such that (i) t j = s φ(j) for all j ∈ J , and (ii)
for each i 0 ∈ I, there is j 0 ∈ J such that i 0 ≤ φ(j) whenever j 0 ≤ j. Let
a ∈ approx(s) be arbitrary. Then because ((s i ), s) ∈ C, there is an i 0 ∈ I such
that a [ s i whenever i 0 ≤ i. Since t j is a subnet of s i , there is j 0 ∈ J such
that i 0 ≤ φ(j) whenever j 0 ≤ j. But then we have a [ s φ(j) whenever j 0 ≤ j,
that is, a [ t j whenever j 0 ≤ j. Therefore, ((t j ), s) ∈ C.
(3) Suppose that ((s i ), s) ∈ C. Then there exists a ∈ approx(s) such that
for each index i 0 there is an index j 0 ≥ i 0 with a [ s j0 . Let J denote the
collection of all these j 0 . Then clearly J is cofinal in I, and hence (t j ) j
is
∈J
a subnet of (s i ), where t j = s j for each j ∈ J . It is clear that if (r k ) is any
subnet of (t j ), then we have ((r k ), s) ∈ C.
(4) Suppose that the conditions stated in (4) of Definition 3.1.2 all hold
and that lim m lim n x(m, n) ≡ s (C), where x : F
' → D. Let a ∈ approx(s)
be arbitrary. Because lim m lim n x(m, n) ≡ s (C), there is an index m 0 ∈ I
such that a [ lim n x(m, n) whenever m ≥ m 0 . But now we see that a ∈
approx(lim n x(m, n)). Therefore, for each fixed m ≥ m 0 , there is an index
n m ∈ J m such that a [ x(m, n) whenever n ≥ n m . Define f ∈ m I
by
∈ J m
setting f (m) = n m ∈ J m whenever m ≥ m 0 , and otherwise letting f (m) ∈ J m
be arbitrary. Suppose that (m
' , g) ≥ (m 0 , f ). Then m
'
s
≥ m 0 and g ≥ f , so that
g(m
' ) ≥ f (m
' ) = n m that
/ ,
is, g(m
' ) ≥ n m / . Thus, a [ x(m
' , g(m
' )) whenever
(m
' , g) ≥ (m 0 , f ). Hence, a [ x ◦ r(m
' , g) whenever (m
' , g) ≥ (m 0 , f ), and it
follows that (x ◦ r, s) ∈ C, as required.
Next, we verify that the topology induced on D by the convergence condition coincides with the Scott topology on D. Let O be open in the topology
associated with the convergence class C, let x ∈ O, and suppose that x [ y;
suppose further that y ∈ O, that is, suppose that y is in the closed set D \ O.
Then there is a net s i → y with s i ∈ D \ O for all i. Let a ∈ approx(x) be arbitrary. Then a ∈ approx(y) and, hence, a [ s i eventually. It follows from this
that s i → x. Therefore, by (b) of Theorem A.3.5, we see that s i is eventually
in O. This contradiction sho
is a directed set with x =
as a net, A → x. Therefore,
ws that y is, in fact, in O. Next, suppose that A
A ∈ O. Then by Proposition A.6.1 we have that,
A is eventually in O, and so A ∩ O = ∅. Hence, O
is a Scott-open set.
Conversely, suppose that O is a Scott-open set, and let x ∈ O. We show
that O is open in the topology associated with the convergence class C by
establishing that, whenever s i → x, we have s i eventually in O, and then the
result follows
from (b) of Theorem A.3.5 again. Now, approx(x) is a directed
set, and x = approx(x) ∈ O. Therefore, there is an element a ∈ approx(x)
such that a ∈ O. Since s i → x, it now follows that there is i 0 such that for
i 0 ≤ i we have a [ s i . But then, since a ∈ O and O is Scott open, we have
s i ∈ O whenever i 0 ≤ i, as required to finish the proof.
•