On the computational content of the Lawson topology

Frédéric De Jaeger

DI, Ecole Normale Supérieure, Paris

Martín Escardó

School of Computer Science, St Andrews University

Gabriele Santini

DI, Ecole Normale Supérieure, Paris

1st July 2000, revised 19th July 2005

Abstract

An element of an effectively given domain is computable iff its basic Scott open neighbourhoods are recursively enumerable. We thus refer to computable elements as Scott computable and define an element to be Lawson computable if its basic Lawson open neighbourhoods are recursively enumerable. Since the Lawson topology is finer than the Scott topology, a stronger notion of computability is obtained. For example, in the powerset of the natural numbers with its standard effective presentation, an element is Scott computable iff it is a recursively enumerable set, and it is Lawson computable iff it is a recursive set. Among other examples, we consider the upper powerdomain of Euclidean space, for which we prove that Scott and Lawson computability coincide with two notions of computability for compact sets recently proposed by Brattka and Weihrauch in the framework of type-two recursion theory.

1 Introduction

The Lawson topology has its origins in topological algebra [8, 7]. A Lawson semilattice is a locally compact Hausdorff topological semilattice for which each point has a neighbourhood base of subsemilattices. Before continuous lattices and domains were introduced by Dana Scott, it was known that the topology of a Lawson semilattice is uniquely determined by its lattice structure. It was an amazing discovery that the underlying lattices of the compact Lawson semilattices are precisely the bounded complete continuous dcpos [8, 7]. Thus, the Lawson topology of a bounded complete continuous dcpo arises as the unique compact Hausdorff topology that makes the binary meet operation jointly continuous.

Given this, it may come as a surprise that the Lawson topology happens to have manifestations in the theory of computation. The first application to semantics of which we are aware is Plotkin’s characterization of the so-called “2/3 SFP” property of a domain as compactness with respect to the Lawson topology [1, 3]. Other applications occur in the theory of function spaces over semantic domains [11] and in the theory of computational models of classical topological spaces [12].

Smyth has observed that the Scott topology can be regarded as a topology of positive information, and that the Lawson topology can be regarded as a topology of positive-and-negative information [18]. In this paper we make explicit the computational content of Smyth’s observation.

It is easy to see that an element of an effectively given domain is computable iff its basic Scott open neighbourhoods are recursively enumerable. This is elaborated in the technical development that follows. We thus refer to computable elements as Scott computable and define an element to be Lawson computable if its basic Lawson open neighbourhoods are recursively enumerable. Since the Lawson topology is finer than the Scott topology, a stronger notion of computability is obtained. As the Lawson topology is the join of the Scott and the dual topologies, it is natural to also consider an induced notion of dual computability.

For example, in the powerset of the natural numbers with its standard effective presentation, an element is Scott computable iff it is a recursively enumerable set, it is dual computable iff its complement is a recursively enumerable set, and it is Lawson computable iff it is a recursive set.

Among other examples, we consider the upper powerdomain of Euclidean space. Brattka and Weihrauch have recently shown that a considerable number of possible effectivizations of the notion of compactness for subsets of Euclidean space reduce, up to equivalence, to three [4]. We show that they correspond to Scott, dual and Lawson computability in the upper powerdomain.

A point-free approach to the Lawson topology of a domain, and more generally to the patch topology of a stably locally compact space, has been developed in [5, 6]. The constructions and results are intuitionistic in the sense of topos logic. We leave it to further work to relate that approach to the classical pointset approach based on recursion theory that is developed in this paper. In particular, we plan to investigate a notion of effectively given stably locally compact space (and locale), with associated notions of computability, dual computability and patch computability for points and maps.

Stably locally compact spaces are of interest in this context because their theory reduces to that of continuous lattices, via a Stone-type duality, and because they constitute a general framework that includes continuous Scott domains (under their Scott, dual and Lawson topologies) and classical spaces such as locally compact Hausdorff spaces at the same time. Moreover, they are closed under the formation of various useful constructions such as upper and Vietoris hyperspaces and probabilistic powerdomain [10, 9, 14, 2].

2 Computability in effective domain theory

We consider three notions of computability for elements of effectively given domains, which are induced by effectivizations of the Scott, dual and Lawson topologies.

2.1 Effectively given topological spaces

Good introductions of topology for the theory of computation are Mislove [13], Smyth [18], and Vickers [19]. In Weihrauch’s recent work, a theory of effectively given topological spaces is developed as an intermediate tool for studying computability notions induced by naming systems—see e.g. [20] and [21].

Definition 2.1 (Weihrauch [21]) An effectively given topological space is a topological space together with an enumeration of a base of the topology. Such an enumeration is called a notation.

In Weihrauch’s original definition, effectively given spaces are assumed to be T_{0}. Having in mind that points are indentified with their (indices of basic) neighbourhoods, this is a reasonable assumption. However, it is superfluous in the mathematical development that follows. Also, in Weihrauch’s original definition, one has an enumeration of a subbase rather than of a base of the topology, but, since it is possible to effectively obtain an enumeration of a base from an enumeration of a subbase, our definition is equivalent.

