To Appear in Mathematical Logic Quarterly

\begin{matrix}c \\ ◯ \end{matrix} WILEY-VCH Verlag Berlin GmbH 2001

In Domain Realizability, not all Functionals on C[−1, 1] are Continuous

Martín Escardó^{a} and Thomas Streicher^{b}

a School of Computer Science, University of Birmingham, Birmingham B15 2TT, England^{1)}

b Fachbereich Mathematik, Technishe Universität Darmstadt, Schloßgartenstraße 7, 64289, Darmstadt, Germany^{2)}

Abstract. In this note we exhibit a continuity principle for real-valued functions on C[−1, 1] that is not validated by realizability over domains although it is validated by Kleene’s functional realizability corresponding to Weihrauch’s theory of type 2 effectivity.

Mathematics Subject Classification: 03F50, 03F60, 18C50, 06B35.

Keywords: Domain realizability, continuity principles.

1 Introduction

It is well known (see e.g. [1]) that in the function realizability topos RT(K_{2}), where K_{2} is the so-called 2^{nd} Kleene algebra with underlying set ℕ^{ℕ}, it holds that

“all functions from C[−1, 1] to ℝ are continuous”. This follows from the validity in RT(K_{2}) of the statement that “all functions from ℕ^{ℕ} to ℕ are continuous”, which in turn is equivalent to the statement that “all functions between complete separable metric spaces are continuous” (see e.g. [3]). It is also well known, from e.g. [3], that in realizability over Pω the statement “all functions from ℕ^{ℕ} to ℕ are continuous” is not valid internally, despite the fact that from the external point of view all morphisms from ℕ^{ℕ} to ℕ are actually continuous. This remains true when considering realizability over 𝕋^{ω} or some universal Scott domain. However, one may show, using the so-called Berger–Gandy functional that computes a uniform modulus of continuity for total functionals from Cantor space 2^{ℕ} to ℕ, that in RT(𝕋^{ω}) it holds that

“all functions from ℝ^{n} to ℝ are continuous” for all natural numbers n. Thus, there arises quite naturally the question whether domain realizability validates continuity of real-valued functionals on infinite dimensional Banach spaces. The aim of this note is to answer this question negatively for the space C[−1, 1] of continuous functionals from the closed interval [−1, 1] to ℝ under the supremum norm. However, the proposition “there is a discontinuous function from C[−1, 1] to ℝ” does not hold either as from it one could derive the limited principle of omniscience (see [3]) which fails in RT(𝕋^{ω}) as there all maps from 2^{ℕ} to 2 are continuous.

1)e-mail: M.Escardo@cs.bham.ac.uk

2)e-mail: streicher@mathematik.tu-darmstadt.de

\begin{matrix}c \\ ◯ \end{matrix} WILEY-VCH Verlag Berlin GmbH, 13086 Berlin, 2001 0942-5616/00/000-0001 $ 17.50+.50/0

We wish to thank P. Lietz for asking the question we answer in this note and A. Bauer and A. Simpson for discussions about the problem and our preliminary attempts to solve it.

2 The Theorem

Before proceeding to the statement and the proof of the theorem, we review some terminology and notation. For general information about realizability and domain theory see [1] and [2], respectively.

As 𝕋^{ω} is a universal domain for the category Dom_{coh} of coherently complete countably algebraic cpo’s (with ⊥) we know that RT(𝕋^{ω}) and RT(Dom_{coh}) are equivalent categories. Actually, all our considerations will take place within PER(Dom_{coh}), the category of per’s on domains in Dom_{coh} and equivariant continuous maps as morphisms. But all our arguments apply also for the case when Dom_{coh} is replaced by the more popular category Dom of Scott domains.

We write C for partial Cantor space and B for partial Baire space, i.e. [ℕ → 3_{⊥}] and [ℕ → ℕ_{⊥}], respectively, where 3 = {−1, 0, 1}. A canonical admissible representation of [−1, 1] by the total Cantor space is given by assigning x = ∑_{n=0}^{∞} γ_{n} · 2^{−n} ∈ [−1, 1] to γ: ℕ → 3 in which case we write γ ⊩ x.

