68
Mathematical Aspects of Logic Programming Semantics
3.1.3 Theorem Let C be a convergence class in a non-empty set X. For each
A ⊆ X, let A
c = {s ∈ X | there is a net (s i ) in A with ((s i ), s) ∈ C}. Then
c
· is a closure operator on X and, hence, defines a topology τ on X, called
the topology associated with C. Moreover, we have ((s i ), s) ∈ C if and only if
s i → s with respect to τ .
Conversely, suppose that τ is a topology on a non-empty set X. Let C
denote the set of all pairs ((s i ), s), where s ∈ X and (s i ) i∈I is a net in X
which converges to s in the topology τ . Then C is a convergence class in X
whose associated topology coincides with τ .
Proof: The proof of the first part of the theorem is well-known and will be
omitted, and we refer the reader to [Kelley, 1975] or [Seda et al., 2003] for
details.
For the converse, we note that properties (1), (2), and (3) in the definition
of a convergence class are immediate for the class C by elementary properties
of nets converging in a topology (see Definition A.3.3). Property (4) of the
definition follows from the Theorem on Iterated Limits, see [Kelley, 1975, Page
69], and, hence, the class C is a convergence class. Finally, let A ⊆ X be an
arbitrary subset of X. By the definition of the closure operator determined by
C as given in the first statement in the theorem, we have s ∈ A
c if and only
if there is a net (s i ) in A converging to s. But this is equivalent to s ∈ A by
statement (a) of Theorem A.3.5, and it follows that the associated topology
of C coincides with τ .
•
Another basic definition is that of continuous function, as follows.
3.1.4 Definition Let (X, S) and (Y, T ) be convergence spaces. Then a function f : X → Y is said to be continuous at s ∈ X if (f (s i )) ∈ T f (s) whenever
(s i ) ∈ S s , that is, if f (s i ) converges to f (s) whenever s i converges to s.
There are a few points to be made about these definitions. First, suppose
that C is a convergence class on X. For each s ∈ X, let S s denote the collection
of nets (s i ) such that ((s i ), s) ∈ C. Then conditions (1) and (2) in the definition
of C show that (X, (S s ) s∈X ) is, in fact, a convergence space. Second, since a
function f : X → Y between topological spaces is continuous at s ∈ X
if and only if f (s i ) converges to f (s) whenever the net s i converges to s,
see (d) of Theorem A.3.5, we note that the notion of continuity just defined
coincides with topological continuity when the convergence spaces in question
are actually convergence classes. Finally, definitions equivalent to these can
be given entirely in terms of filters, but we omit the details.
7
It is known that the full generality of convergence spaces is needed in modelling hybrid systems, as observed earlier. Here, in fact, all the convergence
conditions we consider give rise to convergence classes and, hence, to topologies, rather than to strict convergence spaces, and therefore our focus is on
convergence classes as already noted.
7 We refer the reader to [Seda et al., 2003] for a treatment in terms of filters.
Mathematical Aspects of Logic Programming Semantics
3.1.3 Theorem Let C be a convergence class in a non-empty set X. For each
A ⊆ X, let A
c = {s ∈ X | there is a net (s i ) in A with ((s i ), s) ∈ C}. Then
c
· is a closure operator on X and, hence, defines a topology τ on X, called
the topology associated with C. Moreover, we have ((s i ), s) ∈ C if and only if
s i → s with respect to τ .
Conversely, suppose that τ is a topology on a non-empty set X. Let C
denote the set of all pairs ((s i ), s), where s ∈ X and (s i ) i∈I is a net in X
which converges to s in the topology τ . Then C is a convergence class in X
whose associated topology coincides with τ .
Proof: The proof of the first part of the theorem is well-known and will be
omitted, and we refer the reader to [Kelley, 1975] or [Seda et al., 2003] for
details.
For the converse, we note that properties (1), (2), and (3) in the definition
of a convergence class are immediate for the class C by elementary properties
of nets converging in a topology (see Definition A.3.3). Property (4) of the
definition follows from the Theorem on Iterated Limits, see [Kelley, 1975, Page
69], and, hence, the class C is a convergence class. Finally, let A ⊆ X be an
arbitrary subset of X. By the definition of the closure operator determined by
C as given in the first statement in the theorem, we have s ∈ A
c if and only
if there is a net (s i ) in A converging to s. But this is equivalent to s ∈ A by
statement (a) of Theorem A.3.5, and it follows that the associated topology
of C coincides with τ .
•
Another basic definition is that of continuous function, as follows.
3.1.4 Definition Let (X, S) and (Y, T ) be convergence spaces. Then a function f : X → Y is said to be continuous at s ∈ X if (f (s i )) ∈ T f (s) whenever
(s i ) ∈ S s , that is, if f (s i ) converges to f (s) whenever s i converges to s.
There are a few points to be made about these definitions. First, suppose
that C is a convergence class on X. For each s ∈ X, let S s denote the collection
of nets (s i ) such that ((s i ), s) ∈ C. Then conditions (1) and (2) in the definition
of C show that (X, (S s ) s∈X ) is, in fact, a convergence space. Second, since a
function f : X → Y between topological spaces is continuous at s ∈ X
if and only if f (s i ) converges to f (s) whenever the net s i converges to s,
see (d) of Theorem A.3.5, we note that the notion of continuity just defined
coincides with topological continuity when the convergence spaces in question
are actually convergence classes. Finally, definitions equivalent to these can
be given entirely in terms of filters, but we omit the details.
7
It is known that the full generality of convergence spaces is needed in modelling hybrid systems, as observed earlier. Here, in fact, all the convergence
conditions we consider give rise to convergence classes and, hence, to topologies, rather than to strict convergence spaces, and therefore our focus is on
convergence classes as already noted.
7 We refer the reader to [Seda et al., 2003] for a treatment in terms of filters.