Definition 2.2 The name of a point of an effectively given space is the set of indices of its basic open neighbourhoods. A point of an effectively given space is computable if its name is a recursively enumerable set.

Of course, this notion of computability heavily depends on the notation that effectively presents the space. For example, if U_{n} is an enumeration of a base and ψ is a non-recursive permutation of the natural numbers, then V_{n} = U_{ψ(n)} is another enumeration, which induces a completely different notion of computability.

2.2 Continuous domain and the way-below relation

We assume some familiarity with continuous domain theory [1, 3, 8, 7]. Recall that a dcpo is a poset with joins of directed sets. For a dcpo D and elements x and y of D one defines x ≪ y, and says that x is way below y, if for every directed set S with y ⊑ ⨆ S, already x ⊑ s for some s ∈ S. The dcpo D is said to be continuous if for every x ∈ D, the set

↓ ↓x =^{def} {b ∈ D | b ≪ x}

is directed and has x as its join. A continuous domain is a continuous dcpo. A basis of a continuous domain D is a set B such that for every x in D, the set ↓ ↓x ∩ B is directed and has x as its join.

2.3 Effectively given domains

For the purposes of this paper, an effectively given domain is a continuous domain together with an enumeration of a basis, subject to the condition that the way-below relation on basis elements is semidecidable with respect to the indexing. For the theory of effectively given domains and its applications, some technical conditions on the enumeration have to be added, particularly if one is interested in closure under the formation of function spaces [17]. But such conditions play no technical rôle in this work and hence they can be safely omitted. An element of an effectively given domain is computable if the basis elements way below it are recursively enumerable. Notice that by the assumption that the way-below relation is semidecidable, all basis elements are computable. With a natural definition of a notion of computability for Scott continuous maps, this assumption is equivalent to the identity function being computable.

2.4 Scott computability

Recall that the Scott topology of a domain has as opens the upper sets U such that whenever ⨆ S ∈ U for a directed set S, already s ∈ S for some s ∈ S. A base for the Scott topology of a continuous domain D is given by the sets

↑ ↑b =^{def} {x ∈ D | b ≪ x},

for b ∈ B, where B is any basis of the domain. Thus, an effective presentation b_{n} of a domain D induces an effective presentation ↑ ↑b_{n} of the Scott topology of D.

Definition 2.3 An element of an effectively given domain is Scott computable if it is computable via the induced effective presentation of the Scott topology.

Since b_{n} ≪ x is equivalent to x ∈ ↑ ↑b_{n}, it is clear that an element of an effectively given domain is computable in the sense of the previous subsection iff it is Scott computable in the sense of the above definition.

2.5 Dual computability

The dual topology of a continuous domain D is generated by the closed subbase consisting of the sets of the form

↑ x =^{def} {y ∈ D | x ⊑ y}

for x an element of the domain. Equivalently, one can take as a closed subbase the compact saturated sets in the Scott topology. Here compactness is taken in the topological sense: any open cover by Scott open sets has a finite subcover. Recall that a set is saturated if and only if it is an upper set, if and only if it is the intersection of its neighbourhoods in the Scott topology.

Lemma 2.4 If B is a basis of a continuous domain D, then the sets ↑ b, for b ∈ B, form a closed subbase of the dual topology of D.

Proof Let y be a member of the subbasic open set D \ ↑ x. This means that x ⋢ y. By continuity of D and the fact that B is a basis, there is b ∈ B with b ≪ x such that already b ⋢ y, and it is clear that y ∈ D \ ↑ b ⊆ D \ ↑ x. □

Thus, an effective presentation b_{n} of D induces an effective presentation D \ ↑ b_{n} of an open subbase of the dual topology of D, which in turns induces an effective presentation of an open base.

Definition 2.5 An element of an effectively given domain is dual computable if it is computable via the induced effective presentation of the dual topology.

2.6 Lawson computability

The Lawson topology of a domain is the join of the Scott topology and the dual topology. A base for this topology is given by the sets of the form ↑ ↑b\↑ F where b is a basis element, F is a finite set of basis elements, and ↑ F = ⋃_{x∈F} ↑ x. Thus, an effective presentation of a domain induces an effective presentation of the Lawson topology via a standard coding of finite sets of natural numbers.

Definition 2.6 An element of an effectively given domain is Lawson computable if it is computable via the induced effectivization of the Lawson topology.

2.7 Order-theoretic characterizations

In summary, the notions of Scott, dual and Lawson computability are characterized in order-theoretical terms as follows.

Proposition 2.7 For any element x of a continuous domain with effective basis B,

1. x is Scott computable iff the condition b ≪ x is semidecidable in b ∈ B.

2. x is dual computable iff the condition b ≰ x is semidecidable in b ∈ B.

