67
Topology and Logic Programming
concerning nets, and our notation in this respect, can be found in the Appendix.
4 Indeed, all the basic facts we need concerning general topology have
been collected together in the Appendix.
We begin with some basic definitions.
3.1.1 Definition Let X be a non-empty set. We call the pair (X, S) =
(X, (S s ) s∈X ) a convergence space if, for each s ∈ X, S s is a non-empty collection of nets in X with the following properties.
(1) If (s i ) is a constant net, that is, s i = s ∈ X for all i, then (s i ) ∈ S s .
(2) If (s i ) i∈I ∈ S s and (t j ) j∈J is a subnet of (s i ), then (t j ) j∈J ∈ S s .
If (s i ) ∈ S s , we say s i converges to s and sometimes write s i → s to indicate
this.
3.1.2 Definition Let X be a non-empty set, and suppose that C is a class of
pairs ((s i ), s), where (s i ) i∈I is a net in X and s is an element of X. We call C
a convergence class if it satisfies the conditions below, in which we will write
that s i converges (C) to s or that lim i s i ≡ s (C) if and only if ((s i ), s) ∈ C.
(1) (Constant nets) If (s i ) is a net such that s i = s for all i, then ((s i ), s) ∈ C.
(2) (Convergence of subnets) If (s i ) converges (C) to s, then so does every
subnet of (s i ).
(3) (Non-convergence)
5 If (s i ) does not converge (C) to s, then there is a
subnet of (s i ), of which no subnet converges (C) to s.
(4) (Iterated limits) Suppose that I is a directed set and that J m is a directed
set for each m ∈ I. Form the fibred product F
' = I × I
m∈I J m =
{(m, n) | m ∈ I, n ∈ J
'
m }, and
s suppose that x : F → X. Let F denote
the product directed set
6 I × m I J m , and let r : F → F
' be defined
∈
by r(m, f ) = (m, f (m)). If lim m lim n x(m, n) ≡ s (C), then the net x ◦ r
converges (C) to s.
The principal result concerning convergence classes, see [Kelley, 1975,
Chapter 2] or [Seda et al., 2003], is that each convergence class C on X induces a closure operator on X which in turn induces a topology on X, in
accordance with Theorem A.2.9, in which the convergent nets and their limits
are precisely those given in C. More precisely, we have the following result
which shows that the notion of convergence may be taken as fundamental.
4 We refer the reader again to [Kelley, 1975] for more details.
5 This formulation is as given in [Kelley, 1975]. An equivalent form, given in positive
terms, is as follows: if every subnet of a net (s i ) has a subnet converging to s, then (s i )
converges to s.
6 By a product
Q directed set
Q
Im, we understand, of course, the pointwise ordering
m∈I
on the product
Im of the directed sets Im; thus, for elements f and g of
I
m
m,
∈I
m∈I
we have f ≤ g if and only if f (m) ≤ g(m) for each m ∈ I.
Q
Topology and Logic Programming
concerning nets, and our notation in this respect, can be found in the Appendix.
4 Indeed, all the basic facts we need concerning general topology have
been collected together in the Appendix.
We begin with some basic definitions.
3.1.1 Definition Let X be a non-empty set. We call the pair (X, S) =
(X, (S s ) s∈X ) a convergence space if, for each s ∈ X, S s is a non-empty collection of nets in X with the following properties.
(1) If (s i ) is a constant net, that is, s i = s ∈ X for all i, then (s i ) ∈ S s .
(2) If (s i ) i∈I ∈ S s and (t j ) j∈J is a subnet of (s i ), then (t j ) j∈J ∈ S s .
If (s i ) ∈ S s , we say s i converges to s and sometimes write s i → s to indicate
this.
3.1.2 Definition Let X be a non-empty set, and suppose that C is a class of
pairs ((s i ), s), where (s i ) i∈I is a net in X and s is an element of X. We call C
a convergence class if it satisfies the conditions below, in which we will write
that s i converges (C) to s or that lim i s i ≡ s (C) if and only if ((s i ), s) ∈ C.
(1) (Constant nets) If (s i ) is a net such that s i = s for all i, then ((s i ), s) ∈ C.
(2) (Convergence of subnets) If (s i ) converges (C) to s, then so does every
subnet of (s i ).
(3) (Non-convergence)
5 If (s i ) does not converge (C) to s, then there is a
subnet of (s i ), of which no subnet converges (C) to s.
(4) (Iterated limits) Suppose that I is a directed set and that J m is a directed
set for each m ∈ I. Form the fibred product F
' = I × I
m∈I J m =
{(m, n) | m ∈ I, n ∈ J
'
m }, and
s suppose that x : F → X. Let F denote
the product directed set
6 I × m I J m , and let r : F → F
' be defined
∈
by r(m, f ) = (m, f (m)). If lim m lim n x(m, n) ≡ s (C), then the net x ◦ r
converges (C) to s.
The principal result concerning convergence classes, see [Kelley, 1975,
Chapter 2] or [Seda et al., 2003], is that each convergence class C on X induces a closure operator on X which in turn induces a topology on X, in
accordance with Theorem A.2.9, in which the convergent nets and their limits
are precisely those given in C. More precisely, we have the following result
which shows that the notion of convergence may be taken as fundamental.
4 We refer the reader again to [Kelley, 1975] for more details.
5 This formulation is as given in [Kelley, 1975]. An equivalent form, given in positive
terms, is as follows: if every subnet of a net (s i ) has a subnet converging to s, then (s i )
converges to s.
6 By a product
Q directed set
Q
Im, we understand, of course, the pointwise ordering
m∈I
on the product
Im of the directed sets Im; thus, for elements f and g of
I
m
m,
∈I
m∈I
we have f ≤ g if and only if f (m) ≤ g(m) for each m ∈ I.
Q