We now proceed to the formulation and proof of our theorem.

T h e o r e m 2.1. The statement

“not all functions from C[−1, 1] to ℝ are continuous” is valid in RT(T^{ω}).

As usual, a functional F is called continuous iff

∀f ∈ C[−1, 1]. ∀n ∈ ℕ. ∃k ∈ ℕ.∀g ∈ C[−1, 1]. ||f−g|| < 2^{−k} ⟹ |F (f)−F (g)| < 2^{−n}

where ||.|| is the supremum norm on C[−1, 1].

P r o o f. If RT(𝕋^{ω}) would validate “all functions from C[−1, 1] to ℝ are continuous” then there would exist a continuous functional M: [[C → B] → B] → N satisfying the specification that whenever ϕ ⊩ F then M(ϕ) = n ∈ ℕ with

(†) |F (f) − F (0)| < 2^{−1} for all f ∈ C[−1, 1] with ||f|| < 2^{−n}.

For deriving a contradiction from this assumption first recall the following fact from functional analysis.

L e m m a 2.2. Consider the sequence F_{k}: C[−1, 1] → ℝ of linear continuous functionals where F_{k}(f) = f(0) − f(2^{−k}). For all k there is an f ∈ C[−1, 1] with ||f|| = 1 and |F_{k}(f)| = 2. However, the sequence F_{k} converges to O: = λf ∈ C[−1, 1].0 in the sequential topology, i.e. lim_{k→∞} F_{k}(f_{k}) = 0 for any convergent sequence f_{k} in the norm topology of C[−1, 1].

For c > 0 the sequence c · F_{k} also converges to O in the sequential topology and for every k there is an f ∈ C[−1, 1] with ||f|| = 1 such that |c · F_{k}(f)| = 2c. Thus, the optimal modulus of continuity for c · F_{k} w.r.t. \frac{1}{2} at O is precisely \frac{1}{4c}.

P r o o f. For every continuous function f with f(0) = 1 and f(2^{−k}) = −1 we have F_{k}(f) = 2. There are plenty of continuous functions f with ||f|| = 1 satisfying f(0) = 1 and f(2^{−k}) = −1. For such f we have ||f|| = 1 and |F_{k}(f)| = 2.

Now suppose that f_{k} converges to some f in the norm topology. Then by the triangle inequality we have

|F_{k}(f_{k})| ≤ |f_{k}(0) − f(0)| + |f(0) − f(2^{−k})| + |f(2^{−k}) − f_{k}(2^{−k})|
< |f(0) − f(2^{−k})| + 2||f − f_{k}||

and, therefore, as the right hand side goes to 0 when k goes to ∞ this holds also for the left hand side of the inequality. Thus, the sequence F_{k} converges to O in the sequential topology. From these considerations the corresponding statement for the sequence c · F_{k} follows immediately.

Thus, for every c > 0 there is an f ∈ C[−1, 1] with ||f|| = \frac{1}{4c} and |c · F_{k}(f)| = \frac{1}{2} from which it follows that

∀f ∈ C[−1, 1]. (||f|| < δ ⟹ |c · F_{k}(f)| < \frac{1}{2})

holds precisely for δ ≤ \frac{1}{4c}. Thus, the optimal modulus of continuity for c · F_{k} w.r.t. \frac{1}{2} at O is \frac{1}{4c}. □

Furthermore, we need the following.

L e m m a 2.3. There is a continuous function znorm: C → C such that

(1) if α ⊩ x ∈ [−1, 1] then znorm(α) ⊩ x and

(2) if α ⊩ 0 then znorm(α) = 0^{∞} ⊩ 0.

That is, znorm realizes the identity on [−1, 1] and sends all realizers of 0 to 0^{∞} = λn: ℕ.0, the canonical realizer for 0.

P r o o f. The function znorm is given by the following functional program

znorm(0 : x) = 0 : znorm(x)

znorm(1 : −1 : x) = znorm(0 : 1 : x) = 0 : znorm(1 : x)

znorm(−1 : 1 : x) = znorm(0 : −1 : x) = 0 : znorm(−1 : x)