3. x is Lawson computable iff both conditions are semidecidable.

3 Basic examples

In this section we characterize the notions of Scott, dual and Lawson computability in some basic examples of domains that arise in applications of domain theory to semantics, recursion theory and effective analysis. As all the conclusions require only a basic knowledge of domain theory and recursion theory, we only state them, leaving the details of the proofs to the reader. A more elaborate example is the topic of Section 5 below.

3.1 The powerset of the natural numbers

The powerset 𝒫ω of the natural numbers ordered by inclusion with a standard enumeration Δ_{n} of the basis of finite subsets is an effectively given algebraic domain, which is investigated in detail by Scott [16]. In this domain, X ≪ Y iff X is a finite subset of Y.

1. An element of 𝒫ω is Scott computable iff it is recursively enumerable.

2. An element of 𝒫ω is dual computable iff it is co-r.e.

3. It follows that an element of 𝒫ω is Lawson computable iff it is recursive.

3.2 The partial functions

The domain of partial endofunctions on the natural numbers ordered by graph inclusion is another algebraic domain, with an effective presentation given by a standard enumeration of the functions with finite graph.

1. A partial function is Scott-computable iff its graph is r.e., which means that it is partial recursive.

2. A partial function is dual-computable iff its graph is co-r.e.

3. A partial function is Lawson-computable iff it has a recursive graph.

3.3 The extended real line

The domain [−∞, ∞] of extended reals under their natural order is a first example of a continuous, non-algebraic domain. Its way-below relation is characterized by x ≪ y iff x < y or x = −∞. A countable basis is given by a standard enumeration of the rationals enlarged by −∞. A base for the Scott topology is given by the open sets of the form ↑ ↑r = (r, ∞] with r rational. Thus, the Scott topology is the topology of lower semicontinuity. A real number is Scott computable iff it is lower semicomputable, or left computable in Weihrauch’s terminology, which means that one can semidecide if a rational is strictly smaller than the real. A base for the dual topology is given by the open sets of the form [−∞, ∞] \ ↑ r = [−∞, ∞] \ [r, ∞] = [−∞, r) with r rational. Thus, the dual topology is the topology of upper semicontinuity. Hence a real is dual computable iff it is upper semicomputable or right computable. The Lawson topology, being the join of the Scott and the dual topology, is the Euclidean topology. A real is Lawson computable iff it is computable in the classical sense of effective analysis, which means that it is both lower and upper semicomputable. Thus, these are effectivizations of the notions of right, left and double Dedekind sections: a real is Scott computable iff its left Dedekind section is r.e., it is dual computable if its right Dedekind section is r.e., and it is Lawson computable if both sections are r.e.

3.4 The partial real line

Our last example in this section is the domain of non-empty compact intervals of the extended Euclidean real line ordered by reverse inclusion. We regard intervals as partial real numbers, and singletons as total real numbers. Partial (and total) reals numbers are ranged over by the letters x, y, z and are regarded as generalized real numbers, and one writes x = [\underline{x}, \overline{x}]. The following facts are well known.

1. Partial real numbers form a domain with joins of directed sets given by intersections.

2. x ≪ y iff the interior of x in the Euclidean topology contains y.

3. Partial real numbers form a continuous domain with the intervals with rationals endpoints as a basis.

An effective presentation is given by a standard enumeration of the rational basis. The following facts are routine consequences of the definitions.

1. A partial number x is Scott computable iff \underline{x} is lower semicomputable and \overline{x} is upper semicomputable.

2. A partial number x is dual computable iff \underline{x} is upper semicomputable and \overline{x} lower semicomputable.

3. A partial number x is Lawson computable iff both \underline{x} and \overline{x} are computable.

In particular, for total real numbers, we have that Scott, dual, and Lawson computability coincide. This is an effectivization of the fact that the relative Scott, dual and Lawson topologies on total real numbers coincide with the Euclidean topology.

4 Effective reducibility

In our main example, which is the subject of the next section, we discuss notions of computability for compact subsets of Euclidean space. As a preparation, in this section we develop some tools for effective reducibility of effective presentations of topologies.

So far, we have deliberately avoided introducing formal notation. At this point, for easy comparison with Weihrauch’s work, it is convenient to adopt his notation, which we introduce as we proceed. We begin by recalling the definition of an effectively given topological space and introducing its associated formal notation.

Definition 4.1 An effective topological space is a triple 𝔗 = (M, τ, ν) where M is a set, τ is a topology on M and ν is an enumeration of a base of τ. Such an enumeration ν is called a notation. The 𝔗-name of a point x ∈ M, denoted by ℕ_{𝔗}(x), is the set of indices n such that x ∈ ν_{n}. A point of M is 𝔗-computable if its 𝔗-name is recursively enumerable.

