69
Topology and Logic Programming
3.2 The Scott Topology on Spaces of Valuations
The Scott topology is normally encountered in domain theory in the context of solving recursive domain equations and in understanding self reference.
However, it also has a role in logic programming, which we discuss in this section, and indeed, in a certain sense, it naturally underpins definite programs.
We begin with the following basic definition and refer the reader to the
Appendix, both for proofs of the results we simply state here and also for a
development of the elements of the Scott topology.
3.2.1 Definition Let (D, [) be a complete partial order. A set O ⊆ D is
called Scott open
8 if it satisfies the following two conditions: (1) O is upwards
closed in the sense that whenever x ∈ O and x [ y, we have y ∈ O, and (2)
whenever A ⊆ D is directed and A ∈ O, then A ∩ O = ∅.
In the case of a domain D, this topology has a rather simple description
in that the collection {↑ a | a ∈ D c } is a base for the Scott topology on D,
where ↑ x = {y ∈ D | x [ y} for any x ∈ D, as we see in the next proposition.
3.2.2 Proposition Let (D, [) be a domain. Then the following statements
hold.
(a) The Scott-open sets form a topology on D called the Scott topology.
(b) For each compact element a ∈ D c , the set ↑ a is a Scott-open set.
(c) The collection {↑ a | a ∈ D c } is a base for the Scott topology on D.
Proof: (a) That ∅ and D are Scott open is easy to see. If O 1 and O 2 are
Scott open, if x ∈ O 1 ∩ O 2 , and if x [ y, then it is clear that y ∈ O 1 ∩ O 2 .
Suppose that A is directed and A ∈ O 1 ∩ O 2 . Then there are a 1 , a 2 ∈ A
such that a 1 ∈ O 1 and a 2 ∈ O 2 . Therefore, by directedness of A, there is
a 3 ∈ A such that a 1
[ a 3 and a 2 [ a 3 . But then a 3 ∈ O 1 ∩ O 2 , and hence
a 3 ∈ A ∩ (O 1 ∩ O 2 ), as required
to see that O 1 ∩ O 2 is Scott open. Finally, it is
easy to check that a union i O i of Scott-open sets O , i ∈ I, is itself Scott
∈I
i
open.
(b) If x ∈ ↑ a and x
[ y, then it is immediate that y ∈ ↑ a. Now suppose
that A is directed and A ∈ ↑ a. Then a is compact and a [ A. Therefore,
there is a
' ∈ A such that a [ a
' . Hence, a
' ∈ ↑ a by definition
of ↑ a, that is,
a
' ∈ A ∩ ↑ a showing that A ∩ ↑ a = ∅, as required.
(c) First we show that this collection is a base for some topology on D.
Let x ∈ D be arbitrary. Then approx(x) is directed and is non-empty; let a ∈
approx(x). Then, a ∈ D c and a [ x, so that x ∈ ↑ a, and hence
8 See [Abramsky and Jung, 1994, Gierz et al., 2003, Stoltenberg-Hansen
a∈D ↑ a = D.
et al., 1994].
Précédent

- 100/305

Suivant