znorm(1 : 0 : x) = 1 : 0 : x

znorm(1 : 1 : x) = 1 : 1 : x

znorm(−1 : 0 : x) = −1 : 0 : x

znorm(−1 : −1 : x) = −1 : −1 : x

which sends infinite streams to infinite streams as it reads at most two items of input before producing some item of output.

As znorm(1 : −1^{∞}) = 0 : znorm(1 : −1^{∞}) and znorm(−1 : 1^{∞}) = 0 : znorm(−1 : 1^{∞}) it follows that znorm(1 : −1^{∞}) = 0^{∞} = znorm(−1 : 1^{∞}) and, therefore, all realizers of 0, namely 0^{∞}, 0^{k}: 1 : −1^{∞} and 0^{k}: −1 : 1^{∞}, are mapped to 0^{∞} by znorm. □

Now suppose that M: [[C → B] → B] → N is a continuous domain function satisfying condition (†) above and the requirement that whenever ϕ ⊩ F: C[−1, 1] → ℝ then M(ϕ) = n ∈ ℕ. Let ϕ = λc: C.0^{∞}: C → B and n: = M(ϕ).

Using Lemma 2.3 there is a function ρ: B → B such that

(1) ρ realizes the function r: ℝ → ℝ which is the identity on [−1, 1] and sends all other numbers to 1 if they are positive and to −1 if they are negative

(2) ρ(α) = 0^{∞} whenever α ⊩ 0. Let γ be a realizer for 2^{n} ∈ ℝ and α_{k} a sequence in C such that α_{k} ⊩ 2^{−k} for all k and lim_{k→∞} α_{k} = 0^{∞} in C. Consider the sequence ϕ_{k} in [C → B] → B with

ϕ_{k}(f) = ρ(mult(γ, sub(f(0^{∞}), f(α_{k}))

where sub and mult realize subtraction and multiplication on ℝ, respectively. Obviously, the domain-theoretic functions ϕ_{k} realize the continuous maps r ∘ (2^{n} · F_{k}) from C[−1, 1] to ℝ where the F_{k} are as in Lemma 2.2 and r is as in (1) above. It follows from Lemma 2.2 with c = 2^{n} that for all k the optimal modulus of continuity of r ∘ (2^{n} · F_{k}) w.r.t. \frac{1}{2} at λx.0 is 2^{n+2}. Thus, we have M(ϕ_{k}) ≥ n + 2 for all k. As the α_{k} converge to 0^{∞} the ϕ_{k} converge to some ϕ′ with

(3) ϕ′(h) = 0^{∞} for all h ∈ C → B realizing some function in C[−1, 1] and

(4) M(ϕ′) ≥ n + 2 as the M(ϕ_{k}) converge to M(ϕ′). Then ϕ̃: = λh: [C → B]. (0^{∞} ⊓ ϕ′(h)) is a continuous function below ϕ and ϕ′ and still realizes O. Thus M(ϕ̃) is a natural number and M(ϕ̃) ⊑ M(ϕ), M(ϕ′). Thus, we have M(ϕ̃) = n and, therefore, n ⊑ M(ϕ′) contradicting (4) and hence concluding the proof of Theorem 2.1. □

We think that the above theorem can be extended to other infinite dimensional spaces like Hilbert space etc. We consider our result as a contribution to the question of comparing domain realizability with function realizability. The former is more suitable for extracting functional programs from constructive proofs whereas the latter supports comfortable principles like continuity axioms for a wide class of spaces.

References

[2] Abramsky, S. and Jung, A. Domain Theory. In: Handbook of Logic in Computer Science, Vol. 3, pp.1–168, Oxford University Press (1994).

[1] Bauer, A. The Realizability Approach to Computable Analysis and Topology. PhD Thesis, Carnegie–Mellon University. (2000).

[3] Troelstra, A. and van Dalen, D. Constructivism in Mathematics. 2 volumes, Elsevier (1988).

[4] Weihrauch, K. Computable analysis. Texts in Theoretical Computer Science. Springer (1988).

(Received: December 21, 2001; Revised: March 27, 2002)