Our approach is formally different from Weihrauch’s, because he uses Turing machines that operate on infinite words over a finite alphabet Σ, while we use partial recursive operators. The main resulting difference is that Weihrauch’s representations are surjective partial maps from Σ^{ω} to M, while our 𝔗-names are total maps from M to 𝒫ω. For the formal definition and theory of partial recursive operators, see Rogers [15]. One can think of a partial recursive operator, which is formally defined to be an endofunction of 𝒫ω subject to some effectivity conditions, as an algorithm that reads integers sequentially from an input list and that, from time to time, adds an integer to the output list.

Definition 4.2 Let 𝔗 = (M, τ, ν) and 𝔗′ = (M, τ′, ν′) be two effective topological spaces with the same underlying set M. We say that 𝔗 is effectively reducible to 𝔗′ if there exists a partial recursive operator Φ_{τ→τ′} : 𝒫ω → 𝒫ω such that

ℕ_{𝔗′} = Φ_{τ→τ′} ∘ ℕ_{𝔗}.  \xymatrix{ & 𝒫ω \ar@{.>}[dd]^{Φ_{τ→τ′}} \\ M \ar[ur]^{ℕ_{𝔗}} \ar[dr]_{ℕ_{𝔗′}} \\  & 𝒫ω}

When there is no ambiguity regarding the involved topologies, we denote the operator simply by Φ.

Proposition 4.3 Let 𝔗 = (M, τ, ν) and 𝔗′ = (M, τ′, ν′) be two effective topological structures on the same set M. If 𝔗 is effectively reducible to 𝔗′, then τ is finer than τ′.

Proof Let U be a τ′-open set and x be a point of U. By hypothesis, there exists an index m such that x ∈ ν′(m) ⊆ U. Because Φ is computable, it is Scott continuous. The continuity condition expressed at ℕ_{𝔗}(x) tells us that Φ^{−1}(↑ ↑{m}) is a Scott open subset of 𝒫ω containing ℕ_{𝔗}(x). Thus, there exists a finite subset F of ℕ_{𝔗}(x) such that Φ(↑ ↑F) ⊆ ↑ ↑{m}, which means that Φ(F) ∋ m. Hence V =^{def} ∩_{i∈F} ν(i), being a finite intersection of τ-opens, is a τ-open set. Now, for all y ∈ V, we have that ℕ_{𝔗}(y) ⊇ F. By monotonicity of Φ, we conclude that ℕ_{τ′}(y) = Φ(ℕ_{τ} (y)) ⊇ Φ(F) ∋ m. This implies that y ∈ ν′(m). Therefore x ∈ V ⊆ ν′(m) ⊆ U, which shows that U is τ-open. □

For the converse, an additional hypothesis is needed.

Lemma 4.4 Let 𝔗 = (M, τ, ν) and 𝔗′ = (M, τ′, ν′) be two effective topological spaces on the same set M. If τ is finer than τ′ and the predicate ν(n) ⊆ ν′(m) is r.e. in n and m then 𝔗 is effectively reducible to 𝔗′.

Proof We define Φ as an algorithm. We suppose we are parsing a sequence n_{i} that enumerates the set {n | x ∈ ν(n)}. Each time we read an n_{i}, we fork a process that prints a list of the set {m | ν(n_{i}) ⊆ ν′(m)}. The set we obtain is clearly a subset of {m | x ∈ ν′(m)}. And because τ is finer than τ′, the inclusion in the other direction also holds. □

This lemma is our main tool in proofs of effective equivalence of topologies.

Corollary 4.5 If 𝔗 is effectively reducible to 𝔗′, then every 𝔗-computable point x ∈ M is 𝔗′-computable.

Proof The image of an r.e. subset of ℕ by a recursive operator is again an r.e. subset of ℕ — see e.g. [15]. □

Definition 4.6 Let 𝔗 and 𝔗′ be two effective topological spaces on the same set, we say that 𝔗 and 𝔗′ are effectively equivalent iff they are effectively reducible to each other.

In this case, it is clear that they induce the same computable points.

5 Main example

We now come to our last example, the domain of compact subsets of the Euclidean space ℝ^{N} for some finite dimension N. This example is more complex than the previous and we thus study it in detail. It is a generalization of the last example of Section 3. The main difference is that the ambient space is not compact anymore. This lack of compactness changes some results concerning dual computability.

5.1 The upper powerdomain of Euclidean space

Let 𝒦 be the set of non-empty compact subsets of ℝ^{N}, and endow ℝ^{N} with any classical norm such as L_{1}, L_{2} or L_{∞}. In fact, we only need a norm such that Lemma 5.4 below holds. That is, we must be able to decide natural latticetheoretic questions about the basic elements. We denote by B(x, r) the open ball with center x and radius r with respect to this norm. We extend this notation to a subset A of ℝ^{N} by B(A, r) = ⋃_{x∈A} B(x, r). Let B_{n} be a standard enumeration of the open balls with rational center and radius, where a point of ℝ^{N} is called rational if its coordinates are rational. Similarly, let K_{n} be a standard enumeration of the finite unions of closed rational balls. Notice that the sets K_{n}, being bounded, are compact.

Notation 5.1 The interior of a subset A of a topological space is denoted by Å or (A)^{∘}, and its complement by A^{c}. The lattice of open sets of a topological space X is denoted by O X.

Proposition 5.2 The following predicates are decidable in m and n:

1. K_{n} ⊆ K_{m},

2. K_{n} ⊆ K̊_{m},

3. K_{n} ∩ K_{m} = ∅,

4. K̊_{n} ∩ K̊_{m} = ∅,

5. K̊_{n} ∩ K_{m} = ∅.

Proof These conditions can be checked by a finite number of comparisons between rational numbers. □

As usual, we order the upper powerdomain 𝒦 by reverse inclusion:

K ⊑ L ⟺ K ⊇ L,

which is clearly a directed complete partial order.

Proposition 5.3 For K, L ∈ 𝒦, the condition K ≪ L is equivalent to L ⊆ K̊.

Proof See e.g. [8]. □

Lemma 5.4 For every K ∈ 𝒦 and every ϵ > 0 there is n with

K ⊆ K̊_{n} ⊆ B(K, ϵ).

Proof Given K ∈ 𝒦, and ϵ > 0, let K_{ϵ} =^{def} B(K, ϵ). Then

K ⊆ K_{ϵ} = ⋃_{B_{n}⊆K_{ϵ}} B_{n},

and we can thus extract a finite subcover such that K ⊆ ⋃_{i=1}^{p} B_{n_{i}}. Since there is n with K_{n} = ⋃_{i=1}^{p} B̄_{n_{i}}, we conclude that K ⊆ ⋃_{i=1}^{p} B_{n_{i}} ⊆ K̊_{n} ⊆ K_{ϵ}. □

Proposition 5.5 The set 𝒦 of compact subsets of ℝ^{N} ordered by reverse inclusion is a continuous domain with the compact sets of the form K_{n} as a basis.

Proof The fact that 𝒦 is continuous comes from the fact that ℝ^{N} is a locally compact Hausdorff space. We only have to prove that the K_{n} form a basis of this domain. Given indices n and m such that K_{n} ≪ K and K_{m} ≪ K, we have that K ⊆ K̊_{n} ∩ K̊_{m} = (K_{n} ∩ K_{m})^{∘}. This implies that K ∩ ((K_{n} ∩ K_{m})^{∘})^{c} = ∅. And because K is compact and the other set is closed, the distance δ between them is strictly positive. By Lemma 5.4, we can choose an index p with K ⊆ K̊_{p} ⊆ K_{δ} ⊆ K_{n} ∩ K_{m}. Then we have that K_{n} ∨ K_{m} ⊑ K_{p} ≪ K, which shows that the set of K_{n} that are way-below K is directed. Its join is K because K = ⋂_{ϵ>0} B(K, ϵ). □

We assume that ℝ^{N} is endowed with the Euclidean topology, which coincides with the topology induced by the norm, denoted by 𝒪ℝ^{N}.

Definition 5.6 For U ∈ 𝒪ℝ^{N}, we define 1. □U = {K ∈ 𝒦 | K ⊆ U},

2. ♢U = {K ∈ 𝒦 | K ∩ U ≠ ∅}. Proposition 5.7

1. □ and ♢ are injective monotone maps from 𝒪ℝ^{N} to 𝒫(𝒦),

2. □U ∩ □V = □(U ∩ V),

3. □U ∪ □V ⊆ □(U ∪ V),

4. ♢U ∩ ♢V ⊇ ♢(U ∩ V),

5. ♢U ∪ ♢V = ♢(U ∪ V).

5.2 The upper topology

The Scott topology on 𝒦 is generated by open sets of the form ↑ ↑K_{n} = □K̊_{n} for K ∈ 𝒦. Thus, Scott computability coincides with 𝔗-computability for the effective topological space 𝔗_{S} = (𝒦, τ_{S}, ν_{S}) where ν_{S}(n) = ↑ ↑K_{n}.

Following Weihrauch [21], we effectively present the upper topology, denoted by τ_{>}, on 𝒦 by considering an enumerated subbase defined by

U_{>,⟨n,r⟩} =^{def} □B(0, r) ∩ □B̄_{n}^{c}.

In order to have a base of the topology, we need to consider all the finite intersections of sets of this form. But we have that

⋂_{1≤i≤k} U_{>,⟨n_{i},r_{i}⟩} = □ (B(0, min_{1≤i≤k} r_{i}) ⋂ ( ⋃_{1≤i≤k} B̄_{n_{i}} )^{c})
= □ (B(0, min_{1≤i≤k} r_{i}) ∩ K_{m}^{c}) for some m.

Thus we have a base of the upper topology by considering sets of the form

O_{>,⟨n,r⟩} =^{def} □ (B(0, r) ∩ K_{n}^{c}) .

Define

𝔗_{>} = (𝒦, τ_{>}, ν_{>}) where ν_{>}(p) = O_{>,p}.

Lemma 5.8 The following equivalences hold:

ν_{S}(m) ⊆ ν_{>}(⟨n, r⟩) ⟺ K̊_{m} ⊆ B(0, r) and K̊_{m} ∩ K_{n} = ∅,
ν_{>}(⟨n, r⟩) ⊆ ν_{S}(m) ⟺ K̊_{m} ∪ K_{n} ⊇ B(0, r).

Moreover, these predicates are recursive in n and m.

Proof This follows from Propositions 5.7 and 5.2. □

Proposition 5.9 𝔗_{>} and 𝔗_{S} are effectively equivalent.

Proof Choose an open O_{>,⟨n,r⟩} and a compact K ∈ O_{>,⟨n,r⟩}. Then we have that K ⊆ B(0, p) and K ∩K_{n} = ∅. Because K is compact and B(0, p)^{c} is closed, there exists ϵ > 0 such that B(K, ϵ) ⊆ B(0, p) and B(K, ϵ) ∩ K_{n} = ∅. Then choose a K_{m} according to Lemma 5.4 such that K ⊆ K̊_{m} ⊆ B(K, ϵ). Thus, by Lemma 5.8, we have that K ∈ ↑ ↑K_{m} ⊆ O_{>,⟨n,r⟩}. This proves that τ_{S} is finer than τ_{>}.

Now choose a K_{m} and K ∈ ↑ ↑K_{m}. Firstly, there is an index p with K_{m} ⊆ B(0, p). Secondly, there is ϵ > 0 with B(K, ϵ) ⊆ K̊_{m}. Since L = B̄(0, p)∩(K̊_{m})^{c} is a non-empty compact subset of ℝ^{N}, there is a K_{n} such that L ⊆ K̊_{n} ⊆ B(L, ϵ/2) according to Lemma 5.4. By the triangle inequality, we have that d(K_{n}, K) ≥ ϵ/2, so that K_{n} ∩ K = ∅. Thus K ∈ □ (B(0, r) ∩ K_{n}^{c}) = O_{>,⟨n,r⟩}. On the other hand, B(0, r) ⊆ L ∪ K̊_{m} ⊆ K_{n} ∪ K̊_{m}. Hence, by the Lemma 5.8, we have that O_{>,⟨n,r⟩} ⊆ ↑ ↑K_{m}, which proves that τ_{>} is finer than τ_{S}.

Now, we have proved that τ_{>} and τ_{S} are the same topology. Lemma 5.8 tells us also that the predicates ν_{>}(n) ⊆ (resp. ⊇) ν_{S}(m) are recursive. So we can apply Lemma 4.4 twice to obtain the desired result. □

In other words:

Theorem 5.10 A compact subset of ℝ^{N} is upper computable if and only it is Scott computable.

5.3 The lower topology

Weihrauch introduces another effective topology on 𝒦. A subbase of this topology is given by sets of the form

U_{<,⟨n,r⟩} =^{def} □B(0, r) ∩ ♢B_{n}.

As before, we need to take all the finite intersections of such sets. This gives us the following natural enumeration of the base:

O_{<,⟨n,r⟩} =^{def} □B(0, r) ⋂ (∩_{i=1}^{k}♢B_{n_{i}}) ,

where n = ⟨k, m⟩ and m = ⟨n_{1}, …, n_{k}⟩. Then 𝔗_{<} = (𝒦, τ_{<}, ν_{<}) where ν_{<}(p) =^{def}

O_{<,p}.

This topology gives information from the inside of a compact set. We want to relate it to the dual topology of the domain (𝒦, ⊇). A subbase of the dual topology is given by opens of the form 𝒦\ ↑K_{m}. Then we enumerate all the finite intersections of such open sets:

ν_{D}(m) =^{def} ⋂_{i=1}^{k} 𝒦\↑K_{m_{i}}

where m = ⟨k, n⟩ and n = ⟨m_{1}, ⋯, m_{k}⟩.

Lemma 5.11 For ν_{<}(n) =^{def} □B(0, r) ⋂ ∩_{i}♢B_{n_{i}} and ν_{D}(m) =^{def} ⋂_{j}(𝒦\ ↑K_{m_{j}}), we have that

ν_{<}(n) ⊆ ν_{D}(m) ⟺ ∀j∃i, B(0, r) ∩ B_{n_{i}} ∩ K_{m_{j}} = ∅.

This proves that the predicate ν_{<}(n) ⊆ ν_{D}(m) is r.e.

Proposition 5.12 𝔗_{<} is effectively reducible to 𝔗_{D} and τ_{<} is strictly finer than τ_{D}.

Proof As before, because we know that ν_{<}(n) ⊆ ν_{D}(m) is r.e., we only have to prove that τ_{<} is strictly finer than τ_{D}. For this, choose K and m such that K ∈ 𝒦\↑K_{m}. Then we have that K ⊈ K_{m}. So there exists a point x ∈ K \K_{m}, a ball B_{n} and a radius r > 0 such that x ∈ B_{n}, K ⊆ B(0, r) and B_{n} ∩ K_{m} = ∅. Now, let p satisfy

O_{<,p} = □B(0, r) ∩ ♢B_{n}.

Then it is clear that K ∈ O_{<,p} ⊆ 𝒦\↑K_{m}. Hence τ_{<} is finer than τ_{D}.

Now, for every m and every r > 0, we can find K ∈ ν_{D}(m) with K ⊈ B(0, r). This implies that we never have ν_{D}(m) ⊆ ν_{<}(n). Therefore τ_{D} can’t be as fine as τ_{<}. □

In this case, the topologies are not the same. The problem arises from the non-compactness of ℝ^{N}. The point is that we can’t have any boundedness information for a compact by looking at its neighbourhoods in the dual topology. Then, by virtue of Proposition 4.3, this implies that 𝔗_{D} can’t be effectively reducible to 𝔗_{<}.

However, we still have a positive effectivity result. For each R ∈ ℕ, we denote by 𝒦_{R} the set of all the compact subsets of the open ball B̄(0, R) that are not contained in the open ball B̄(0, R − 1), equipped with the induced effective topology (𝔗_{<,R} or 𝔗_{D,R}). Formally, we have 𝒦_{R} = □B(0, R) \ □B(0, R − 1).

Lemma 5.13 If K ∈ 𝒦_{R} then

K ∩ B_{n} ≠ ∅ ⟺ ∃m ∈ ℕ, K_{m} ∪ B_{n} ⊇ B(0, R) and K ⊈ K_{m}.

In this case, we have 𝒦_{R}\↑K_{m} ⊆ ♢B_{n}.

Proof (⟸) Immediate. (⟹) If K ∩ B_{n} ≠ ∅, then, because K is compact and B_{n} = B(x⃗_{n}, R_{n}) is open, there exists an ϵ > 0 such that K ∩ B(x⃗_{n}, R_{n} − ϵ) ≠ ∅. And because L = B̄(0, R) \ B̊_{n} is a compact set, we can apply Lemma 5.4 to obtain a basic compact set K_{m} such that L ⊆ K̊_{m} ⊆ B(L, ϵ). Then K_{m} ∩ B(x⃗_{n}, R_{n} − ϵ) = ∅. And because K ∩ B(x⃗_{n}, R_{n} − ϵ) ≠ ∅, we have that K ⊈ K_{m}. The choice of K_{m} proves that we have B_{n} ∪ K_{m} ⊇ B(0, R). □

Proposition 5.14 𝔗_{D,R} is effectively reducible to 𝔗_{<,R}.

Proof By the lemma, we may assume that we are given K ∈ ν_{<,R}(n) = 𝒦_{R} ⋂ □B(0, r) ⋂ ∩_{i}B_{n_{i}}. Then, for each n_{i} there exists an m_{i} such that K ∈ 𝒦_{R}\ ↑ K_{m_{i}} ⊆ ♢B_{n_{i}}. Intersecting all these subbasic dual neighbourhoods of K, we get an index m such that K ∈ ν_{D,R}(m) ⊆ ν_{<,R}(n). This proves that τ_{D,R} is finer than τ_{<,R}. Moreover, we can deduce from the same lemma that ν_{D,R}(m) ⊆ ν_{<,R}(n) is r.e. Therefore the result follows from Lemma 4.4. □

The following is an immediate consequence of the above development:

Theorem 5.15 A compact subset of ℝ^{N} is lower computable if and only if it is dual computable.

Notice that this is a slightly paradoxical situation. We have two notions of computability on 𝒦 with the same computable elements, but it is impossible to effectively translate the dual name of a compact set into its upper name, even if the compact set is computable. To show the equivalence we used our noneffective, a priori knowledge that our elements are compact and hence bounded, without any information about the bound.

5.4 The strong topology

If we consider the join of the two effective topologies of Weihrauch, we get a stronger effective topology which coincides with the Vietoris topology (induced by the Hausdorff metric). We call 𝔗_{H} = (𝒦, τ_{H}, ν_{H}) this effective topology with ν_{H}(⟨m, n⟩) = ν_{>}(n) ∩ ν_{<}(m). Similarly, we have the Lawson effective topology that we call 𝔗_{L} = (𝒦, τ_{L}, ν_{L}) where ν_{L}(⟨m, n⟩) = ν_{S}(n) ∩ ν_{D}(m). We prove that these topologies are effectively equivalent.

Proposition 5.16 𝔗_{H} and 𝔗_{L} are effectively reducible to each other.

Proof The fact that 𝔗_{H} is effectively reducible to 𝔗_{L} comes from the fact that 𝔗_{V} is the join of 𝔗_{>} and 𝔗_{<}, and each of these effective topologies is effectively reducible respectively to 𝔗_{S} and 𝔗_{D}.

In the other direction, by Proposition 5.9, we have a recursive operator Φ_{S→>} that reduces 𝔗_{S} to 𝔗_{>}. Suppose we are given a K ∈ 𝒦 with Lawson name A. Each time we read a q = ⟨m, p⟩ ∈ A, we can compute an r ∈ ℕ such that K ∈ B(0, r) because we know that K ⊆ K̊_{m}. So, for each r that we parse, we fork a process. This process parses A from the beginning and each time it parses q′ = ⟨m′, p′⟩ ∈ A, it forks again and the new child process prints the list of all the pairs ⟨r, n⟩ such that K_{p′} ∪ B_{n} ⊇ B(0, r) (remember that K ⊈ K_{p′}). By Lemma 5.13, we are enumerating all the subbasic lower neighbourhoods of K. Now, by taking the indices of all the finite intersections, we can generate the lower name of K. This algorithm describes a recursive operator Φ_{L→<} that translates a Lawson name to a lower name. And with the previous operator Φ_{S→>}, we can construct an effective operator Φ_{L→H} from 𝔗_{L} to 𝔗_{H}. □

We have already mentioned that the dual topology is not effectively reducible to the lower topology. But with the help of the information that comes from the Scott topology (essentially an information on the bound of a compact set that is unreachable by the dual topology), we have been able to effectively obtain the lower name.

Theorem 5.17 A compact subset of ℝ^{N} is strongly computable if and only if it is Lawson computable.

Acknowledgements. This work was developed during a visit of the second named author to the DI of the Ecole Normale Supérieure of Paris in January 2000. He is grateful to Giuseppe Longo for the invitation, and to all members of the DI for the hospitality. The authors are also grateful to Giuseppe Longo for lively technical discussions.

References

[1] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3. Clarendon Press, 1994.

[2] M. Alvarez-Manilla, A. Jung, and K. Keimel. The probabilistic powerdomain for stably compact spaces. Theoretical Computer Science, 328:221, 2004.

[3] R.M. Amadio and P.-L. Curien. Domains and Lambda-Calculi, volume 46 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998.

[4] V. Brattka and K. Weihrauch. Computability on subsets of Euclidian space I: closed and compact subsets. Theoretical Computer Science, 219:65–93, 1999.

[5] M.H. Escardó. On the compact-regular coreflection of a stably compact locale. In Proceedings of the 15th conference on Mathematical Foundations of Programming Semantics (MFPS XV), volume 20 of Electronic Notes in Theoretical Computer Science. Elsevier, 1999.

[6] M.H. Escardó. The regular-locally-compact coreflection of stably locally compact locale. Journal of Pure and Applied Algebra, 157(1):41–55, 2001.

[7] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer–Verlag, 1980.

[8] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. Continuous Lattices and Domains. Cambridge University Press, 2003.

[9] A. Jung, M. Kegelmann, and M. A. Moshier. Stably compact spaces and closed relations. In S. Brookes and M. Mislove, editors, 17th Conference on Mathematical Foundations of Programming Semantics, volume 45 of Electronic Notes in Theoretical Computer Science. Elsevier, 2001.

[10] A. Jung and R. Tix. The troublesome probabilistic powerdomain. In A. Edalat, A. Jung, K. Keimel, and M. Kwiatkowska, editors, Third Workshop on Computation and Approximation, volume 13 of Electronic Notes in Theoretical Computer Science. Elsevier, 1998.

[11] J.D. Lawson. The versatile continuous order. In M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Mathematical Foundations of Programming Languages, volume 298 of Lecture Notes in Computer Science, pages 134–160, 1987.

[12] J.D. Lawson. Spaces of maximal points. Math. Structures Comput. Sci., 7(5):543–555, 1997. Logic, domains, and programming languages (Darmstadt, 1995).

[13] M. Mislove. Topology, domain theory and theoretical computer science. Topology and its Applications, 89(1–2):3–59, 1998.

[14] M. A. Moshier and A. Jung. A logic for probabilities in semantics. In Julian Bradfield, editor, Computer Science Logic, volume 2471 of Lecture Notes in Computer Science, pages 216–231. Springer Verlag, 2002.

[15] H. Rogers, Jr. Theory of Recursive Functions and Effective Computability. McGraw–Hill series in higher mathematics. McGraw–Hill, 1967.

[16] D.S. Scott. Data types as lattices. SIAM Journal on Computing, 5:522–587, 1976.

[17] M.B. Smyth. Effectively given domains. Theoretical Computer Science, 5:257–274, 1977.

[18] M.B. Smyth. Topology. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 1, pages 641–761. Clarendon Press, Oxford, 1992.

[19] S.J. Vickers. Topology via Logic. Cambridge University Press, Cambridge, 1989.

[20] K. Weihrauch. A simple introduction to computable analysis. Informatik Berichte, 171, 1995. Second Edition.

[21] K. Weihrauch. An introduction to computable analysis. Springer–Verlag, 2000.