17119 LABEL:LastPageOct. 14, 2019Mar. 02, 2021

# Constructive Domains with Classical Witnesses

Dirk Pattinson  The Australian National University<EMAIL_ADDRESS>and  Mina Mohammadian  The Australian National University and University of
Tabriz<EMAIL_ADDRESS>
###### Abstract.

We develop a constructive theory of continuous domains from the perspective of
program extraction. Our goal that programs represent (provably correct)
computation without witnesses of correctness is achieved by formulating
correctness assertions classically. Technically, we start from a predomain
base and construct a completion. We then investigate continuity with respect
to the Scott topology, and present a construction of the function space. We
then discuss our main motivating example in detail, and instantiate our theory
to real numbers that we conceptualise as the total elements of the completion
of the predomain of rational intervals, and prove a representation theorem
that precisely delineates the class of representable continuous functions.

###### Key words and phrases:

Domain Theory, Constructive Mathematics, Real Number Computation, Predomain
Base, Function Spaces

## Introduction

The ability to extract programs from proofs is one of the hallmark features of
constructive mathematics [TvD88]: from a proof of a formula of the form
$\forall x\exists yP(x,y)$ we can automatically obtain a (computable)
_function_ $f$ such that $P(x,f(x))$ for all $x$. Within mathematics, the
variables usually have _types_ , such as natural or real numbers, or functions
between types.

Computationally, while some of these types, such as the natural numbers, can
be computed with directly, there is no immediate way to compute with others.
The prime example here are the real numbers that are represented either as
infinitely-long running Turing machines [Wei00], rational Cauchy sequences
with modulus [BB85], linear fractional transformations [HE02], digit streams
[ME07] or domains [ES98].

From the view of program extraction, the data structure that is used to
represent mathematical objects is systematically derived from their
definition. If we define real numbers to be Cauchy sequences with modulus,
then programs extracted from an existence proof will produce just that – a
Cauchy sequence with modulus. The vast majority of the work on constructive
real analysis and program extraction has focussed on the Cauchy representation
and its variants such as the signed digit representation, e.g. [TvD88, BB85,
Ber11]. There is little work on other representations, with the notable
exception of [BK09] which develops a theory of constructive domains that is
instantiated to obtain representations of real numbers.

In domain theory, real numbers are represented as nested sequences of
(rational, or dyadic) intervals, with the interpretation that every interval
gives an upper and lower bound to the number being approximated. In other
words, every sequence element gives a guaranteed enclosure of the actual
result, and the successive computation of sequence elements can be halted if
the actual precision, measured by the interval width, falls below a given
threshold.

Compared with a representation as Cauchy sequences with modulus, domains offer
two attractive features. First, every stage of approximation carries an actual
error bound, rather than the worst case error, as given by the modulus of
convergence for Cauchy reals. For example, computing the square root of $2$
using Newton iteration (as carried out in e.g. [Sch16]) one obtains a rational
Cauchy Sequence $(a_{n})_{n}$ such that for example,
$|a_{5}-a_{n}|\leq\frac{1}{6\cdot 2^{4}}\approx 5.2\times 10^{-3}$ for all
$n\geq 5$. Instantiating the same method to obtain a shrinking sequence
$(a_{n},b_{n})_{n}$ of nested rational intervals such that $a_{n}^{2}\leq
2\leq b_{n}^{2}$ one obtains that $|b_{n}-a_{n}|\approx 5.7\times 10^{-49}$
for $n\geq 5$. Both methods use the same initial approximation of $\sqrt{2}$,
and indeed the computed Cauchy sequence is identical to the sequence of upper
interval endpoints. The significant difference is explained as the modulus is
a worst case estimate, whereas the differences between upper and lower
interval endpoint are obtained from the actual computation and avoid over-
estimation. We showcase this by means of an example in Section 7.

The second attractive feature of a domain theoretic approach is that most
classes of domains are closed under the formation of function spaces, i.e. one
systematically obtains a representation of the space of e.g. real-valued
functions.

Both motivate the development of a more general theory of domains, as e.g.
carried out in [BK09]. Our work is similar in spirit, focuses on extracted
programs and data type as an end goal. Specifically, our aim is to extract
(necessarily effective) functions that operate on the basis of the domains
under consideration. For the special case of real numbers (and functions), our
goal is to obtain algorithms in the style descibed in [ES98]. There,
mathematical operations (such as computing square roots) are first extended to
an appropriate domain (such as the interval domain), then restricted to the
base of the domain, and in a third step, shown to be recursive by considering
a computable enumeration of basis elements. Indeed, one of our goals is to
short-circuit effectivity considerations that are often laborious and provide
little insight. Our slogan is “proofs, not programs” as the constructive
reasoning (via a realisability interpretation) immediately yields necessarily
recursive algorithms.

Putting the extracted algorithm into the centre of attention gauges the
formulation of the notion of domain, and this is where differences to [BK09]
begin to emerge. The programs we are seeking to extract should embody _just_
the computational essence, but no additional terms that evidence correctness.
For example, when extracting a program to compute a real number, we only seek
a nested sequence of intervals, but _not_ a witness of the fact that the
intervals are converging to zero in width. This is similar to the approach
taken in [Ber11] where one freely adds (true) axioms without computational
content to the theory that forms the basis of extraction. That is, we are
interested in constructive existence, but are content with classical
correctness. Conceptually, this can be understood as phrasing correctness in
the classical (double negation) fragment of constructive logic. Technically,
the (intended) consequence of this is that correctness proofs do not have any
computational content, and are therefore invisible after program extraction,
using a standard realisability interpretation [TvD88].

For example, subjecting the proof of the existence of the square root of two
to a realisability interpretation, our aim is to extract only a nested
sequence of intervals. To achieve this, the definition of equality needs to be
free of computational content. We solve this by judiciously setting up the
theory in such a way that treats existence of objects as constructive
existence, whereas properties are usually formulated classically.

Another aspect where our theory puts the extracted algorithm into the centre
of attention is the definition of completion of domain bases. It is one of the
hallmark features of domains that ideal elements (such as infinite sequences,
or real numbers) can be approximated by elements of a _base_. Constructively,
we take the notion of a base as primitive, and recover ideal elements in the
completion of the base. Classical domain theory, see e.g. [AJ94] usually
considers completion by directed suprema. Here, take the same approach as
[BK09] and consider completions by infinite sequences, as they are much more
easily representable computationally.

_Plan of the paper and main results._ We introduce the notion of a _predomain
base_ that is similar to [BK09] in Section 2, but our definition of the way-
below relation is classical, and we establish some basic lemmas, notably
interpolation, for later use. We also introduce our main motivating, and
running, example, the predomain base of formal intervals. In Section 3, we
introduce the continuous completion of a predomain base, along with a
(defined) notion of equality. As foreshadowed in the introduction, equality
(defined in terms of way-below) is classical and devoid of computational
content. The main result here is the extension property that allows us to
extend any continuous function defined on a predomain base to its completion.

In Section 4 we align the order-theoretic notion of order-theoretic continuity
to topological continuity. As expected, this necessitates a classical
definition of the Scott topology which we also show to be generated by upsets
of the way-below relation as in the classical theory. In particular, we can
show that order-theoretic and topological continuity coincide. Our
consideration of continuity naturally leads to the construction of function
spaces that we carry out in Section 5. In the classical theory, function
spaces are constructed as the set of Scott continuous functions, with
pointwise ordering. Here, we investigate the construction of function spaces
on the level of predomain bases. More specifically, we present a construction
of a predomain base, the completion of which precisely captures the space of
continuous functions between the completion of two bases. In Sections 6 we
specialise our theory to our initial motivating example, and recapture real
numbers as the total elements of the (continuous completion of the) domain of
formal intervals. We show that the Euclidean topology arises as the
restriction of the Scott topology to real numbers, and investigate the
relationship between Cauchy reals and the domain-theoretic reals. As a
consequence of our constructive existence – classical correctness approach,
both notions are only equivalent if Markov’s principle holds (and in fact, we
can prove Markov’s principle from their equivalence). We conclude by relating
$\epsilon$-$\delta$ continuous functions to the restrictions of Scott
continuous total functions. This unearthes a new notion of continuity which
appears to be weaker than uniform continuity but at the same time stronger
than pointwise continuity that we call _intensional non-discontinuity_. We
leave the question of a more detailed analysis of this notion to future work.

_Related work._ We have already mentioned [BK09] which is closest to the work
reported in this paper. The main differences are that our notions of way-below
and equality are defined classically whereas _op.cit._ employs constructive
definitions. We also present a construction of function spaces as completion
of predomain bases in Section 5.

Our work stands in the tradition of Bishop-style constructive analysis,
[BB85], and indeed we work in a purely constructive setting. What is different
is our treatment of real numbers that we derive from the interval domain,
similarly to the classical treatment of real analysis in [dG97, ES99] via
continuous domains, except that we do not focus on the (classical) notion of
computability. Again from a classical perspective, our real numbers (and
functions) can be thought of as the total objects of (constructively
understood) domains, studied in [Ber93b], although we don’t investigate the
notion of totality _per se_. The comparison between different notions of
continuity on the induced set of real numbers is of course insipred by
[Ish92]. Much of this paper is owed to discussions with Helmut Schwichtenberg.
His notes [Sch16] develop constructive analysis with a view to program
extraction, and the question that motivated the present paper was whether this
is also possible using a domain representation of the reals, rather than a
Cauchy sequence representation with a worst-case modulus of convergence.

##  1\. Preliminaries and Notation

We work in standard Bishop-style constructive mathematics [BB85] that we
envisage as being formalised in higher-type intuitionistic arithmetic
$\mathsf{HA}^{\omega}$ [TvD88]. We write $\mathbb{N}$ for the natural numbers,
$\mathbb{Z}$ for the integers and $\mathbb{Q}$ for the rationals, and
$\mathbb{Q}_{>0}$ for the positive rationals.

We use the term ’weak existence’ to refer to the weak existential quantifier
$\tilde{\exists}=\neg\forall\neg$ which is constructively equivalent to
$\neg\neg\exists$. In informal reasoning, we often say that ‘there must exist
$x$ such that $A$’ or ‘there weakly exists $x$ such that $A$’ for
$\tilde{\exists}x.\,A$. We read defined operations universally, that is
assuming that $A(x)$ defines $x$ uniquely ($(A(x)\wedge A(y))\to x=y$) and we
let $\phi(x)$ denote ‘the unique $x$ such that $A(x)$’, we read a formula
$B(\phi(x))$ as $\forall x.\,A(x)\to B(x)$. In particular, if there must exist
$x$ such that $A(x)$, using $\phi(x)$ does not assert (strong) existence.

##  2\. Predomain Bases and Interpolation

A _predomain base_ is a countable ordered structure that collects finitely
representable objects used to approximate elements of ideal structures, such
as the real numbers. Examples of predomain bases are finite sequences
(approximating infinite streams) and rational intervals (approximating real
numbers). The order structure captures information content, such as the prefix
ordering for finite sequences, and reverse inclusion for rational intervals.

Predomain bases are the constructive analogue of a base in classical domain
theory [AJ94], where arbitrary elements of the domain can be displayed as
directed suprema of base elements. In a constructive setting, the totality of
the domain is not given and needs to be constructed, similar to the
(constructive) notion of real numbers as rational Cauchy sequences with a
modulus of convergence. This section discusses basic properties of predomain
bases, and we then construct completions in Section 3.

######  Definition  (Predomain Bases).

Let $(B,\sqsubseteq)$ be a poset. A _chain_ in $B$ is a sequence $(b_{n})_{n}$
such that $b_{n}\sqsubseteq b_{n+1}$ for all $n\in\mathbb{N}$. If
$(C,\sqsubseteq)$ is (another) poset, we call a monotone function $f:C\to D$
_Scott continuous_ if $f(\bigsqcup_{n}b_{n})=\bigsqcup_{n}f(b_{n})$ for all
chains $(b_{n})_{n}$, provided that all suprema in the last equality exist. An
element $b$ is _way below_ an element $c\in B$ if there must exist
$n\in\mathbb{N}$ such that $b\sqsubseteq x_{n}$ whenever $(x_{n})$ is a chain
in $B$ with $\bigsqcup_{n}x_{n}\in B$ and $c\sqsubseteq\bigsqcup_{n}x_{n}$. We
write $b\ll c$ if $b$ is way below $c$, and also say that $b$ _approximates_
$c$. A chain $(b_{n})$ is an _approximating sequence_ of $b\in B$ if $b_{n}\ll
b$ for all $n\in\mathbb{N}$ and $\bigsqcup_{n}b_{n}=b$. A _predomain base_ is
a countable poset $B=\\{b_{n}\mid n\in\mathbb{N}\\}$ with decidable ordering
$\sqsubseteq$ in which every element has an approximating sequence.

A non-empty, finite set $B_{0}\subseteq B$ is _consistent_ , written
$\mathsf{Cons}(B_{0})$ if it must have an upper bound, i.e. there must exist
$b^{\prime}\in B$ such that $b\sqsubseteq b^{\prime}$ for all $b\in B$. We say
that consistency is _continuous_ if $a_{i}=\bigsqcup_{j}a_{i,j}$ for all $i\in
I$ and $\mathsf{Cons}\\{a_{i,j}\mid i\in I\\}$ for all $j\in\mathbb{N}$
implies $\mathsf{Cons}\\{a_{i}\mid i\in I\\}$ where $I$ is a nonempty, finite
set. The poset $(B,\sqsubseteq)$ is _bounded complete_ if every finite
consistent subset $B_{0}\subseteq B$ has a least upper bound $\bigsqcup
B_{0}$, and _pointed_ if it has a least element $\bot\in B$.

Note that all non-empty bounded complete posets are necessarily pointed, and
that consistency is not necessarily continuous as we demonstrate in Example 2.

######  Remark .

The notion of predomain base differs from that of [BK09] in that _op.cit._
requires that an approximating sequence be a $\ll$-chain. This immediately
entails interpolation: if $x\ll z$ in a predomain base (where every element
has an approximating $\ll$-chain), we have $z=\bigsqcup_{n}z_{n}$ for a
$\ll$-chain $(z_{n})_{n}$ so that $x\sqsubseteq z_{n}$ for some $n$ by
definition of $\ll$. But then $x\sqsubseteq z_{n}\ll z_{n+1}\ll
z_{n+2}\sqsubseteq z$ so that $x\ll z_{n+1}\ll z$, i.e. $y=z_{n+1}$
interpolates between $x$ and $z$.

We require that every element $x\in B$ can be displayed as
$x=\bigsqcup_{n}x_{n}$ where each $x_{n}\ll x$ which is strictly weaker. As a
consequence, we need additional hypotheses to establish interpolation in
Corollary 3. On the other hand, our definition makes it easier to construct
predomain bases as we don’t need to ensure that approximating sequences are
$\ll$-chains, as for example in the construction of function spaces given
later in Lemma 5.37.

We are also adopting a different (weaker) definition of the way-below relation
that is formulated using strong existence in _op.cit._ Both are equivalent if
Markov’s Principle is assumed. By directly phrasing the way-below relation in
terms of weak existence, Markov’s Principle can be avoided. A helpful pattern
of proof that exploits weak existence is the following. Suppose that
$\Gamma,\exists x.A\vdash B$ and $\Gamma\vdash\tilde{\exists}x.A$. Then
$\Gamma\vdash\neg\neg B$. Similarly, the notion of bounded completeness,
phrased in terms of weak existence, is stronger than that of _op.cit._ which
uses strong existence. Technically, we need to use weak existence of an upper
bound to establish that the continuous completion of a (bounded complete)
predomain base has suprema of all increasing chains (Corollary 6).
Conceptually, weak existence suffices as the witness of boundedness of a
finite subset of a predomain base is not used in the construction of the least
upper bound.

######  Example .

Let $B$ be a countable set with decidable equality, that is, $\forall
b,b^{\prime}\in B.(b=b^{\prime})\lor\neg(b=b^{\prime})$ is (constructively)
provable. Then $(B,=)$ and $(B^{*},\sqsubseteq_{\mathsf{pref}})$ are predomain
bases where $B^{*}$ is the set of finite sequences of $B$ and
$\sqsubseteq_{\mathsf{pref}}$ is the prefix ordering. Both are bounded
complete and satisfy $x\ll x$ for all $x\in B$ (resp. $x\in B^{*}$).

If $(B,\sqsubseteq)$ and $(C,\sqsubseteq)$ are predomain bases, then so are
$B\times C$ and $B+C$ with the pointwise and co-pointwise ordering. Moreover
$(B_{\bot},\sqsubseteq_{\bot})$ is a predomain base where
$B_{\bot}=B\cup\\{\bot\\}$ (we tacitly assume $\bot\notin B$) and
$b\sqsubseteq c$ if either $b=\bot$ or $b\neq\bot\neq c$ and $b\sqsubseteq c$.
The predomain bases $B\times C$, $B+C$ and $B_{\bot}$ are the _product_ ,
_coproduct_ and _lifting_ of $B$ and $C$ (resp. of $B$).

######  Example .

The poset $\mathsf{I}\mathbb{Q}=\\{(p,q)\in\mathbb{Q}\times\mathbb{Q}\mid
p\leq q\\}$ ordered by $(p,q)\sqsubseteq(p^{\prime},q^{\prime})$ iff $p\leq
p^{\prime}\leq q^{\prime}\leq q$ is called the _predomain base of rational
intervals_. We usually write $[p,q]$ for the pair
$(p,q)\in\mathsf{I}\mathbb{Q}$ and think of $[p,q]$ as a rational interval.
For $\alpha=[a,b]\in\mathsf{I}\mathbb{Q}$, we sometimes write
$\alpha=[\underline{\alpha},\overline{\alpha}]$ to denote the lower and upper
endpoint of $\alpha$, and
$\alpha\pm\delta=[\underline{\alpha}-\delta,\overline{\alpha}+\delta]$ for the
symmetric extension of $\alpha$ by $\delta\in\mathbb{Q}_{\geq 0}$.

It is not immediate (but easy) to see that $\mathsf{I}\mathbb{Q}$ is a
predomain base. The negative formulation of $\ll$ gives the following
characterisation that has been established in [BK09, Proposition 7.2] using
Markov’s Principle.

######  Lemma .

Let $[p,q],[p^{\prime},q^{\prime}]\in\mathsf{I}\mathbb{Q}$. Then
$[p,q]\ll[p^{\prime},q^{\prime}]\mbox{ iff }p<p^{\prime}\leq q^{\prime}<q$.

###### Proof.

For the only-if direction, assume that $[p,q]\ll[p^{\prime},q^{\prime}]$. As
$[p^{\prime},q^{\prime}]=\bigsqcup_{n}[p^{\prime}-2^{-n},q^{\prime}+2^{-n}]$
there must exist $n\in\mathbb{N}$ such that
$[p,q]\sqsubseteq[p^{\prime}-2^{-n},q^{\prime}+2^{-n}]$ from which we obtain
that $p\leq p^{\prime}-2^{-n}<p^{\prime}\leq q^{\prime}<q^{\prime}+2^{-n}\leq
q$ and hence $p<p^{\prime}\leq q^{\prime}<q$ using decidability of order on
$\mathbb{Q}$.

For the converse, assume that $p<p^{\prime}\leq q^{\prime}<q$ and assume that
$[p^{\prime},q^{\prime}]\sqsubseteq[a,b]=\bigsqcup_{n}[a_{n},b_{n}]$. Then
$a=\sup_{n}a_{n}$ and $b=\inf_{n}b_{n}$. We claim that there must exist $n$
and $m$ so that $a_{n}\geq p$ and $b_{m}\leq q$. So assume that $a_{n}\leq p$
for all $n\in\mathbb{N}$. Then $p$ is an upper bound of $(a_{n})_{n}$ and
therefore $a\leq p$. Hence $a\leq p<p^{\prime}\leq a$, contradiction. The
proof of classical existence of $m$ is analogous. Hence there must exist
$N=\max\\{n,m\\}$ such that we have $p\leq a_{N}\leq b_{N}\leq q$, that is,
$[p,q]\sqsubseteq[a_{N},b_{N}]$. ∎

######  Lemma .

$\mathsf{I}\mathbb{Q}$ is a predomain base.

###### Proof.

Let $[p,q]\in\mathsf{I}\mathbb{Q}$ be given. Then $([p-2^{-n},q+2^{-n}])_{n}$
is a approximating sequence of $[p,q]$. ∎

######  Lemma .

Consistency on $\mathsf{I}\mathbb{Q}$ is continuous.

###### Proof.

Let $I$ be a finite set and let
$\alpha_{i}=\bigsqcup_{j}\alpha_{i,j}\in\mathsf{I}\mathbb{Q}$ for all $i\in
I$. Assume furthermore that $\\{\alpha_{i,j}\mid i\in I\\}$ is consistent for
all $j\in\mathbb{N}$, we show that $\\{\alpha_{i}\mid i\in I\\}$ is
consistent. The latter is the case if $\max\\{\underline{\alpha}_{i}\mid i\in
I\\}\leq\min\\{\overline{\alpha}_{i}\mid i\in I\\}$. We have, for all $i\in
J$, that $\max\\{\underline{\alpha}_{i,j}\mid i\in
I\\}\leq\min\\{\overline{\alpha}_{i,j}\mid i\in I\\}$ which implies the claim.
∎

######  Example .

Consistency is not automatically continuous. Consider for instance the
predomain base $B=\mathsf{I}\mathbb{Q}\setminus\\{[0,0]\\}$ and two sequences
$\alpha_{n}=[-1,2^{-n}]$ and $\beta_{n}=[-2^{-n},1]$. Then $\alpha_{n}$ and
$\beta_{n}$ are consistent for all $n\in\mathbb{N}$ but
$[-1,0]=\bigsqcup_{n}\alpha_{n}$ and $[0,1]=\bigsqcup_{n}\beta_{n}$ are not.

We collect some basic facts about posets and the way-below relation that are
used in the proof of our first technical result, the interpolation property
(Proposition 2 and Corollary 3). The majority of results are standard in
(classical) domain theory, see e.g. [AJ94], and we include them here both to
be self-contained and to demonstrate that they continue to hold in our
framework.

######  Lemma .

Let $(P,\sqsubseteq)$ be a poset for which $\sqsubseteq$ is decidable. Then
$b\sqsubseteq c$ whenever $b\ll c$. Moreover, $a\sqsubseteq b\ll c$ implies
that $a\ll c$, and similarly $a\ll b\sqsubseteq c$ implies that $a\ll c$, for
$a,b,c\in P$.

###### Proof.

For the first item, assume that $b\ll c$. As $c=\bigsqcup_{n}c$ there must
exist $n$ such that $b\sqsubseteq c$ whence $b\sqsubseteq c$.

Now suppose that $a\sqsubseteq b\ll c$. Let $c\sqsubseteq\bigsqcup_{n}c_{n}$.
Then there is $n$, weakly, such that $b\sqsubseteq c_{n}$ whence $a\sqsubseteq
c_{n}$, too. Now suppose that $a\ll b\sqsubseteq c$ and let
$c\sqsubseteq\bigsqcup_{n}c_{n}$. Then $b\sqsubseteq\bigsqcup_{n}c_{n}$ whence
there is $n$, weakly, such that $a\sqsubseteq c_{n}$. ∎

The proof of the above lemma uses that $\sqsubseteq$ is $\neg\neg$-closed
which follows from decidability.

######  Lemma .

Let $(P,\sqsubseteq)$ be a poset, $I$ be a finite set and
$b_{i},b_{i}^{\prime}\in P$ with $b_{i}\ll b_{i}^{\prime}$ for all $i\in I$.
If $s=\bigsqcup_{i}b_{i}$ and $s^{\prime}=\bigsqcup_{i}b_{i}^{\prime}$ then
$s\ll s^{\prime}$.

###### Proof.

Let $(x_{n})$ be a chain in P where
$s^{\prime}=\bigsqcup_{i}b_{i}^{\prime}\sqsubseteq\bigsqcup_{n}x_{n}$. Since
$\bigsqcup_{i}b_{i}^{\prime}$ is an upper bound of $\\{b_{i}^{\prime}\mid i\in
I\\}$, we have $b_{i}^{\prime}\sqsubseteq\bigsqcup_{n}x_{n}$ for all $i\in I$.
Moreover, by assumption $b_{i}\ll b_{i}^{\prime}$ for all $i\in I$, there must
exist $n_{i}$ such that $b_{i}\sqsubseteq x_{n_{i}}$. Now by setting
$n=\max\\{n_{i}\mid i\in I\\}$, then we have $b_{i}\sqsubseteq x_{n}$ for all
$i\in I$. Hence $\bigsqcup_{i}b_{i}\sqsubseteq x_{n}$ as $\bigsqcup_{i}b_{i}$
is the least upper bound. ∎

######  Corollary 1.

Let $(B,\sqsubseteq)$ be a bounded complete poset and $I$ a finite set. If
$b_{i},b_{i}^{\prime}\in B$ for $i\in I$ such that $b_{i}\ll b_{i}^{\prime}$
and $\\{b_{i}^{\prime}\mid i\in I\\}$ is consistent, then both
$\bigsqcup_{i}b_{i}$ and $\bigsqcup_{i}b_{i}^{\prime}$ exist in $B$ and
$\bigsqcup_{i}b_{i}\ll\bigsqcup_{i}b_{i}^{\prime}$.

######  Proof 2.1.

As $\\{b_{i}^{\prime}\mid i\in I\\}$ is consistent,
$\bigsqcup_{i}b_{i}^{\prime}$ exists in $B$, and there must exist an upper
bound $x\in B$ such that $b_{i}^{\prime}\sqsubseteq x$ for all $i\in I$.
Moreover, $b_{i}\sqsubseteq b_{i}^{\prime}\sqsubseteq x$ for all $i\in I$ as
$b_{i}\ll b_{i}^{\prime}$ hence $\\{b_{i}\mid i\in I\\}$ is also consistent
(with upper bound $x$), hence $\bigsqcup_{i}b_{i}$ exists in $B$, and the
claim follows from Lemma 2.

######  Lemma 2.2.

Let $(P,\sqsubseteq)$ be a poset and $(a_{n})_{n}$ and $(b_{n})_{n}$ chains in
$B$. If $s=(\bigsqcup_{n}a_{n})\bigsqcup(\bigsqcup_{n}b_{n})$ exists in $P$
and $s_{n}=a_{n}\bigsqcup b_{n}$ then $s=\bigsqcup_{n}s_{n}$.

######  Proof 2.3.

We first show that $s=a\bigsqcup b$ is an upper bound of $a_{n}\bigsqcup
b_{n}$ for all $n\in\mathbb{N}$. We have that $a_{n}\sqsubseteq a\sqsubseteq
a\bigsqcup b$ as $a$ is an upper bound of $a_{n}$ and $a\bigsqcup b$ is an
upper bound of $b$. Similarly $b_{n}\sqsubseteq a\bigsqcup b$. Hence
$a\bigsqcup b$ is an upper bound of $a_{n}\bigsqcup b_{n}$ and $a_{n}\bigsqcup
b_{n}\sqsubseteq a\bigsqcup b$ follows as $a_{n}\bigsqcup b_{n}$ is the least
upper bound.

Now we show that $a\bigsqcup b$ is indeed the least upper bound of
$a_{n}\bigsqcup b_{n}$. So take another upper bound $x$, that is,
$a_{n}\bigsqcup b_{n}\sqsubseteq x$ for all $n\in\mathbb{N}$. Then
$a_{n}\sqsubseteq a_{n}\bigsqcup b_{n}\sqsubseteq x$ and $b_{n}\sqsubseteq
a_{n}\bigsqcup b_{n}\sqsubseteq x$ for all $n\in\mathbb{N}$. Hence
$a=\bigsqcup_{n}a_{n}\sqsubseteq x$ and $b=\bigsqcup b_{n}\sqsubseteq x$. As
$a\bigsqcup b$ is the least upper bound of $a$ and $b$, it follows that
$a\bigsqcup b\sqsubseteq x$.

The above facts are used to prove our first result, the (weak) interpolation
property.

######  Proposition 2.

Let $(B,\sqsubseteq)$ be a bounded complete predomain base, and assume that
$\ll$ on $B$ is decidable. Then $B$ has the weak interpolation property, that
is, whenever $x\ll z$ for $x,z\in B$ there must exist $y\in B$ such that $x\ll
y\ll z$.

######  Proof 2.4.

We adapt the (classical) proof based on directed suprema ([AJ94, Lemma
2.2.15]) to our setting. Assume that $x\ll z$, and let $B=\\{b_{n}\mid
n\in\mathbb{N}\\}$.

As $z\in B$ and $B$ is a predomain base, we can find an element $b_{n}\in B$
with $b_{n}\ll z$ (e.g. the first element of an approximating sequence of
$z$). By the same reasoning, we can find $b_{m}\in B$ with $b_{m}\ll b_{n}$.
Let $o=\max\\{n,m\\}$ and consider the sequence

$c_{n}=\bigsqcup\\{b_{i}\mid 0\leq i\leq o+n,\exists 0\leq j\leq
o+n.\,b_{i}\ll b_{j}\ll z\\}.$

Then $c_{n}$ is well-defined, as suprema are taken over a non-empty, bounded
(by $z$) and finite set.

We now claim that $\bigsqcup_{n}c_{n}=z$. First, it is clear that
$c_{n}\sqsubseteq z$ for all $n\in\mathbb{N}$. To see that $z$ is a least
upper bound of the $c_{n}$, suppose that $c_{n}\sqsubseteq u$ for all
$n\in\mathbb{N}$, and we show that $z\sqsubseteq u$. Let $(z_{n})_{n}$ be an
approximating sequence for $z$. As $z=\bigsqcup_{n}z_{n}$, it suffices to show
that $z_{n}\sqsubseteq u$ for all $n\in\mathbb{N}$. So let $n\in\mathbb{N}$.
As $z_{n}\in B$, there exists an approximating sequence $(z_{n}^{k})_{k}$ for
$z$, and in particular $z_{n}^{k}\ll z_{n}\ll z$ for all $k\in\mathbb{N}$. Now
fix an arbitrary $k\in\mathbb{N}$, we show that $z_{n}^{k}\sqsubseteq u$. As
$B$ is countable, we can find $p,q\in\mathbb{N}$ such that $z_{n}=b_{p}$ and
$z_{n}^{k}=b_{q}$. Let $r=\max\\{p,q\\}$. Then $b_{q}=z_{n}^{k}\ll
z_{n}=b_{p}\ll z$ and therefore $b_{q}\sqsubseteq c_{r}$ as $p,q\leq r\leq
r+o$. As $c_{r}\sqsubseteq u$ we have that $z_{n}^{k}=b_{q}\sqsubseteq u$. As
$k$ was arbitrary, this implies that $z_{n}=\bigsqcup_{k}z_{n}^{k}\sqsubseteq
u$. By the same argument, as $n$ was arbitrary and $z=\bigsqcup_{n}z_{n}$, we
may conclude that $z\sqsubseteq u$, thus establishing the claim.

We now have that $x\ll z=\bigsqcup_{n}c_{n}$. Therefore, there weakly exists
$n\in\mathbb{N}$ such that $x\sqsubseteq c_{n}$. Let
$c_{n}=\bigsqcup\\{b_{i}\mid i\in I\\}$ where $I\subseteq\\{0,\dots,o+n\\}$ is
a finite, non-empty set. For each $i\in I$ we can moreover find
$b^{\prime}_{i}\in\\{b_{0},\dots,b_{n+o}\\}$ with $b_{i}\ll b_{i}^{\prime}\ll
z$.

By Lemma 2 we have that $x\sqsubseteq\bigsqcup\\{b_{i}\mid i\in
I\\}\ll\bigsqcup\\{b_{i}^{\prime}\mid i\in I\\}\ll z$. Therefore
$y=\bigsqcup\\{b_{i}^{\prime}\mid i\in I\\}$ is our desired interpolant. This
(only) shows weak existence of an interpolant, due to the weak existence of
the number $n$ used in its construction.

######  Corollary 3.

Let $(B,\sqsubseteq)$ be a bounded complete predomain base for which $\ll$ is
decidable. If $b_{1},\dots,b_{n}\in B$ and $b_{i}\ll c$ for all $i=1,\dots,n$
then there must exist an interpolant $b\in B$ such that $b_{i}\ll b\ll c$ for
all $1\leq i\leq n$.

######  Proof 2.5.

By the previous lemma, we can find interpolants $\hat{b}_{i}$ for each $1\leq
i\leq n$ such that $b_{i}\ll\hat{b}_{i}\ll c$. By Lemma 2 we have that
$b=\bigsqcup\\{\hat{b}_{i}\mid 1\leq i\leq n\\}$ satisfies $b\ll c$ and
moreover $b_{i}\ll\hat{b}_{i}\sqsubseteq b$ so that $b_{i}\ll b$ for all
$1\leq i\leq n$.

We conclude the section with a technical lemma on swapping the order of
suprema that we will use later.

######  Lemma 2.6.

Suppose that $P$ is a poset and $f:\mathbb{N}\times\mathbb{N}\to P$ is
monotonic, i.e. $n\leq n^{\prime}$ and $k\leq k^{\prime}$ implies
$f(n,k)\sqsubseteq f(n^{\prime},k^{\prime})$. Then

  1. (1)

the sequence $(f(n,m))_{n}$ is monotonic for all $m\in\mathbb{N}$

  2. (2)

if $\bigsqcup_{n}f(n,m)$ exists for all $m\in\mathbb{N}$, then
$(\bigsqcup_{n}f(n,m))_{m}$ is monotonic

  3. (3)

if both $\bigsqcup_{n}f(n,n)$ and $\bigsqcup_{m}\bigsqcup_{n}f(n,m)$ both
exist, they are equal.

######  Proof 2.7.

The first item is immediate by monotonicity of $f$. For the second item, fix
$m\in\mathbb{N}$. We show that
$\bigsqcup_{n}f(n,m)\sqsubseteq\bigsqcup_{n}f(n,m+1)$. This is immediate as
$\bigsqcup_{n}f(n,m+1)$ is an upper bound of $f(n,m)$ for all
$n\in\mathbb{N}$.

For the last item, suppose that $\bigsqcup_{n}f(n,n)$ and
$\bigsqcup_{m}\bigsqcup_{n}f(n,m)$ both exist, in particular this entails that
$\bigsqcup_{n}f(n,m)$ exists for all $m\in\mathbb{N}$. We first show that
$\bigsqcup_{n}f(n,n)$ is an upper bound of all $\bigsqcup_{n}f(n,m)$ for all
$n\in\mathbb{N}$. By monotonicity, we have that
$\bigsqcup_{n}f(n,m)=\bigsqcup_{n\geq m}f(n,m)\sqsubseteq\bigsqcup_{n\geq
m}f(n,n)=\bigsqcup_{n}f(n,n)$. To finish the proof, we need to show that
$\bigsqcup_{n}f(n,n)$ is the least upper bound of $\bigsqcup_{n}f(n,m)$ for
all $m\in\mathbb{N}$. So let $c$ be a competitor, i.e.
$\bigsqcup_{n}f(n,m)\sqsubseteq c$ for all $m\in\mathbb{N}$. We show that
$\bigsqcup_{n}f(n,n)\sqsubseteq c$. This follows once we establish that
$f(n,n)\sqsubseteq c$ for all $n\in\mathbb{N}$ as $\bigsqcup_{n}f(n,n)$ is the
least upper bound of all $f(n,n)$. So let $n\in\mathbb{N}$. But this is
evident as $f(n,n)\sqsubseteq\bigsqcup_{k}f(k,n)\sqsubseteq c$ by assumption.

######  Corollary 4.

Let $P$ be a poset that has suprema of all increasing chains, and let
$f:\mathbb{N}\times\mathbb{N}\to P$ be monotone. Then both
$\bigsqcup_{n}f(n,n)$ and $\bigsqcup_{m}\bigsqcup_{n}f(n,m)$ exist and are
equal.

##  3\. Completion of Predomain Bases

We give a direct description of the rounded ideal completion of [BK09] with
ideals being represented by chains. The rounded ideal (or continuous)
completion is distinguished from the ideal completion by the definition of the
order $\sqsubseteq$ on the completion in terms of approximation $\ll$ on the
underlying predomain base, rather than in terms of its order.

######  Definition 5 (Continuous Completion).

Let $(B,\sqsubseteq)$ be a predomain base. The _continuous completion_ of $B$
is the set $\hat{B}=\\{(b_{n})_{n}\mid b_{n}\in B,b_{n}\sqsubseteq
b_{n+1}\mbox{ for all }n\in\mathbb{N}\\}$ of increasing sequences in $B$, with
order relation defined by

$(b_{n})\sqsubseteq(b^{\prime}_{n})\mbox{ iff }\forall b\in B.\,\forall
n\in\mathbb{N}.\,b\ll b_{n}\to\tilde{\exists}m\in\mathbb{N}.\,b\ll
b^{\prime}_{m}$

for increasing sequences $(b_{n})_{n}$ and $(b^{\prime}_{n})_{n}$ in $B$.

The function $i:B\to\hat{B}$ that maps $b\in B$ to the constant sequence
$(b)_{n}$ is called the _canonical embedding_ , and in the sequel we identify
elements in $B$ with their canonical embedding.

We show in Lemma 3.10 that the canonical embedding indeed preserves both
$\sqsubseteq$ and $\ll$ which justifies our terminology. The above definition
of the order $\sqsubseteq$ on the completion of a predomain base showcases the
first instance of our “constructive existence – classical correctness”
approach in the classical definition of the order relation on the completion
above. In particular, this implies that a realiser of
$(b_{n})\sqsubseteq(b^{\prime}_{n})_{n}$ carries no computational content. It
is straightforward to see that the order relation $\sqsubseteq$ defined above
is in fact a preorder. We omit the straightforward proof of this fact.

######  Lemma 3.1.

The order relation $\sqsubseteq$ on the continuous completion $\hat{B}$ of a
predomain base $B$ is a preorder.

The preorder $\sqsubseteq$ on the continuous completion $\hat{B}$ of a
predomain base induces an equality relation on $\hat{B}$ where $b=b^{\prime}$
iff $b\sqsubseteq b^{\prime}$ and $b^{\prime}\sqsubseteq b$. In particular,
this gives $(\hat{B},\sqsubseteq)$ the structure of a poset, where arbitrary
suprema, if they exist, are unique up to equality, i.e. $s=\bigsqcup_{i}a_{i}$
and $s^{\prime}=\bigsqcup_{i}a_{i}$ implies $s=s^{\prime}$. Moreover, suprema
are extensional: if $c_{i}=d_{i}$ for all $i\in I$ and $s=\bigsqcup_{i}c_{i}$,
$t=\bigsqcup_{i}d_{i}$ then $s=t$.

It is an easy but very useful observation that every element of the continuous
completion is equal to the supremum of the elements of (the canonical
embeddings of) its representing sequence.

######  Lemma 3.2.

Let $B$ be a predomain base and $x=(x_{n})_{n}\in\hat{B}$. Then
$x=\bigsqcup_{n}x_{n}$.

######  Proof 3.3.

First, $x$ is an upper bound of all $x_{n}$. To see this, let $n\in\mathbb{N}$
and $a\in B$ with $a\ll x_{n}$. We have to show that there must exist some
$k\in\mathbb{N}$ with $a\ll x_{k}$. But this clearly holds for $k=n$. To see
that $x$ is the least upper bound of all $x_{n}$, consider a competing upper
bound $c=(c_{n})_{n}\in\hat{B}$ with $x_{n}\sqsubseteq c$ for all
$n\in\mathbb{N}$. To see that $x\sqsubseteq c$, let $n\in\mathbb{N}$, $a\in B$
with $a\ll x_{n}$. As $x_{n}\sqsubseteq c$ there must exist $k\in\mathbb{N}$
such that $a\ll c_{k}$ which is precisely what we need to show for
$x\sqsubseteq c$.

We now show that the continuous completion $\hat{B}$ of a predomain base $B$
has suprema of all increasing chains. Below, we write $M\ll z$ if $x\ll z$ for
all $x\in M$ and say that a predomain base $B$ _has weak interpolation_ if
there weakly exists $y$ such that $M\ll y\ll z$ whenever $M$ is finite and
$M\ll z$.

######  Lemma 3.4.

Let $B=\\{b_{n}\mid n\in\mathbb{N}\\}$ be a predomain base and
$(b_{n}^{k})_{k}$ an approximating sequence of $b_{n}$. If $(c_{n})_{n}$ is an
increasing sequence in $\hat{B}$ and $c_{n}=(c_{n,m})_{m}$, then the following
statements hold:

  1. (1)

The set $D_{k}=\\{c_{n,m}^{k}\mid 0\leq n,m\leq k\\}$ is consistent. If
consistency is continuous, the same applies to the set
$\hat{D}_{k}=\\{c_{n,k}\mid 0\leq n\leq k\\}$.

  2. (2)

The sequence $(d_{k})_{k}=(\bigsqcup D_{k})_{k}$ is increasing. If consistency
is continuous, the same applies to the sequence
$(\hat{d}_{k})_{n}=(\bigsqcup\hat{D}_{k})_{k}$.

  3. (3)

If $B$ has weak interpolation, we have $c_{n}\sqsubseteq d$ for all
$n\in\mathbb{N}$. If consistency on $B$ is moreover continuous, also
$c_{n}\sqsubseteq\hat{d}$ for all $n\in\mathbb{N}$.

  4. (4)

If $c_{n}\sqsubseteq u$ for all $n\in\mathbb{N}$, then $d\sqsubseteq u$. If
consistency on $B$ is continuous, then also $\hat{d}\sqsubseteq u$.

######  Proof 3.5.

For the first item, fix $k\in\mathbb{N}$ and let $0\leq n,m\leq k$. As
$(c_{n,m}^{i})_{i}$ is an approximating sequence of $(c_{n,m})$ we have
$c_{n,m}^{k}\ll c_{n,m}$. As $c_{n}\sqsubseteq c_{k}$, there must exist
$r=r(n,m)$ such that $c_{n,m}^{k}\ll c_{k,r}$. Let $s=\max\\{r(n,m)\mid 0\leq
n,m\leq k\\}$. Then $c_{n,m}^{k}\ll c_{k,r}\sqsubseteq c_{k,s}$ so that
$c_{k,s}$ is an upper bound of $D_{k}$.

Now assume that consistency is continuous. Then consistency of $\hat{D}_{k}$
follows if the sets $\hat{D}_{k,i}=\\{c_{n,k}^{i}\mid 0\leq n\leq k\\}$ are
consistent for all $i\in\mathbb{N}$. Let $i\in\mathbb{N}$ and
$r=\max\\{i,k\\}$. By what we have just demonstrated, there must exist an
upper bound $b$ of the set $D_{r}$. We show that $b$ is an upper bound of
$\hat{D}_{k,i}$. This follows since for $c_{k,n}^{i}\in\hat{D}_{k,i}$ we have
that $c_{k,n}^{i}\sqsubseteq c_{k,n}^{r}\in D_{r}$ and the fact that $b$ is an
upper bound of $D_{r}$.

The second item, monotonicity of $(d_{k})_{k}$ and $(\hat{d}_{k})_{k}$ is
clear since both $D_{k}\subseteq D_{k+1}$ and
$\hat{D}_{k}\subseteq\hat{D}_{k+1}$.

For the third item, we begin by showing that $c_{n}\sqsubseteq d$. So fix
$m\in\mathbb{N}$ and suppose that $x\ll c_{n,m}$, we show that there must
exist $k\in\mathbb{N}$ such that $x\ll d_{k}$. As
$c_{n,m}=\bigsqcup_{k}c_{n,m}^{k}$ there must exist $k\in\mathbb{N}$ such that
$x\ll c_{n,m}^{k}$. The same relation holds if we replace $k$ by
$k^{\prime}=\max\\{n,m,k\\}$ so we assume that $k\geq n,m$ without loss of
generality. Then $x\ll c_{n,m}^{k}\sqsubseteq\bigsqcup\\{c_{n,m}^{k}\mid 0\leq
n,m\leq k\\}=d_{k}$ as required. Now assume that consistency is continuous. To
see that $c_{n}\sqsubseteq\hat{d}$, fix $m\in\mathbb{N}$, $x\in B$ and assume
that $x\ll c_{n,m}$. We show that there must exist $k\in\mathbb{N}$ such that
$x\ll d_{k}$. This holds, for example, if $k=\max\\{n,m\\}$ for then $x\ll
c_{n,m}\sqsubseteq c_{n,k}\sqsubseteq\bigsqcup\\{c_{n,k}\mid 0\leq n\leq
k\\}=\hat{d}_{k}$.

For the last item, assume that $u=(u_{i})_{i}\in\hat{B}$ and $c_{n}\sqsubseteq
u$ for all $n\in\mathbb{N}$. We first show that $d\sqsubseteq u$. To see this,
fix $k\in\mathbb{N}$, $x\in B$ and assume that $x\ll d_{k}$. We show that
there must exist $s\in\mathbb{N}$ such that $x\ll u_{s}$. By assumption, we
have $x\ll d_{k}=\bigsqcup\\{c_{n,m}^{k}\mid 0\leq n,m\leq k\\}$. Fix $0\leq
n,m\leq k$. Since $c_{n,m}^{k}\ll c_{n,m}$ and $c_{n}\sqsubseteq u$, there
must exist $r=r(n,m)\in\mathbb{N}$ such that $c_{n,m}^{k}\ll u_{r}$. If
$s=\max\\{r(n,m)\mid 0\leq n,m\leq k\\}$, we have $c_{n,m}^{k}\ll u_{s}$ for
all $0\leq n,m\leq k$. Hence, by Corollary 1 we obtain
$d_{k}=\bigsqcup\\{c_{n,m}^{k}\mid 0\leq n,m\leq k\\}\ll u_{s}$ as required.
Now suppose that consistency is continuous. To see that $\hat{d}\sqsubseteq
u$, fix $k\in\mathbb{N}$ and $x\in B$ such that
$x\ll\hat{d}_{k}=\bigsqcup\\{c_{n,k}\mid 0\leq n\leq k\\}$. We show that there
must exist $s\in\mathbb{N}$ such that (as above) $x\ll u_{s}$. Fix $0\leq
n\leq k$. As $x\ll\hat{d}_{k}=\bigsqcup_{0\leq k\leq
n}\bigsqcup_{i}c_{n,k}^{i}=\bigsqcup_{i}\bigsqcup_{0\leq n\leq k}c_{n,k}^{i}$
there must exist $i\in\mathbb{N}$ such that $x\sqsubseteq\bigsqcup_{0\leq
n\leq k}c_{n,k}^{i}$. For this $i\in\mathbb{N}$, we moreover have that
$c_{n,k}^{i}\ll c_{n,k}$ so that there must exist $r=r(n,k,i)$ for which
$c_{n,k}^{i}\ll u_{r}$ since $c_{n}\sqsubseteq u$. Hence for
$s=\max\\{r(n,k,i)\mid 0\leq n\leq k\\}$ we have that $c_{n,k}^{i}\ll u_{s}$
so that $\bigsqcup_{0\leq k\leq n}c_{n,k}^{i}\ll u_{s}$ by Corollary 1, and
finally $x\sqsubseteq\bigsqcup_{0\leq k\leq n}c_{n,k}^{i}\ll u_{s}$ as
desired.

The last lemma finally puts us into a position to show that the completion of
a predomain base is in fact complete.

######  Corollary 6.

Let $(B,\sqsubseteq)$ be a bounded complete predomain base. Then
$(\hat{B},\sqsubseteq)$ has suprema of all increasing chains.

######  Proof 3.6.

For bounded complete predomain bases, we have established the weak
interpolation property in Corollary 3. The claim follows from Lemma 3.4.

We have the following extension theorem.

######  Proposition 7.

Suppose that $B$ and $C$ are predomain bases for which consistency is
continuous, and suppose that $C$ has weak interpolation. Then every Scott
continuous map $f:B\to\hat{C}$ has a Scott continuous extension
$\hat{f}:\hat{B}\to\hat{C}$.

######  Proof 3.7.

Let $(x^{i})_{i}$ be an approximating sequence for each element $x\in B$.
Define $\hat{f}((b_{n})_{n})=(f(b_{n}))_{n}$ for a monotone sequence
$(b_{n})_{n}\in\hat{B}$. Then $\hat{f}((b_{n})_{n})$ is monotone as $f$ is
monotone. We show that $\hat{f}$ is Scott continuous. For this we fix an
increasing sequence $(b_{n})_{n}\in\hat{B}$ where $b_{n}=(b_{n,m})_{m}$ and
use Lemma 3.4 to establish that

$A_{k}=[\hat{f}(\bigsqcup_{n}b_{n})]_{k}=[\hat{f}(\bigsqcup_{n\leq
k}(b_{n,k})_{k})]_{k}=f(\bigsqcup_{n\leq k}b_{n,k})$

for the $k$-th element $[\cdot]_{k}$ of $\hat{f}(\bigsqcup_{n}b_{n})$ using
that consistency on $C$ is continuous. For the $k$-th element of
$\bigsqcup_{n}\hat{f}(b_{n})$ we similarly obtain

$B_{k}=[\bigsqcup_{n}\hat{f}(b_{n})]_{k}=[\bigsqcup_{n}(f((b_{n,k})_{k})]_{k}=\bigsqcup_{n\leq
k}f(b_{n,k})$

also using Lemma 3.4 and continuity of consistencey on $B$. For the claim, we
need to establish $(A_{k})_{k}=(B_{k})_{k}$. To see that
$(A_{k})_{k}\sqsubseteq(B_{k})_{k}$ fix $k\in\mathbb{N}$ and $x\in C$ such
that $x\ll A_{k}=f(\bigsqcup_{n\leq k}b_{n,k})$. We show that there must exist
$l\in\mathbb{N}$ such that $x\ll B_{l}=\bigsqcup_{n\leq l}f(b_{n,l})$. As $C$
has weak interpolation, there must exist $y\in C$ such that $x\ll y\ll
f(\bigsqcup_{n\leq k}b_{n,k})$. Therefore

$y\ll f(\bigsqcup_{n\leq
k}\bigsqcup_{i\in\mathbb{N}}b_{n,k}^{i})=f(\bigsqcup_{i}\bigsqcup_{n\leq
k}b_{n,k}^{i})=\bigsqcup_{i}f(\bigsqcup_{n\leq k}b_{n,k}^{i})$

using continuity of $f$. Therefore there must exist $i\in\mathbb{N}$ such that
$x\ll y\sqsubseteq f(\bigsqcup_{n\leq k}b_{n,k}^{i})$. As $b_{n}\sqsubseteq
b_{k}$ for $n\leq k$ and $b_{n,k}^{i}\ll b_{n,k}$ there must exist $j(n)$ such
that $b_{n,k}^{i}\ll b_{k,j(n)}$. Let $j=\max\\{j(n)\mid 0\leq n\leq k\\}$.
Then $x\ll f(\bigsqcup_{n\leq k}b_{n,k}^{i})\sqsubseteq f(b_{k,j})$. For
$l=\max\\{j,k\\}$ we therefore obtain that $x\ll
f(b_{k,j})\sqsubseteq\bigsqcup_{n\leq l}f(b_{n,l})=B_{l}$. For the reverse
direction $(B_{k})_{k}\sqsubseteq(A_{k})_{k}$ fix $k\in\mathbb{N}$ and $x\in
C$ such that $x\ll B_{k}=\bigsqcup_{n\leq k}f(b_{n,k})$. We show that there
must exist $l\in\mathbb{N}$ such that $x\ll f(\bigsqcup_{n\leq l}b_{n,l})$.
But this is evident for $l=k$ as $f(b_{n,k})\sqsubseteq f(\bigsqcup_{n\leq
k}b_{n,k})$ by monotonicity of $f$, for all $0\leq k\leq n$, whence
$x\ll\bigsqcup_{n\leq k}f(b_{n,k})\sqsubseteq f(\bigsqcup_{n\leq k}b_{n,k})$.

We now show that bounded completeness (Definition 2) transfers from a
predomain base to its completion.

######  Lemma 3.8.

Let $(B,\sqsubseteq)$ be a bounded complete predomain base and suppose that
consistency on $B$ is continuous. Let $I\subseteq\hat{B}$ be finite and
consistent.

  1. (1)

$I_{n}=\\{x_{n}\mid(x_{n})_{n}\in I\\}$ is consistent for all
$n\in\mathbb{N}$.

  2. (2)

$\bigsqcup I=(\bigsqcup I_{n})_{n}$

i.e. the completion of a bounded complete predomain base is bounded complete,
and finite suprema of consistent sets are calculated pointwise.

######  Proof 3.9.

For the first item, let $b=(b_{n})_{n}$ be an upper bound of $I$, and let
$(x^{i})_{i}$ be an approximating sequence of $x\in B$. As consistency on $B$
is continuous, it suffices to show that $\\{x_{n}^{i}\mid(x_{n})_{n}\in I\\}$
is continuous for all $n,i\in\mathbb{N}$. So let $i,n\in\mathbb{N}$. For
$x=(x_{n})_{n}\in I$, as $x_{n}^{i}\ll x_{n}$ and $(x_{n})_{n}\sqsubseteq b$,
there must exist $k(x)$ such that $x_{n}^{i}\ll b_{k(x)}$. Let
$k=\max\\{k(x)\mid x\in I\\}$. Then $b_{k}$ is an upper bound of
$\\{x_{n}^{i}\mid(x_{n})_{n}\in I\\}$.

For the second item, note that $\bigsqcup I_{n}\in B$ exists since $I_{n}$ is
consistent and $(\bigsqcup I_{n})_{n}$ is monotone as all $x\in I$ are
monotone so that $(\bigsqcup I_{n})_{n}\in\hat{B}$. We first show that
$(\bigsqcup I_{n})_{n}$ is an upper bound of all $x\in I$. So let $x\in I$,
$n\in\mathbb{N}$ and assume that $z\in B$ with $z\ll x_{n}$. Then $z\ll\sqcup
I_{n}$ whence $x\sqsubseteq(\sqcup I_{n})_{n}$ by definition of $\sqsubseteq$
on $\hat{B}$. We now show that $(\bigsqcup I_{n})_{n}$ is the least upper
bound of $I$. So assume that $x\sqsubseteq b$ for all $x\in I$. We show that
$(\bigsqcup I_{n})_{n}\sqsubseteq b$. So let $n\in\mathbb{N}$, $z\in B$ with
$z\ll\bigsqcup I_{n}$. We show that there must exist $k\in\mathbb{N}$ with
$z\ll b_{k}$. As $\bigsqcup
I_{n}=\bigsqcup\\{\bigsqcup_{i}x_{n}^{i}\mid(x_{n})_{n}\in
I\\}=\bigsqcup_{i}\bigsqcup\\{x_{n}^{i}\mid(x_{n})_{n}\in I\\}$ (using Lemma
2.2) and $z\ll\bigsqcup I_{n}$, there must exist $l\in\mathbb{N}$ such that
$z\sqsubseteq\bigsqcup\\{x_{n}^{k}\mid(x_{n})_{n}\in I\\}$. For
$x=(x_{n})_{n}\in I$ we moreover have that $x_{n}^{k}\ll x_{n}$, and since
$x\sqsubseteq b$ there must exist $l(x)\in\mathbb{N}$ such that $x_{n}^{i}\ll
b_{l(x)}$. Let $l=\max\\{l(x)\mid x\in I\\}$. Then
$z\sqsubseteq\bigsqcup\\{x_{n}^{k}\mid(x_{n})_{n}\in I\\}\ll b_{l}$ by Lemma
2.

We conclude the section with properties of the canonical embedding that have
already been reported in [BK09], albeit in a slight different setting.

######  Lemma 3.10.

Let $B$ be a bounded complete predomain base. Then the embedding
$B\hookrightarrow\hat{B}$ preserves and reflects $\sqsubseteq$ and preserves
$\ll$.

######  Proof 3.11.

It is clear that the embedding preserves and reflects the order $\sqsubseteq$.
To see that it preserves $\ll$, assume that $b,c\in B$ with $b\ll c$ in $B$.
We show that $b\ll c$ in $\hat{B}$ where we identify $b$ and $c$ with the
constant sequences $(b)_{n}$ and $(c)_{n}$.

To see that $b\ll c$ in $\hat{B}$, let $(x_{n})_{n}$ be a chain in $\hat{B}$
with $c\sqsubseteq\bigsqcup_{n}x_{n}$. Let $x_{n}=(x_{n,m})_{m}$ and choose an
approximating sequence $(a^{n})_{n}$ for every element $a\in B$. As
$\bigsqcup_{n}x_{n}=(\bigsqcup\\{x_{n,m}^{k}\mid 0\leq n,m\leq k\\})_{k}$ by
Lemma 3.4 and $b\ll c$, there must exist $k\in\mathbb{N}$ such that
$b\sqsubseteq\bigsqcup\\{x_{n,m}^{k}\mid 0\leq k\leq n\\}$ in $B$ and hence
also in $\hat{B}$. For $0\leq n,m\leq k$ we have $x_{n,m}^{k}\sqsubseteq
x_{n,m}\sqsubseteq x_{n}\sqsubseteq x_{k}$ and so $b\sqsubseteq x_{k}$ as
required.

##  4\. The Scott topology

We investigate the Scott topology on the completion of a predomain base. We
show that every topologically continuous function is Scott continuous, and
that the Scott topologgy is generated by the way-below relation. These results
are also used later in the function space construction. In particular, we
employ a classical definition of the Scott topology to align open sets with
the way-below relation.

######  Definition 8 (Basic Notions).

Let $(P,\sqsubseteq)$ be a poset. A subset $\mathcal{O}\subseteq P$ is _Scott-
open_ if it is an upper set ($\forall x,y\in P.\,x\sqsubseteq y\land x\in P\to
y\in P$) and inaccessible by suprema of increasing chains (if
$\bigsqcup_{n}x_{n}\in O$ for an increasing chain $(x_{n})_{n}$ then there
must exist $k\in\mathbb{N}$ such that $x_{k}\in\mathcal{O}$).

######  Lemma 4.1.

Let $B$ be a bounded complete predomain base. Then
$b\twoheaduparrow=\\{x\in\hat{B}\mid b\ll x\\}$ is Scott-open for all
$b\in\hat{B}$.

######  Proof 4.2.

To see that $b\twoheaduparrow$ is an upper set, assume that $x,y\in\hat{B}$
with $x\sqsubseteq y$ and let $x\in b\twoheaduparrow$, i.e. $b\ll x$. Then
$b\ll x\sqsubseteq y$ so that $b\ll y$ by Lemma 2. To see that
$b\twoheaduparrow$ is inacessible by suprema increasing chain increasing
chainss, assume that $\bigsqcup_{n}x_{n}\in b\twoheaduparrow$, i.e.
$b\ll\bigsqcup_{n}x_{n}$. By definition of $\ll$, there must exist
$n\in\mathbb{N}$ such that $b\ll x_{n}$, hence $x_{n}\in b\twoheaduparrow$.

######  Lemma 4.3.

Let $B$ be a bounded complete predomain base, $x\in\hat{B}$ and
$\mathcal{O}\subseteq\hat{B}$ be Scott-open with $x\in\mathcal{O}$. Then there
must exist $b\in B\cap\mathcal{O}$ such that $x\in
b\twoheaduparrow\subseteq\mathcal{O}$.

######  Proof 4.4.

Choose an approximating sequence $(a^{n})_{n}$ for every $a\in B$ and let
$x=(x_{n})_{n}$. Then $x=\bigsqcup_{n}x_{n}$ by Lemma 3.2 and
$x_{n}=\bigsqcup_{m}x_{n}^{m}$ by assumption so that
$x=\bigsqcup_{n}x_{n}=\bigsqcup_{n}\bigsqcup_{m}x_{n}^{m}=\bigsqcup_{n}\bigsqcup_{m}(\bigsqcup_{i\leq
n}x_{i}^{m})=\bigsqcup_{n}\bigsqcup_{i\leq n}x_{i}^{n}$ by Corollary 4. As
$\mathcal{O}$ is Scott-open, there must exist $n\in\mathbb{N}$ such that
$\bigsqcup_{i\leq n}x_{i}^{n}\in\mathcal{O}$. For $i\leq n$, we have
$x_{i}^{n}\ll x_{i}\sqsubseteq x_{n}$ so that $\bigsqcup_{i\leq n}x_{i}^{n}\ll
x_{n}$ and therefore $\bigsqcup_{i\leq n}x_{i}^{n}\ll x$ by Lemma 2. As $B$ is
bounded complete, we have $b=\bigsqcup_{i\leq n}x_{i}^{n}\in B$ so that $b\in
B\cap\mathcal{O}$. As $\mathcal{O}$ is an upper set, it follows that
$b\twoheaduparrow\subseteq\mathcal{O}$.

######  Remark 4.5.

Taken together, the last two lemmas show that the Scott topology on $\hat{B}$
is generated by sets of the form $b\twoheaduparrow$ for $b\in B$.

The following lemma shows that Scott continuity, as defined in Definition 2 as
preservation of suprema of increasing chains, is also constructively
equivalent to preservation of open sets under inverse image.

######  Lemma 4.6.

Let $B$ and $C$ be bounded complete predomain bases and $f:\hat{B}\to\hat{C}$
be Scott-continous. Then $f^{-1}(\mathcal{O})$ is open whenever
$\mathcal{O}\subseteq\hat{C}$ is open.

######  Proof 4.7.

Let $\mathcal{O}\subseteq\hat{C}$ be Scott-open. We show that
$f^{-1}(\mathcal{O})$ is an upper set. So let $x\sqsubseteq y\in\hat{B}$ with
$x\in f^{-1}(\mathcal{O})$, i.e. $f(x)\in\mathcal{O}$. By monotonicity of $f$,
we have $f(x)\sqsubseteq f(y)$ and as $\mathcal{O}$ is an upper set, we have
$f(y)\in\mathcal{O}$, i.e. $y\in f^{-1}(\mathcal{O})$. We now show that
$f^{-1}$ is inaccessible by suprema of increasing chains. So let
$\bigsqcup_{n}x_{n}\in f^{-1}(\mathcal{O})$. Then
$\bigsqcup_{n}f(x_{n})=f(\bigsqcup_{n}x_{n})\in\mathcal{O}$ and since
$\mathcal{O}$ is inaccessible by directed suprema, there must exist
$n\in\mathbb{N}$ such that $f(x_{n})\in\mathcal{O}$ whence $x_{n}\in
f^{-1}(\mathcal{O})$.

We need the following technical result before we can prove the converse of the
above lemma.

######  Lemma 4.8.

Let $B$ be a bounded complete predomain base with decidable $\ll$ and choose
an approximating sequence $(b^{i})_{i}$ for all $b\in B$. Furthermore, let
$x=(x_{n})_{n}\in\hat{B}$ and $y=(y_{n})_{n}=(\bigsqcup_{i\leq
n}x_{i}^{n})_{n}$. Then y is well defined (i.e. $\\{x_{i}^{n}\mid i\leq n\\}$
is consistent) for all $n\in\mathbb{N}$ and $x=y$.

######  Proof 4.9.

It is evident that $\\{x_{i}^{n}\mid 0\leq i\leq n\\}$ is consistent for all
$n\in\mathbb{N}$, as for $0\leq i\leq n$ we have that $x_{i}^{n}\sqsubseteq
x_{i}\sqsubseteq x_{n}$, hence $x_{n}$ is the required upper bound.

To see that $x\sqsubseteq y$ let $n\in\mathbb{N}$ and $b\in B$ with $b\ll
x_{n}$. We show that there must exist $k\in\mathbb{N}$ with $b\ll y_{k}$.
First, by interpolation, there must exist $c\in B$ such that $b\ll c\ll
x_{n}$. As $(x_{n}^{i})_{i}$ is an approximating sequence, there must exist
$i\in\mathbb{N}$ such that $b\ll c\sqsubseteq x_{n}^{i}$, hence $b\ll
x_{n}^{i}$. Let $k=\max\\{i,n\\}$. Then $b\sqsubseteq x_{n}^{i}\sqsubseteq
x_{n}^{k}\sqsubseteq\bigsqcup_{i\leq k}x_{n}^{k}=y_{k}$.

To see that $y\sqsubseteq x$, let $b\in\mathbb{N}$ and $b\ll y_{n}$. Put
$k=n$. Then $b\ll y_{n}=\bigsqcup_{i\leq
n}x_{i}^{n}\sqsubseteq\bigsqcup_{i\leq n}x_{i}\sqsubseteq x_{n}=x_{k}$.

######  Lemma 4.10.

Let $f:\hat{B}\to\hat{C}$ be a function between bounded complete predomain
bases where $\ll$ is decidable on $C$ such that $f^{-1}(\mathcal{O})$ is open
for all open $\mathcal{O}\subseteq\hat{C}$. Then $f$ is Scott continuous.

######  Proof 4.11.

We first show that $f$ is monotone. So let $x\sqsubseteq y\in\hat{B}$. To see
that $f(x)\sqsubseteq f(y)$ let $n\in\mathbb{N}$, $c\in C$ and suppose that
$c\ll f(x)_{n}$. We show that there must exist $k$ such that $c\ll f(y)_{k}$.
Since $c\ll f(x)_{n}\sqsubseteq f(x)$ we have that $f(x)\in c\twoheaduparrow$
so that $x\in f^{-1}(c\twoheaduparrow)$ which is open and therefore an upper
set. As $x\sqsubseteq y$, we have $y\in f^{-1}(c\twoheaduparrow)$ so that
$c\ll f(y)$. If $(f(y)_{n}^{i})_{i}$ is an approximating sequence of
$f(y)_{n}$, Lemma 4.8 gives $c\ll\bigsqcup_{n}\bigsqcup_{i\leq
n}f(y)_{i}^{n}$. Therefore there must exist $k$ such that
$c\sqsubseteq\bigsqcup_{i\leq k}f(y)_{i}^{k}$. We have, for $i\leq k$, that
$f(y)_{i}^{k}\ll f(y)_{i}\sqsubseteq f(y)_{k}$ so that $\bigsqcup_{i\leq
k}f(y)_{i}^{k}\ll f(y)_{k}$ by Lemma 2 as required.

Now suppose that $x=\bigsqcup_{n}x_{n}\in\hat{B}$, we show that
$f(x)=\bigsqcup_{n}f(x_{n})$. As $x_{n}\sqsubseteq x$, it is clear that
$\bigsqcup_{n}f(x_{n})\sqsubseteq f(x)$. To see that
$f(x)\sqsubseteq\bigsqcup_{n}f(x_{n})$, let $(f(x_{n})_{m}^{i})_{i}$ be an
approximating sequence of $f(x_{n})_{m}$ for all $n,m\in\mathbb{N}$. Then
$(\bigsqcup_{n}f(x_{n}))_{k}=\bigsqcup_{0\leq n,m\leq k}f(x_{n})_{m}^{k}$ by
Lemma 3.4 so that we need to show that $f(x)\sqsubseteq(\bigsqcup_{0\leq
n,m\leq k}f(x_{n})_{m}^{k})_{k}$. So let $c\in C$, $n\in\mathbb{N}$ and
suppose that $c\ll f(x)_{n}$. By Corollary 3, there must exist an interpolant
$c^{\prime}\in C$ such that $c\ll c^{\prime}\ll f(x)_{n}$. We show that there
must exist $k\in\mathbb{N}$ such that $c\ll\bigsqcup_{n,m\leq
k}f(x_{n})_{m}^{k}$.

As $c^{\prime}\ll f(x)_{n}\sqsubseteq f(x)$ we have that $x\in
f^{-1}(c^{\prime}\twoheaduparrow)$ which is open by assumption. As
$x=\bigsqcup_{n}x_{n}$, there must exist $m$ such that $x_{m}\in
f^{-1}(c^{\prime}\twoheaduparrow)$, i.e. $c^{\prime}\ll f(x_{m})$. By Lemma
4.8, we have that $f(x)_{m}=\bigsqcup_{n}\bigsqcup_{i\leq n}f(x_{m})_{i}^{n}$
so that there must exist $n\in\mathbb{N}$ such that
$c^{\prime}\sqsubseteq\bigsqcup_{i\leq n}f(x_{m})_{i}^{n}$. Let
$k=\max\\{n,m\\}$. Then $c\ll c^{\prime}\sqsubseteq\bigsqcup_{i\leq
n}f(x_{m})^{i}\sqsubseteq\bigsqcup_{i\leq
n}f(x_{m})^{k}\sqsubseteq\bigsqcup_{0\leq n,m\leq k}f(x_{m})^{k}$ as required.

##  5\. Function Spaces

Given two predomain bases $B$ and $C$, we construct a predomain base $B\to C$
so that the continuous completion of $B\to C$ is the space of continuous
functions between the continuous completions of $B$ and $C$.

######  Definition 9.

Let $(B,\sqsubseteq)$ and $(C,\sqsubseteq)$ be predomain bases. A _single step
function_ of type $B\to C$ is a pair $(b,c)\in B\times C$, written $b$. A
_step function_ is a finite set of single step functions, written
$\bigsqcup_{i}b_{i}$ such that

$\mathsf{Cons}(\\{b_{j}\mid j\in J\\})\to\mathsf{Cons}(\\{c_{j}\mid j\in
J\\})$

for all (finite, non-empty) $J\subseteq I$. Now suppose that $\ll$ on $B$ is
decidable and $C$ is bounded complete. Then a single step function $b$ defines
the function $b$ by $b$ if $b\ll x$, and $b$, otherwise. A step function
$\bigsqcup_{i}b_{i}$ defines the function $(\bigsqcup_{i}b_{i}$. Step
functions are ordered by $s\sqsubseteq t$ iff $s(x)\sqsubseteq t(x)$ for all
$x\in B$. We write $B\to C$ for the set of step functions of type $B\to C$.

Our first goal is to show that the collection of step functions forms a
predomain base, and we begin with collecting conditions that ensure
decidability of the ordering. The proof needs the following condition that
allows us to separate two subsets using the way below relation.

######  Definition 10.

Let $(B,\sqsubseteq)$ be predomain base. Two subsets $A,D\subseteq B$ are
_separated_ if there must exist $\omega\in B$ such that $a\ll\omega$ for all
$a\in A$ and $d\not\ll\omega$ for all $d\in D$.

Crucially, for the ordering on step functions to be decidable, we need to
require that separatedness is decidable.

######  Example 5.10.

  1. (1)

Consider the predomain base $(B,=)$ from Example 2, i.e. equality $=$ on $B$
is decidable. Then $A$ and $D$ are separated if $A$ is a singleton and $A\cap
D=\emptyset$. As a consequence, separatedness between finite sets on $(B,=)$
is decidable.

  2. (2)

For the predomain base $(B^{\ast},\sqsubseteq_{\mathsf{pref}})$ of finite
sequences of $B$, we have that $A$ and $D$ are separated if there exists $a\in
A$ such that every (other) $a^{\prime}\in A$ is a prefix of $a$, and no $d\in
D$ is a prefix of $a$. As a consequence, separatedness is decidable for finite
subsets $A,D\subseteq B^{\ast}$.

The situation with the predomain base of rational intervals is slightly more
complex, and warrants a separate lemma.

######  Lemma 5.11.

Two finite subsets $A,B\subseteq\mathsf{I}\mathbb{Q}$ are separated if and
only if $\bigsqcup A$ exists and is not a singleton (i.e.
$\twoheaduparrow\bigsqcup A$ is not empty) and $b\not\sqsubseteq\bigsqcup A$
for all $b\in B$.

######  Proof 5.12.

Assume that $A=\\{[a_{i},b_{i}]\mid i\in I\\}$ and $B=\\{[c_{j},d_{j}]\mid
j\in J\\}$ for finite sets $I$ and $J$. For the ’if’ direction, assume
moreover that $[a,b]=\bigsqcup A$ exists in $\mathsf{I}\mathbb{Q}$ and
$[c_{j},d_{j}]\not\sqsubseteq\bigsqcup A$ for all $j\in J$. We show that $A$
and $B$ are separated by constructing a witness $\omega$ of separation.
Consider the sets $C$ and $D$ defined by

$C=\\{c_{i}\mid a<c_{i}<b\\}\mbox{ and }D=\\{d_{j}\mid a<d_{j}<b\\}.$

We first consider the case where both $C$ and $D$ are non-empty, and let
$c=\min C$, $d=\max D$, $\epsilon=\min\\{c,d\\}$ and $\delta=\max\\{c,d\\}$.
It is immediate that $a<\epsilon\leq\delta<b$ from the definition of $C$ and
$D$. We now claim that $\omega=[\frac{\epsilon+a}{2},\frac{\delta+b}{2}]$
witnesses separatednes of $A$ and $B$.

First note that $\frac{1}{2}(\epsilon+a)\leq\frac{1}{2}(\delta+b)$ as
$\epsilon\leq\delta$ and $a<b$ so that $\omega\in\mathsf{I}\mathbb{Q}$.
Moreover, $a<\frac{\epsilon+a}{2}\leq\frac{\delta+b}{2}<b$ so that
$[a,b]\ll\omega$ by Lemma 2 and as $[a_{i},b_{i}]\sqsubseteq[a,b]\ll\omega$ we
have that $[a_{i},b_{i}]\ll\omega$ for all $i\in I$ using Lemma 2. To see that
$[c_{j},d_{j}]\not\ll\omega$ suppose that we have $j\in J$ with
$[c_{j},d_{j}]\ll\omega$. Applying Lemma 2 again, we obtain
$c_{j}<\frac{\epsilon+a}{2}<\frac{\epsilon+\epsilon}{2}=\epsilon<b$ and
similarly $a<\delta=\frac{\delta+\delta}{2}<\frac{\delta+b}{2}<d_{j}$. As we
have assumed that $[c_{j},d_{j}]\not\sqsubseteq[a,b]$, we have that $a<c_{j}$
or $d_{j}<b$. In the first case, we obtain $c_{j}\in C$, and hence $c\leq
c_{j}<\epsilon\leq c$, a contradiction. In the second case, we similarly have
$d_{j}\in D$ and obtain a contradiction as $d\leq\delta<d_{j}\leq d$.

We now consider the case where $C\neq\emptyset$ and $D=\emptyset$. Here, we
define $\epsilon=\delta=\min C$ and let
$\omega=[\frac{\epsilon+a}{2},\frac{\delta+b}{2}]$ as before. Again, we have
that $a<\delta=\epsilon<b$ and
$a<\frac{\epsilon+a}{2}\leq\frac{\delta+b}{2}<b$ so that
$\omega\in\mathsf{I}\mathbb{Q}$ and $\omega\ll[a,b]$ whence
$\omega\ll[a_{i},b_{i}]$ for all $i\in I$. Again, if $[c_{j},d_{j}]\ll\omega$
we obtain that $c_{j}<\frac{\epsilon+a}{2}<\frac{\epsilon+\epsilon}{2}<b$ and
$\delta=\frac{\delta+\delta}{2}<\frac{\delta+b}{2}<d_{j}$. As we have assumed
that $[c_{j},d_{j}]\not\sqsubseteq[a,b]$ we again have two cases: $a<c_{j}$ or
$d_{j}<b$. In the first case, we obtain $c_{j}\in C$ and as before we argue
that then $c\leq c_{j}<\epsilon\leq c$ which is impossible. The second case is
slightly different to the argument above, but we just need to observe that
$d_{j}<b$ implies that $d_{j}\in D$, contradicting $D=\emptyset$.

The case where $C=\emptyset$ and $D\neq\emptyset$ is entirely analogous and
left to the reader. Finally, we consider the case where both $C$ and $D$ are
empty. Here, we put $\omega=[\frac{a+b}{2},\frac{a+b}{2}]$. Then
$[a,b]\ll\omega$ as $a<b$, and by the same argument as before,
$[a_{i},b_{i}]\sqsubseteq[a,b]\ll\omega$ whence $[a_{i},b_{i}]\ll\omega$ for
all $i\in I$. To see that $[c_{j},d_{j}]\not\ll\omega$ we again assume that
$[c_{j},d_{j}]\ll\omega$ and show that this is impossible. From the assumption
$[c_{j},d_{j}]\ll\omega$ we obtain that $c_{j}<\frac{a+b}{2}<d_{j}$, using
Lemma 2 one more time. Given that $c_{j}\notin C$, we furthermore obtain that
$c_{j}\leq a$ or $c_{j}\geq b$. The latter case is impossible as then
$\frac{a+b}{2}\leq\frac{b+b}{2}=b\leq c_{j}\leq d_{j}$ which cannot happen as
we assumed that $[c_{j},d_{j}]\ll\omega$. As a consequence, we have that
$c_{j}\leq a$.

For the same reason, given that $d_{j}\notin D$ we have that $d_{j}\leq a$ or
$d_{j}\geq b$. Again the case $d_{j}\leq a$ is impossible (for a similar
reason) so that $d_{j}\geq b$. But then $c_{j}\leq a\leq b\leq d_{j}$ so that
$[c_{j},d_{i}]\sqsubseteq\bigsqcup A$ which contradicts our assumption. This
finishes the proof of the ’if’-implcation.

Conversely, suppose that $A$ and $B$ are separated and $\omega$ is a witness
of separatedness of $A$ and $B$. Then $\omega$ is an upper bound of $A$ so
that $[a,b]=\bigsqcup A$ exists as $\mathsf{I}\mathbb{Q}$ is bounded complete.
As $[a,b]\ll\omega$ by Lemma 2 which implies that $a<b$ by Lemma 2. We now
claim that every $[c_{j},d_{j}]\in D$ satisfies
$[c_{j},d_{j}]\not\sqsubseteq\bigsqcup A$. This follows, for if
$[c_{j},d_{j}]\sqsubseteq[a,b]$ we obtain
$[c_{j},d_{j}]\sqsubseteq[a,b]\ll\omega$ so that $[c_{j},d_{j}]\ll\omega$
which is impossible as $\omega$ witnesses the separation of $A$ and $B$.

As the above characterisation deals with finite subset of
$\mathsf{I}\mathbb{Q}$ and decidable properties only, the following Corollary
is immediate.

######  Corollary 11.

Separatedness is decidable for finite subsets
$A,D\subseteq\mathsf{I}\mathbb{Q}$.

We now use separatedness to characterise the order between step and single
step functions which takes us one step closer to the goal of establishing
decidability of the order on the set of step functions.

######  Theorem 12.

Let $B$ be a predomain base for which $\ll$ is decidable, and let $C$ be
bounded complete. Furthermore, let $I$ be a finite set,
$\\{\alpha\\}\cup\\{\gamma_{i}\mid i\in I\\}\subseteq B$ and
$\\{\beta\\}\cup\\{\delta_{i}\mid i\in I\\}\subseteq C$ and and
$\bigsqcup_{i\in I}\gamma_{i}$ be a step function. Then the following are
equivalent:

  * $\triangleright$

$\alpha$

  * $\triangleright$

for all $x\in B$ with $\alpha\ll x$ we have that
$\beta\sqsubseteq\bigsqcup\\{\delta_{i}\mid i\in I\mbox{ and }\gamma_{i}\ll
x\\}$

  * $\triangleright$

for any $I_{0}\subseteq I$ such that $A=\\{\alpha\\}\cup\\{\gamma_{i}\mid i\in
I_{0}\\}$ and $D=\\{\gamma_{i}\mid i\notin I_{0}\\}$ are separated, we have
$\beta\sqsubseteq\bigsqcup\\{\delta_{i}\mid i\in I_{0}\\}$.

######  Proof 5.16.

The equivalence of the first two items is immediate. So assume that $\alpha\ll
x$ implies that $\beta\sqsubseteq\bigsqcup\\{\delta_{i}\mid\gamma_{i}\ll x\\}$
for all $x\in B$. Moreover, let $I_{0}\subseteq I$ be finite and assume that
$A=\\{\alpha\\}\cup\\{\gamma_{i}\mid i\in I_{0}\\}$ and $D=\\{\gamma_{i}\mid
i\notin I_{0}\\}$ are separated. Note that in this case, the supremum
$\bigsqcup\\{\delta_{i}\mid i\in I_{0}\\}$ exists, as $\bigsqcup_{i\in
I}\gamma_{i}$ is a step function, and $C$ is bounded complete. As
$\sqsubseteq$ is decidable, we may argue classically to show that
$\beta\sqsubseteq\bigsqcup\\{\delta_{i}\mid i\in I_{0}\\}$. As $A$ and $D$ are
separated, we can (classically) find $w$ that witnesses separatedness of $A$
and $D$ (as per Definition 10). In particular, $\alpha\ll\omega$ so that we
have
$\beta\sqsubseteq\bigsqcup\\{\delta_{i}\mid\gamma_{i}\ll\omega\\}=\bigsqcup\\{\delta_{i}\mid
i\in I_{0}\\}$.

For the other direction, assume the last statement above and let $x\in B$ with
$\alpha\sqsubseteq x$. Put $I_{0}=\\{i\in I\mid\gamma_{i}\ll x\\}$. Then
$A=\\{\alpha\\}\cup\\{\gamma_{i}\mid i\in I_{0}\\}$ and $D=\\{\gamma_{i}\mid
i\notin I_{0}\\}$ are separated, and we obtain
$\beta\sqsubseteq\bigsqcup\\{\delta_{i}\mid i\in
I_{0}\\}=\bigsqcup\\{\delta_{i}\mid\gamma_{i}\ll x\\}$ as required.

The above lemma is the key stepping stone to see that the ordering on the
predomain representing the function space is indeed decidable.

######  Corollary 13.

Let $B$ and $C$ be predomain bases where $\ll$ on $B$ is decidable, $C$ is
bounded complete, and separatedness on $C$ is decidable. Then $\sqsubseteq$ on
$B\to C$ is decidable.

######  Proof 5.18.

Immediate by the previous lemma, as $\bigsqcup_{i\in I}\alpha_{i}$ if and only
if $\alpha_{i}$ for all $i\in I$.

Single step functions, and step functions themselves, are automatically Scott
continuous.

######  Lemma 5.21.

Let $B$ and $C$ be predomain bases where $C$ is pointed, $\ll$ on $B$ is
decidable, and $B$ has weak interpolation. Then every single step function $b$
is Scott continuous.

######  Proof 5.23.

Let $(x_{n})_{n}$ be an increasing sequence in $B$ and $x\in B$ with
$x=\bigsqcup_{n}x_{n}$. We show that $b$. This is evident if $c=\bot$. So
suppose $c\neq\bot$. By definition of single step functions (and the fact that
$\ll$ on $B$ is decidable), we may distinguish two cases.

_Case 1._ $b\ll\bigsqcup_{n}x_{n}$ and $b$. By weak interpolation on $B$,
there must exists $y\in B$ such that $b\ll y\ll\bigsqcup_{n}x_{n}$, therefore
there must exist $n\in\mathbb{N}$ such that $b\ll y\sqsubseteq x_{n}$.
Therefore $\bigsqcup_{n}b$. Note that the latter expression is a Harrop-
formula, and therefore $\neg\neg$-stable.

_Case 2._ It is not the case that $b\ll\bigsqcup_{n}x_{n}$. We show that
$\bigsqcup_{n}b$. This follows, if $b$ for all $n\in\mathbb{N}$. So pick
$n\in\mathbb{N}$. We show that $\neg(b\ll x_{n})$. Assume $b\ll x_{n}$. But
then $b\ll\bigsqcup_{n}x_{n}$ whence $b\ll\bigsqcup_{n}x_{n}$ which entails
$b$, a contradiction.

The following lemma is standard in (classical) domain theory, e.g. [AJ94,
Proposition 4.0.2], and helps to construct approximating sequences that in
turn are required to show that step functions form a predomain base.

######  Lemma 5.31.

Let $s$ be a step function. Then $b$ whenever $c\ll s(b)$.

######  Proof 5.33.

Assume that $s\sqsubseteq\bigsqcup_{n}s_{n}$ where the $s_{n}$ are step
functions. Then $s(b)\sqsubseteq\bigsqcup_{n}s_{n}(b)$. Since $c\ll s(b)$ we
can find $n\in\mathbb{N}$ such that $c\sqsubseteq s_{n}(b)$. Let $x\in B$, we
show that $b$. In case $\neg(b\ll x)$ we have $b$. In case $b\ll x$ we have
$b$ by monotonicity of $s_{n}$.

######  Lemma 5.37.

Let $B$ be a countable, bounded complete predomain base and suppose that $\ll$
and separatedness of finite sets on $B$ are decidable, and let $C$ be bounded
complete. Then the set $B\to C$ of step functions is a predomain base.

######  Proof 5.38.

We have to show that every step function $s\in B\to C$ has an approximating
sequence. Let $B=\\{b_{n}\mid n\in\mathbb{N}\\}$. As $C$ is a predomain base,
every $s(b_{i})\in B$ has an approximating sequence $(e_{i}^{j})_{j}$. Let
$s_{n}=\bigsqcup_{0\leq i\leq n}b_{i}$.

We first show that $s_{n}$, for $n\in\mathbb{N}$, is indeed a step function.
Let $J\subseteq\\{0,\dots,n\\}$ be a non-empty subset such that $\\{b_{j}\mid
j\in J\\}$ is consistent. We need to show that $\\{e_{j}^{n}\mid j\in J\\}$ is
consistent. Pick $j\in J$. Then

$e_{j}^{n}\ll s(b_{j})\sqsubseteq s(\bigsqcup_{j\in J}b_{j})$

so that $s(\bigsqcup_{j}b_{j})$ is an upper bound of all $e_{j}^{n}$ for $j\in
J$.

It follows from Lemma 5.31 in combination with Corollary 1 that $s_{n}\ll s$
for all $n\in\mathbb{N}$.

We now show that $s\sqsubseteq\bigsqcup_{n}s_{n}$ for all $n\in\mathbb{N}$.
Fix $n\in\mathbb{N}$ and let $x\in B$, we show that $s_{n}(x)\sqsubseteq
s(x)$. This follows from

$\displaystyle s_{n}(x)$ $\displaystyle=\bigsqcup\\{e_{i}^{n}\mid 0\leq i\leq
n,b_{i}\ll x\\}$ $\displaystyle\sqsubseteq\bigsqcup\\{s(b_{i})\mid 0\leq i\leq
n,b_{i}\ll x\\}$ $\displaystyle\sqsubseteq\bigsqcup\\{s(x)\mid 0\leq i\leq
n,b_{i}\ll x\\}$ $\displaystyle=s(x)$

so that $s$ is an upper bound of the $s_{n}$ in $B\to C$.

We next establish that $s$ is in fact the least upper bound of the $s_{n}$. So
let $t$ be a step function and suppose that $s_{n}\sqsubseteq t$ for all
$n\in\mathbb{N}$. Let $x\in B$, we show that $s(x)\sqsubseteq t(x)$. As $s$ is
a step function, we may assume that $s=\bigsqcup_{i\in I}b_{i}$ for a finite
set $I\subseteq\mathbb{N}$ and elements $c_{i}\in C$. Let $J=\\{i\in I\mid
b_{i}\ll x\\}$ so that $s(x)=\bigsqcup\\{c_{j}\mid j\in J\\}$. By the
interpolation Lemma (Corollary 3) we may find an interpolant $\hat{x}$ such
that $b_{j}\ll\hat{x}\ll x$ for all $j\in J$. Then

$b_{i}\ll x\mbox{ iff }b_{i}\ll\hat{x}\mbox{ for all }i\in I$

so that $s(x)=s(\hat{x})$. As $B$ is countable, we may assume that
$\hat{x}=b_{i}$ for some $i\in\mathbb{N}$. As $(e_{i}^{j})_{j}$ is an
approximating sequence for $s(x)=s(\hat{x})$, it suffices to show that
$e_{i}^{n}\sqsubseteq t(x)$. Now, for $n\geq i$, we have

$\displaystyle e_{i}^{n}$ $\displaystyle\sqsubseteq\bigsqcup_{0\leq i\leq
n}b_{i}$ (as $b_{i}=\hat{x}\ll x$ and $n\geq i$)
$\displaystyle=s_{n}(x)\sqsubseteq t(x)$

so that $e_{i}^{n}\sqsubseteq t(x)$ for all $n\in\mathbb{N}$ whence
$s(x)=\bigsqcup_{n}e_{i}^{n}\sqsubseteq t(x)$ and finally $s\sqsubseteq t$ as
$x$ was arbitrary. We note that this goal formula is stable whence applying
the approximation lemma (that only guarantees classical existence of an
interpolant) in fact proves the claim.

We finally need to establish that $s_{n}\ll s$ for all $n\in\mathbb{N}$. But
this is immediate from Lemma 2. The last requirement for a predomain base,
decidability of ordering, has already been established in Corollary 13.

######  Remark 5.42.

It is in general not true that $c\ll c^{\prime}$ implies that $b$. If
$b^{\prime}\ll b$ in addition to $c\ll c^{\prime}$ we have $b$. This fact
cannot be exploited in the proof of the above Lemma as we have no way of
approximating base elements from above.

We now show that every Scott continuous function arises as a supremum of step
functions.

######  Lemma 5.47.

Let $B,C$ be predomain bases for which consistency is continuous, let $B$ be
bounded complete with decidable $\ll$, and let $C$ be pointed. Then, for every
Scott continuous $f:\hat{B}\to\hat{C}$ there exists
$s=(s_{n})_{n}\in\widehat{B\to C}$ such that $s(x)=\bigsqcup_{n}s_{n}(x)=f(x)$
for all $x\in\hat{B}$.

######  Proof 5.48.

Let $B=\\{b_{0},b_{1},\dots\\}$ and assume that $(b^{i})_{i}$ is an
approximating sequence for all $b\in B$. Suppose that $f:\hat{B}\to\hat{C}$ is
Scott continuous. Let

$s_{n}=\bigsqcup_{0\leq i\leq n}b_{i}$

where we write $f(b_{i})_{n}$ for the $n$-th element of the sequence
$f(b_{i})\in\hat{C}$. Let $x=(x_{n})_{n}\in\hat{B}$ be given.

We first show that $f(x)\sqsubseteq\bigsqcup_{n}s_{n}(x)$. Let
$y_{n}=\bigsqcup_{0\leq i\leq n}x_{i}^{n}$ and $y=(y_{n})_{n}$. Then $x=y$ by
Lemma 4.8 and it therefore suffices to show that

$\bigsqcup_{n}f(y_{n})\sqsubseteq\bigsqcup_{n}s_{n}(x)$

as $f$ is extensional, i.e. $f(x)=f(y)$ and Scott continuous, i.e.
$f(\bigsqcup_{n}y_{n})=\bigsqcup_{n}f(y_{n})$. We have the following
calculations for the $k$-th elements of the respective sequences:

$A_{k}=(\bigsqcup_{n}f(y_{n}))_{k}=\bigsqcup_{n\leq
k}f(y_{n})_{k}=\bigsqcup_{n\leq k}f(\bigsqcup_{i\leq n}x_{i}^{n})$

and

$B_{k}=(\bigsqcup_{n}s_{n}(x))_{k}=\bigsqcup_{n\leq
k}s_{n}(x_{k})=s_{k}(x_{k})=\bigsqcup\\{f(b_{i})_{k}\mid 0\leq i\leq
k,b_{i}\ll x_{k}\\}$

by Definition of $s_{n}$ and Lemma 3.4. We therefore need to show that
$(A_{k})_{k}\sqsubseteq(B_{k})_{k}$. So let $k\in\mathbb{N}$ and $x\in C$ such
that $x\ll A_{k}$. Choose $l$ large enough so that $l\geq k$,
$\\{x_{0},\dots,x_{k}\\}\subseteq\\{b_{0},\dots,b_{l}\\}$ and
$\bigsqcup_{i\leq n}x_{i}^{n}\in\\{b_{0},\dots,b_{l}\\}$ for all $n\leq k$.

Now fix $n\leq k$. By our assumption on $l$, we have $j\leq l$ such that
$\bigsqcup_{i\leq n}x_{i}^{n}=b_{j}$. Moreover, for all $i\leq n$ we have
$x_{i}^{n}\ll x_{i}\sqsubseteq x_{l}$ so that $b_{j}=\bigsqcup_{i\leq
n}x_{i}^{n}\ll x_{l}$. Hence

$f(\bigsqcup_{i\leq
n}x_{i}^{n})_{k}=f(b_{j})_{k}\sqsubseteq\bigsqcup\\{f(b_{i})_{k}\mid 0\leq
i\leq l,b_{i}\ll x_{l}\\}=B_{l}.$

As $n$ was arbitrary, we therefore obtain $\bigsqcup_{n\leq
k}f(\bigsqcup_{i\leq n}x_{i}^{n})\sqsubseteq B_{l}$ and finally $x\ll B_{l}$
as required.

We now show that $\bigsqcup_{n}s_{n}(x)\sqsubseteq f(x)$. By Scott-continuity
of $f$, we have $f(x)=\bigsqcup_{n}f(x_{n})$ and the claim follows if
$\bigsqcup_{n}s_{n}(x)\sqsubseteq\bigsqcup_{n}f(x_{n})$. As above, we
calculate for the $k$-th element of the respective sequences that

$A_{k}=(\bigsqcup_{n}f(x_{n}))_{k}=\bigsqcup_{n\leq k}f(x_{n})_{k}$

and

$B_{k}=(\bigsqcup_{n}s_{n}(x))_{k}=\bigsqcup\\{f(b_{i})_{k}\mid 0\leq i\leq
k,b_{i}\ll x\\}$

where we have used Lemma 3.4 for the calculation of $A_{k}$, and the
calcuation of $B_{k}$ is as above. To see that
$(B_{k})_{k}\sqsubseteq(A_{k})_{k}$, fix $x\in C$, $k\in\mathbb{N}$ and assume
that $x\ll B_{k}$. Let $N=\\{0\leq i\leq k\mid b_{i}\ll x_{k}\\}$ so that
$B_{k}=\bigsqcup\\{f(b_{i})_{k}\mid i\in N\\}$.

We claim that $f(b_{i})\sqsubseteq f(x_{k})$ for every $i\in N$. This is
immediate, since $i\in N$ implies that $b_{i}\ll x_{k}$, therefore
$b_{i}\sqsubseteq x_{k}$ and $f(b_{i})\ll f(x_{k})$ by monotonicity of $f$. As
a consequence,
$f(b_{i})_{k}\sqsubseteq\bigsqcup_{n}f(b_{i})_{n}=f(b_{i})\sqsubseteq
f(x_{k})$ whence $\bigsqcup\\{f(b_{i})_{k}\mid i\in N\\}\sqsubseteq f(x_{k})$
where we view the left-hand side of the last equation as a constant sequence.
As $x\ll B_{k}=\bigsqcup\\{f(b_{i})_{k}\mid i\in N\\}$ there must exist
$l\in\mathbb{N}$ such that $x\ll f(x_{k})_{l}$. By monotonicity of
$(f(x_{k})_{n})_{n}$, the same holds for $l$ replaced by $\max\\{l,k\\}$ so
that we assume without loss of generality that $l\geq k$. In summary, we have
obtained $x\ll f(x_{k})_{l}\sqsubseteq\bigsqcup_{n\leq l}f(x_{n})_{l}=A_{l}$
as required.

##  6\. Real Numbers as Total Elements of the Interval Domain

We now consider an important example of predomain bases in more detail, the
predomain base of rational intervals that we have already introduced in
Example 2. Specifically, we introduce a constructive representation of the set
of real numbers as the total elements of the interval domain, and give a
characterisation of continuous functions on real numbers in terms of Scott
continuous functions on the interval domain. Specifically, we compare total
elements of the interval domain with the (standard) constructive notion of
Cauchy reals, and characterise the total elements of the interval domain as
_Markov reals_ , i.e. Cauchy reals where the modulus of convergence has been
replaced with a modulus of non-divergence.

In summary, we establish that if Markov’s principle holds, Cauchy reals and
Markov reals are equivalent, and in turn equivalent to total reals in the
sense of domain theory.

######  Definition 14 (Basic Notions).

We write $\mathsf{I}\mathbb{R}$ for the continuous completion of
$\mathsf{I}\mathbb{Q}$, and write $\underline{\alpha},\overline{\alpha}$ for
the upper and lower endpoint of $\alpha\in\mathsf{I}\mathbb{Q}$ as in Example
2, and identify $x\in\mathsf{I}\mathbb{R}$ with the sequence $(x_{n})_{n}$ so
that $x=(x_{n})_{n}=([\underline{x}_{n},\overline{x}_{n}])_{n}$ for
$x\in\mathsf{I}\mathbb{R}$. The _length_ of $a\in\mathsf{I}\mathbb{Q}$ is
given by $\ell(a)=\overline{a}-\underline{a}$. An element
$x\in\mathsf{I}\mathbb{R}$ is a _total real_ or a simply a _real_ , if for all
$k\in\mathbb{N}$ there must exist $n\in\mathbb{N}$ such that $\ell(x_{n})\leq
2^{-k}$. We write $\mathbb{R}$ for the set of total reals, and call a function
$f:\mathsf{I}\mathbb{R}\to\mathsf{I}\mathbb{R}$ _total_ if $f(x)\in\mathbb{R}$
whenever $x\in\mathbb{R}$. For $a,b\in\mathsf{I}\mathbb{Q}$ we put

$a+b=[\underline{a}+\underline{b},\overline{a}+\overline{b}]\qquad-a=[-\overline{a},-\underline{a}]$

and $|a|=a$ if $0\leq\underline{a}$,
$|a|=[0,\max\\{-\underline{a},\overline{a}\\}]$ if $\underline{a}\leq
0\leq\overline{a}$ and $|a|=-a$ if $\overline{a}\leq 0$. These operations are
extended pointwise to elements $x,y\in\mathsf{I}\mathbb{R}$, i.e.
$x+y=(x_{n}+y_{n})_{n}$, $-x=(-x_{n})_{n}$, $|x|=(|x_{n}|)_{n}$ for all
$n\in\mathbb{N}$. For $x=(x_{n})_{n}\in\mathsf{I}\mathbb{R}$ we put $0\leq x$
if given $k\in\mathbb{N}$ there must exist $n\in\mathbb{N}$ such that
$-2^{-k}\leq\underline{x}_{n}$ and $x\leq y$ if $0\leq y-x$.

Given that the arithmetic operation above are defined on equivalence classes
of (elements of) the continuous completion of $\mathsf{I}\mathbb{Q}$, we need
to show that they are well defined with respect to the (defined) equality in
the continuous completion (Definition 5). This is a standard verification.

######  Lemma 6.1.

Let $x$, $y$, $x^{\prime}$ and $y^{\prime}\in\mathsf{I}\mathbb{R}$ and suppose
that $x=x^{\prime}$ and $y=y^{\prime}$. Then $x+y=x^{\prime}+y^{\prime}$,
$-x=-x^{\prime}$, $|x|=|x^{\prime}|$ and $0\leq x$ if and only if $0\leq
x^{\prime}$.

######  Proof 6.2.

We write $x=(x_{n})_{n}$, $x_{n}=[\underline{x}_{n},\overline{x}_{n}]$ and
similarly for $x^{\prime}$, $y$ and $y^{\prime}$. For an element
$z=[\underline{z},\overline{z}]\in\mathsf{I}\mathbb{Q}$ and
$\epsilon\in\mathbb{Q}$ with $\epsilon\geq 0$ we write
$z\pm\epsilon=[\underline{z}-\epsilon,\overline{z}+\epsilon]$ as in Example 2.
We begin with addition where it suffices to show that $x+y\sqsubseteq
x^{\prime}+y^{\prime}$. So assume that $b\in\mathsf{I}\mathbb{Q}$,
$n\in\mathbb{N}$ and $b\ll(x+y)_{n}$. We show that there must exist $m$ such
that $b\ll(x^{\prime}+y^{\prime})_{m}$. Because $b\ll(x+y)_{n}$, there exists
$\epsilon>0$ such that $b\ll(x+y)_{n}\pm\epsilon$. Because $x\sqsubseteq
x^{\prime}$ there mus exist $m_{x}$ such that $x_{n}\pm\frac{\epsilon}{2}\ll
x^{\prime}_{m_{x}}$. For the same reason, there must exist $m_{y}$ such that
$y_{n}\pm\frac{\epsilon}{2}\ll y^{\prime}_{m_{y}}$. For
$m=\max\\{m_{x},m_{y}\\}$ we therefore obtain that
$b\ll(x+y)_{n}\pm\epsilon=x_{n}\pm\frac{\epsilon}{2}+y_{n}\pm\frac{\epsilon}{2}\sqsubseteq
x^{\prime}_{m_{x}}+y^{\prime}_{m_{y}}\sqsubseteq(x^{\prime}+y^{\prime})_{m}$
as required.

For unary minus, it similarly suffices to show that
$-x\sqsubseteq-x^{\prime}$. If $b\ll-x_{n}$, Lemma 2 shows that $-b\ll x_{n}$
whence there must exist $m$ such that $-b\ll x^{\prime}_{m}$ so that
$b\ll-x^{\prime}_{m}$ by applying Lemma 2 again.

For the last claim, assume that $0\leq x$, we show that $0\leq x^{\prime}$.
Let $k\geq 0$ be given. We show that there must exist $m\in\mathbb{N}$ such
that $-2^{-k}\leq\underline{x}^{\prime}_{m}$. As $0\leq x$, there must exist
$n$ such that $-2^{-(k+1)}\leq\underline{x_{n}}$. As $x_{n}\pm 2^{-(k+1)}\ll
x_{n}$, there must exist $m$ such that $x_{n}\pm 2^{-(k+1)}\ll x^{\prime}_{m}$
as $x=x^{\prime}$ by assumption. In summary, we then obtain
$-2^{-k}=-2^{-(k+1)}-2^{-(k+1)}\leq\underline{x_{n}}-2^{-(k+1)}\leq x_{m}$ as
required.

To show that $|x|=|x^{\prime}|$ assume that $b\ll|x|_{n}$. As ordering on
$\mathbb{Q}$ is decidable, we may distinguish the following cases.

_Case 1: $0<\underline{x}_{n}$._ It is easy to see that in this case, there
must exist $m_{0}$ such that $0<\underline{x}^{\prime}_{m_{0}}$. Also, as
$b\ll|x_{n}|=x_{n}$, there must exist $m_{1}$ such that $b\ll
x^{\prime}_{m_{1}}$. For $m=\max\\{m_{0},m_{1}\\}$ we therefore have that
$b\ll x^{\prime}_{m_{1}}\sqsubseteq x^{\prime}_{m}$ and as
$0\leq\underline{x}^{\prime}_{m_{0}}\leq\underline{x}^{\prime}_{m}$ we have
that $|x^{\prime}_{m}|=x^{\prime}_{m}$ so that $b\ll|x^{\prime}_{m}|$ as
required.

_Case 2:_ $\underline{x}_{n}\leq 0\leq\overline{x}_{n}$. In this case we have
$b\ll[0,\max\\{-\underline{x}_{n},\overline{x}_{n}\\}]$ so that
$\underline{b}<0$ and
$\overline{b}>\max\\{-\underline{x}_{n},\overline{x}_{n}\\}$. We then have
that $[-\overline{b},\overline{b}]\ll x_{n}$ and because $x=x^{\prime}$ there
must exist $m$ such that $[-\overline{b},\overline{b}]\ll x^{\prime}_{m}$.
Again the decidability of order on $\mathbb{Q}$ allows us to distinguish three
subcases to relate this to $|x^{\prime}_{m}|$.

_Subcase 2a: $\underline{x}^{\prime}_{m}>0$_. Then
$\underline{b}<0<\underline{x}^{\prime}_{m}\leq\overline{x}^{\prime}_{m}<\overline{b}$
as $-b<0$ and $[-\overline{b},\overline{b}]\ll x^{\prime}_{m}$. Hence
$b=[\underline{b},\overline{b}]\ll x^{\prime}_{m}=|x^{\prime}_{m}|$.

_Subcase 2b: $\underline{x}^{\prime}_{m}\leq 0\leq\overline{x}^{\prime}_{m}$._
As $[-\overline{b},\overline{b}]\ll x_{m}$ we have that
$\max\\{-\underline{x}^{\prime}_{m},\overline{x}^{\prime}_{m}\\}<\overline{b}$.
As $\underline{b}<0$ as noted above, this gives
$\underline{b}<0\leq\max\\{-\underline{x}^{\prime}_{m},\overline{x}^{\prime}_{m}\\}<\overline{b}$
so that
$b\ll[0,\max\\{-\underline{x}^{\prime}_{m},\overline{x}^{\prime}_{m}\\}]=|x_{m}|$.

_Subcase 2c: $\overline{x}^{\prime}_{m}<0$._ Similarly to Subcase 2a we obtain
that
$-\overline{b}<\underline{x^{\prime}_{m}}\leq\overline{x}^{\prime}_{m}<0<-\underline{b}$
so that
$\underline{b}<0<-\overline{x}^{\prime}_{m}\leq-\underline{x}^{\prime}_{m}<\overline{b}$
and
$[\underline{b},\overline{b}]\ll[-\overline{x}^{\prime}_{m},-\underline{x}^{\prime}_{m}]=|x_{m}|$.

Our last case is analogous to the first:

_Case 3: $\overline{x}_{n}<0$._ As in the first case, it is easy to see that
there must exist $m_{0}$ such that $x^{\prime}_{m_{0}}<0$. Moreover,
$b\ll|x_{n}|=-x_{n}$ so that $-b\ll x_{n}$. As consequence, there must exist
$m_{1}$ such that $-b\ll x^{\prime}_{m_{1}}$. Let $m=\max\\{m_{0},m_{1}\\}$.
Then $-b\ll x^{\prime}_{m}$ whence $b\ll-x^{\prime}_{m}$ and
$\overline{x}^{\prime}_{m}<0$ so that $|x^{\prime}_{m}|=-x^{\prime}_{m}$.
Taken together this gives $b\ll|x^{\prime}_{m}|$ as required.

This argument shows that $|x|\sqsubseteq|x^{\prime}|$ which is sufficient to
establish the penultimate claim.

The fact that the total reals coincide with the maximal elements of
$\mathsf{I}\mathbb{R}$ is essentially a consequence that totality is
formulated negatively (and, like maximality, has no computational content).

######  Lemma 6.3.

The total reals are precisely the maximal elements of $\mathsf{I}\mathbb{R}$.

######  Proof 6.4.

Let $x\in\mathbb{R}$ be total and suppose that $x\sqsubseteq y$ where
$y\in\mathsf{I}\mathbb{R}$. We show $y\sqsubseteq x$. So let
$a\in\mathsf{I}\mathbb{R}$, $n\in\mathbb{N}$ and suppose that $a\ll y_{n}$. We
show that there must exist $k\in\mathbb{N}$ such that $a\ll x_{k}$. By Lemma 2
there exists $\epsilon\in\mathsf{I}\mathbb{Q}$, $\epsilon>0$ so that $a\ll
y_{n}\pm\epsilon$. As $x$ is an interval real, there must exist
$k\in\mathbb{N}$ such that $\ell(x_{k})\leq\frac{\epsilon}{2}$. We show that
$a\ll x_{k}$. Since $x_{k}\pm\frac{\epsilon}{2}\ll x_{k}$ and $x\sqsubseteq y$
there must exist $l\in\mathbb{N}$ such that $x_{k}\pm\frac{\epsilon}{2}\ll
y_{l}$. We may assume that $l\geq n$. Using Lemma 2 this entails that
$\underline{x}_{k}-\frac{\epsilon}{2}<\underline{y}_{l}\leq\overline{y}_{l}<\overline{x}_{k}+\frac{\epsilon}{2}$
so that $\underline{y}_{l}-\overline{x}_{k}-\frac{\epsilon}{2}<0$. Using this
estimate, we obtain

$\underline{a}<\underline{y}_{n}-\epsilon\leq\underline{y}_{n}-(\overline{x}_{k}-\underline{x}_{k}+\frac{\epsilon}{2})\leq\underline{x}_{k}+\underline{y}_{l}-\overline{x}_{k}-\frac{\epsilon}{2}\leq\underline{x}_{k}.$

One analogously establishes that $\overline{x}_{k}<\overline{a}$ so that $a\ll
x_{k}$ as desired.

Now let $x$ be maximal. We show that $\forall
k\in\mathbb{N}.\,\tilde{\exists}n\in\mathbb{N}.\,\ell(x_{n})\leq 2^{-k}$. So
assume that $k\in\mathbb{N}$ and $\forall n\in\mathbb{N}.\,\neg\ell(x_{n})\leq
2^{-k}$. We establish a contradiction.

Define $y_{n}=[\underline{x}_{n}+2^{-n-1},\overline{x}_{n}-2^{-n-1}]$. Then
$y=(y_{n})_{n}\in\mathsf{I}\mathbb{R}$ and $x\sqsubseteq y$. As $x$ is
maximal, we have $y\sqsubseteq x$. Since $y_{k}\pm 2^{-k-1}\ll y_{k}$ and
$y\sqsubseteq x$, there must exist $m\in\mathbb{N}$ such that $y_{k}\pm
2^{-k-1}\ll x_{m}$. We may assume that $m\geq k$. Then
$\ell(y_{k})+2^{-k}=\ell(y_{k}\pm 2^{-k-1})<\ell(x_{m})$. But then
$\ell(x_{k})=\ell(y_{k})+2^{-k}<\ell(x_{m})\leq\ell(x_{n})$, the desired
contradiction.

We characterise total reals as Cauchy sequences where we reformulate the
notion of Cauchyness to account for the lack of information on convergence
speed.

######  Definition 15.

A _classical null sequence_ is a decreasing sequence $(q_{n})_{n}$ in
$\mathbb{Q}_{\geq 0}\cup\\{\infty\\}$ such that
$\forall\epsilon>0.\,\tilde{\exists}m\in\mathbb{N}.\,\forall n\geq
m.\,q_{n}\leq\epsilon$. We write $(q_{n})_{n}\searrow 0$ if $(q_{n})_{n}$ is a
classical null-sequence.

A _modulus of non-divergence_ of a rational sequence $(q_{n})_{n}$ is a
classical null-sequence $(c_{n})_{n}$ such that $\forall
N\in\mathbb{N}.\,\forall n,m\geq N.\,|q_{n}-q_{m}|\leq c_{N}$.

Finally, _modulus of convergence_ of a rational sequence $(q_{n})_{n}$ is a
non-decreasing function $M:\mathbb{N}\to\mathbb{N}$ such that $\forall n,m\geq
M(k).\,|q_{n}-q_{m}|\leq 2^{-k}$.

A rational sequence $(q_{n})_{n}$ is _Cauchy_ if it has a modulus of
convergence, and _Markov_ if it has a modulus of non-divergence. A _Cauchy
real_ (_Markov real_) is a rational sequence together with a modulus of
convergence (modulus of non-divergence).

We allow classical null sequences to begin with $\infty$ to account for
partially defined approximations of functions later. The following is simple
observation, but requires a rather technical proof to allow us to convert
between moduli of (dis-) continuity.

######  Lemma 6.5.

Every Cauchy sequence is Markov.

The proof of this lemma needs the following auxiliary statement that helps to
convert the modulus into a (classical) null sequence.

######  Lemma 6.6.

Let $M:\mathbb{N}\to\mathbb{N}$. Then there exists a non-decreasing function
$W:\mathbb{N}\to\mathbb{N}$ such that $W(M(0))=0$, $(2^{-W(n)})_{n}$ is a
classical null sequence and $M\circ W(n)\leq n$ for all $n\geq M(0)$.

######  Proof 6.7.

We put $W(n)=0$ for $n\leq M(0)$ and use induction for $n>M(0)$, i.e.

$W(n)=\begin{cases}W(n-1)&\mbox{ if }M(W(n-1)+1)>n\\\ W(n-1)+1&\mbox{ if
}M(W(n-1)+1)\leq n\end{cases}$

for all $n>M(0)$. It is clear that $W(M(0))=0$. We first claim that $W$ is
non-decreasing, but this is evident from the definition of $W$. Next, we show
by induction on $n$ that $M\circ W(n)\leq n$ for all $n\geq M(0)$. For
$n=M(0)$ this follows directly from the definition, as then $M\circ
W(n)=M(0)\leq M(0)=n$. Now let $n>M(0)$. We distinguish two cases. If
$M(W(n-1)+1)>n$, then $M\circ W(n)=M\circ W(n-1)\leq n-1\leq n$. If on the
other hand, $M(W(n-1)+1)\leq n$, we obtain $M\circ W(n)=M(W(n-1)+1)\leq n$ by
assumption.

We now show that $W$ is progressive, that is, $\forall n\geq M(0).\,\exists
m\geq n+1.\,W(m)>W(n)$. Fix $n\geq M(0)$ and put $m=n+k$ where
$k=\max\\{1,M(W(n)+1)-M(W(n))\\}$. As $W$ is monotone, it suffices to show
that $W(n)=W(n+1)=\dots=W(n+k)$ is contradictory as the latter chain of
equivalences is decidable.

So assume that $W(n)=W(n+1)=\dots=W(n+k)$. In particular, as
$W(n+k)=W(n+k-1)$, we obtain $M(W(n+k-1)+1)>n+k$. Since $W(n+k-1)=W(n)$ this
gives $M(W(n)+1)>n+k$. Substituting the definition of $k$, this gives
$M(W(n)+1)>n+M(W(n)+1)-M(W(n))$, i.e. $M\circ W(n)>n$, contradicting our
earlier statement.

We now show that $W(n)$ is not bounded, i.e. $\forall k\in\mathbb{N}.\,\exists
n\in\mathbb{N}.\,W(n)\geq k$. This follows by induction on $k$, and for $k=0$
we put $n=0$. For the inductive step, assume that there exists
$n^{\prime}\in\mathbb{N}$ such that $W(n^{\prime})\geq k-1$. By the previous
claim, there exists $n\geq n^{\prime}+1$ such that $W(n)>W(n^{\prime})\geq
k-1$ so that $W(n)\geq k$.

This now shows that $(2^{-W(n)})_{n}$ is a classical null-sequence, for any
$\epsilon\geq 0$ there exists $k\geq\frac{1}{\epsilon}+1$ and in turn
$n\in\mathbb{N}$ such that $W(n)\geq k$ whence $2^{-W(n)}\leq
2^{-k}\leq\frac{1}{k}\leq\epsilon$ as $k\geq 1$.

We now give the proof of Lemma 6.5.

######  Proof 6.8.

Let $(q_{n})_{n}$ be a Cauchy sequence with modulus $M$, i.e. $\forall
k\in\mathbb{N}.\,\forall n,m\geq M(k),\hskip 4.2679pt|q_{n}-q_{m}|\leq
2^{-k}$. By Lemma 6.6 there exists a non-decreasing function
$W:\mathbb{N}\to\mathbb{N}$ such that $M\circ W(n)\leq n$ for all $n\geq M(0)$
and $(2^{-W(n)})_{n}$ is a classical null-sequence.

We define a sequence $(c_{n})_{n}$ of non-negative rationals by
$c_{n}=1+\max\\{|q_{k}-q_{l}|\mid n\leq k,l\leq M(0)\\}$ if $n<M(0)$ and
$c_{n}=2^{-W(n)}$ if $n\geq M(0)$.

We now show that if $m,n\geq N$, then $|q_{n}-q_{m}|\leq c_{N}$. To see this,
we distinguish the cases $N<M(0)$ and $N\geq M(0)$. First suppose that
$N<M(0)$. If both $n,m\leq M(0)$ this follows by definition of $c_{N}$. If
both $n,m\geq M(0)$ then $|q_{n}-q_{m}|\leq 2^{0}=1\leq c_{N}$. Now consider
without loss of generality that $n<M(0)$ and $m\geq M(0)$. Then
$|q_{n}-q_{m}|\leq|q_{n}-q_{M(0)}|+|q_{M(0)}-q_{m}|\leq\max\\{|q_{k}-q_{l}|:N\leq
k,l\leq M(0)\\}+1=c_{N}$.

Now suppose that $N\geq M(0)$ and let $m,n\geq N$. Then $M\circ W(N)\leq N$ so
that $m,n\geq M(W(n))$ whence $|q_{n}-q_{m}|\leq 2^{-W(N)}=c_{N}$. It remains
to show that $(c_{n})_{n}$ is a classical null-sequence which is however
immediate from the fact that that $2^{-W(n)}$ is a classical null sequence.

In fact, it turns out that the equivalence of Cauchy and Markov reals
characterises Markov’s principle itself.

######  Lemma 6.9.

If Markov’s Principle holds, every Markov sequence is Cauchy.

######  Proof 6.10.

Let $(q_{n})_{n}$ be a Markov sequence with (Markov-) moduls $(c_{n})_{n}$. As
$c_{n}$ is a classical null-sequence, we obtain that $\forall
k\in\mathbb{N}.\,\tilde{\exists}n\in\mathbb{N}.\,c_{n}\leq 2^{-k}$. By
Markov’s principle, we may replace the weak existential quantifier by a strong
one, and number choice yields the Cauchy modulus.

######  Lemma 6.11.

If every Markov Sequence is Cauchy, then Markov’s principle holds.

######  Proof 6.12.

Suppose that every Markov sequence is Cauchy, and let $P(n)$ be a decidable
predicate on natural numbers. Suppose that $\tilde{\exists}n.\,P(n)$. We show
that $\exists n.\,P(n)$. Define a sequence $(q_{n})_{n}$ by $q_{n}=0$ if
$\forall k\leq n.\,\neg P(n)$, and $q_{n}=1$, otherwise. We claim that
$(q_{n})_{n}$ is a Markov sequence. Put $c_{n}=1-q_{n}$. Then clearly
$|q_{n}-q_{m}|\leq c_{N}$ for $n,m\geq N$ and $N\in\mathbb{N}$. If $c_{N}=1$
then clearly $|q_{n}-q_{m}|\leq 1$. If, on the other hand, $c_{N}=0$ we have
$q_{N}=1$ and therefore $q_{n}=q_{m}=1$ as $n,m\geq N$. It remains to see that
$(c_{n})\searrow 0$, i.e. $(c_{n})_{n}$ is a classical null-sequence. It is
clear that $c_{n}$ is decreasing. Now let $\epsilon>0$. We show that
$\tilde{\exists}n.\,c_{n}\leq\epsilon$ by showing that
$\tilde{\exists}n.\,c_{n}=0$. But we have $\tilde{\exists}n.\,P(n)$ hence
$\tilde{\exists}n.\,q_{n}=1$ whence $\tilde{\exists}n.\,c_{n}=0$.

We are now in a position to relate Markov reals to the total reals, i.e. the
maximal elements in the interval domain.

######  Lemma 6.13.

Every Markov real is a total real, and vice versa. More precisely, the
following hold:

  1. (1)

Every total real $x=(x_{n})_{n}$ defines a Markov sequence
$m(x)=(\frac{1}{2}(\overline{x}_{n}+\underline{x}_{n}))$ with Markov modulus
$c_{n}=\overline{x}_{n}-\underline{x}_{n}$.

  2. (2)

Every Markov-sequence $q=(q_{n})_{n}$ with modulus $(c_{n})_{n}$ defines a
total real $t(q)=(x_{n})_{n}=(\bigsqcup_{0\leq i\leq n}q_{i}\pm c_{i})_{n}$.

  3. (3)

If $x$ is a total real, then $x=t(m(x))$, that is, the above constructions
perserve equality.

######  Proof 6.14.

First suppose that $x=(x_{n})_{n}=([\underline{x}_{n},\overline{x}_{n}])_{n}$
is a total real and let
$q_{n}=\frac{1}{2}(\overline{x}_{n}+\underline{x}_{n})$. By definition,
$c_{n}=\overline{x}_{n}-\underline{x}_{n}$ is a classical null-sequence, so
that we just need to establish that $|q_{n}-q_{m}|\leq c_{N}$ whenever
$n,m\geq N$. Let $k=\min\\{n,m\\}$ and $l=\max\\{n,m\\}$. Then $k,l\geq N$ and
we have that
$q_{n}-q_{m}=\frac{1}{2}(\overline{x}_{n}+\underline{x}_{n}-\overline{x}_{m}-\underline{x}_{m})\leq\frac{1}{2}(\overline{x}_{k}+\underline{x}_{l}-\overline{x}_{l}-\underline{x}_{k})=\frac{1}{2}(c_{k}+c_{l})\leq
c_{N}$ by monotonicity of $x$. One analogously establishes that $-c_{N}\leq
q_{n}-q_{m}$ whence $|q_{n}-q_{m}|\leq c_{N}$.

For the converse, we just need to establish that $\\{q_{i}\pm c_{i}\mid 0\leq
i\leq n\\}$ is consistent, given a Markov sequence $(q_{n})_{n}$ with modulus
$(c_{n})_{n}$ which is evident as for example $c_{n}\sqsubseteq q_{i}\pm
c_{i}$ for all $0\leq i\leq n$. The last claim is evident by construction.

If we were to define the natural equality relation on Markov reals, we would
also be able to establish that the above constructions also preserve equality
of Markov reals, but this is not needed for what follows.

##  7\. Example: Computation of Square Roots

Having established the interval domain as a way of reperesenting real numbers,
we now exemplify the claim that we made in the introduction by means of an
example: computation with constructive domain theoretic reals gives actual-
case error bounds that are much tighter than the worst case error bounds of
Cauchy reals.

Throughout the section, we fix a positive rational number $q>0$ and
demonstrate how to compute a total real
$s=([\underline{s}_{n},\overline{s}_{n}])_{n}$ such that
$\underline{s}_{n}^{2}\leq q\leq\overline{s}_{n}^{2}$ for all
$n\in\mathbb{N}$, i.e. $s$ represents the square root of $q$.

Our definition is based on Newton iteration, specifically

$\overline{s}_{-1}=1\qquad\overline{s}_{n}=\frac{1}{2}\left(\overline{s}_{n-1}+\frac{q}{\overline{s}_{n-1}}\right)\qquad\underline{s}_{n}=q/\overline{s}_{n}$

for all $n\in\mathbb{N}$. We show that
$s=([\underline{s}_{n},\overline{s}_{n}])_{n}$ is indeed a total real, and
represents the square root of $q$. This is a sequence of lemmas involving
standard estimates, the proofs of which we elide. In particular:

######  Lemma 7.1.

Let $s$ be given as above.

  1. (1)

Both $\underline{s}_{n}>0$ and $\overline{s}_{n}>0$ for all $n\in\mathbb{N}$.

  2. (2)

$(\overline{s}_{n})_{n}$ is decreasing with $\overline{s}_{n}^{2}\geq q$ for
all $n\in\mathbb{N}$.

  3. (3)

$(\underline{s}_{n})_{n}$ is increasing with $\underline{s}_{n}^{2}\leq q$ for
all $n\in\mathbb{N}$.

  4. (4)

$\underline{s}_{n}\leq\overline{s}_{n}$ for all $n\in\mathbb{N}$.

We now need to demonstrate that $s$ is indeed total, i.e. the distance
$\overline{s}_{n}-\underline{s}_{n}$ can be made arbitrarily small. This is an
immediate consequence of the fact that $(\underline{s}_{n})$ is increasing
that we use in the following lemma.

######  Lemma 7.2.

We have that
$\overline{s}_{n}-\underline{s}_{n}\leq\frac{1}{2}(\overline{s}_{n-1}-\underline{s}_{n-1})$
for all $n>0$.

######  Proof 7.3.

Immediate, as

$\overline{s}_{n}-\underline{s}_{n}\leq\frac{1}{2}\left(\overline{s}_{n-1}+\frac{q}{\overline{s}_{n-1}}\right)-\underline{s}_{n-1}\leq\frac{1}{2}\left(\overline{s}_{n-1}-\underline{s}_{n-1}\right)$

using that $\underline{s}_{n}$ is increasing.

The following is now immediate:

######  Corollary 16.

With $\underline{s}_{n}$ and $\overline{s}_{n}$ defined as above,
$s=(\underline{s}_{n},\overline{s}_{n})_{n}$ is a total real with $s^{2}=q$.

We have the following comparision to Cauchy reals.

######  Comparison 17.

If $q=2$, in particular we have that
$|\overline{s}_{n}-\overline{s}_{m}|\leq\frac{1}{6\cdot 2^{n}}$ for all $m\geq
n$. In other words, computing the $n$-th iterate of the square root of two,
the attained precision is $\frac{1}{6\cdot 2^{n}}$. This is precisely the same
modulus of convergence that was obtained for the very same example in [Sch16].
The following table compares this to the interval width obtained from a domain
theoretic approach where we have used a simple (hand extracted) Haskell
program to obtain the data reported.

Iterations | Interval Width | Modulus Precision
---|---|---
1 | $4.9\times 10^{-3}$ | $8.3\times 10^{-2}$
2 | $4.2\times 10^{-6}$ | $4.2\times 10^{-2}$
3 | $3.2\times 10^{-12}$ | $2.1\times 10^{-2}$
4 | $1.8\times 10^{-24}$ | $1.0\times 10^{-2}$
5 | $5.7\times 10^{-49}$ | $5.2\times 10^{-3}$

While we cannot draw any valid conclusions from this very small experiment, we
nonetheless note that the difference in precision is staggering, and warrant
further investigation.

##  8\. Scott Topology vs Euclidean Topology

In Section 6, we have investigated total reals _individually_ by relating them
to Markov and Cauchy reals. We continue our investigation of the real line
induced by the total elements of the interval domain by also considering the
topology on the real line, and linking that with the Scott topology of the
interval domain.

As with convergence speed, we adopt a classical definition of properties, in
particular that of openness.

######  Definition 18 (Basic Notions).

A subset $O\subseteq\mathbb{R}$ is _open_ , if for all $x\in O$ there must
exist $k\in\mathbb{N}$ such that $\forall y\in\mathbb{R}.\,|x-y|\leq 2^{-k}\to
y\in O$.

Our first result shows that the topology defined above is the subspace
topology on the set of total reals, induced by the Scott topology. That is,
every open set arises as the intersection of a Scott open set with the total
reals, and every such intersection is itself open.

######  Lemma 8.1.

Let $\mathcal{O}\subseteq\mathsf{I}\mathbb{R}$ be Scott-open. Then
$\mathcal{O}\cap\mathbb{R}$ is open.

######  Proof 8.2.

Let $x\in\mathcal{O}\cap\mathbb{R}$. As $x\in\mathcal{O}$, there must exist
$\alpha\in\mathsf{I}\mathbb{Q}$ so that $\mathcal{O}\ni\alpha\ll x$ by Lemma
4.1. As $x=\bigsqcup_{n}x_{n}$ by Lemma 3.2, there must exist $n\in\mathbb{N}$
such that $\alpha\sqsubseteq x_{n}$ and hence $\alpha\ll x_{n}$. By Lemma 2
there exists $\epsilon\in\mathbb{Q}_{>0}$ such that $\alpha\ll
x_{n}\pm\epsilon$. We now claim that all $y\in\mathcal{O}$ whenever
$y\in\mathbb{R}$ with $|x-y|\leq\epsilon$. So pick $y\in\mathbb{R}$ and assume
that $|y-x|\leq\epsilon$. Then $\alpha\ll x_{n}\pm\epsilon\sqsubseteq
x\pm\epsilon\sqsubseteq y$ by Lemma 8.14. Hence $\alpha\ll y$ so that
$y\in\mathcal{O}$.

######  Lemma 8.3.

Let $O\subseteq\mathbb{R}$ be open. Then

$\mathcal{O}=\\{\alpha\in\mathsf{I}\mathbb{R}\mid\tilde{\exists}[p,q]\in\mathsf{I}\mathbb{Q},[p,q]\sqsubseteq\alpha\mbox{
and }[p,q]\subseteq O\\}$

is Scott-open and satisfies $\mathcal{O}\cap\mathbb{R}=O$.

######  Proof 8.4.

We show that $\mathcal{O}$ is Scott-open. First, it is immediate that
$\mathcal{O}$ is an upper set. To see that $\mathcal{O}$ is inacessible by
directed suprema, let $(\alpha_{n})_{n}$ be an increasing sequence in
$\mathsf{I}\mathbb{R}$ with $\bigsqcup_{n}\alpha_{n}\in\mathcal{O}$. This
gives $[p,q]\in\mathsf{I}\mathbb{Q}$ with $[p,q]\sqsubseteq\alpha$ and
$[p,q]\subseteq O$. As $O$ is open, there must exist $\epsilon>0$ and
$\epsilon\in\mathbb{Q}$ with $[p,q]\pm\epsilon\subseteq O$. To see that there
must exist $m\in\mathbb{N}$ with $\alpha_{m}\in\mathcal{O}$, we show that
there must exist $m\in\mathbb{N}$ with
$[p,q]\pm\epsilon\sqsubseteq\alpha_{m}$. Because
$[p,q]\pm\epsilon\ll[p,q]\sqsubseteq\bigsqcup_{n}\alpha_{n}$ this $m$ must
exist, i.e. $m$ must exist with $[p,q]\pm\epsilon\sqsubseteq\alpha_{m}$.

It remains to be seen that $\mathcal{O}\cap\mathbb{R}=O$. Let
$x\in\mathcal{O}\cap\mathbb{R}$. Because $x\in\mathcal{O}$ we have
$[p,q]\in\mathsf{I}\mathbb{Q}$ with $[p,q]\sqsubseteq x$ and
$[p,q]\subseteq\mathcal{O}$. As $O$ is open, this entails that there must
exist $\epsilon>0$ and $\epsilon\in\mathbb{Q}$ such that
$[p,q]\pm\epsilon\subseteq O$. We show that $p-\epsilon\leq x\leq q+\epsilon$
which implies $x\in O$. This follows from $[p,q]\pm\epsilon\ll[p,q]\sqsubseteq
x$. It is clear that $O\subseteq\mathcal{O}\cap\mathbb{R}$.

We state and prove the following technical lemma to help deal with the
Euclidean topology.

######  Lemma 8.5.

Let $a,b\in\mathsf{I}\mathbb{Q}$. Then $a\leq b$ iff $-b\leq-a$ and $|a|\leq
b$ iff $-b\leq a\leq b$ and $0\leq b$.

######  Proof 8.6.

For the first statement, assume that $a\leq b$. Then
$\underline{a}\leq\overline{b}$ whence
$\underline{-b}=-\overline{b}\leq-\underline{a}=\overline{-a}$. If $-b\leq-a$
then $a=--a\leq--b=b$.

For the second statement, first suppose that $|a|\leq b$. We show that
$-\overline{b}=\underline{-b}\leq\overline{a}$ and
$\underline{a}\leq\overline{b}$. We distinguish three cases. If
$0\leq\underline{a}$, then $a=|a|\leq b$ whence
$\underline{a}\leq\overline{b}$ and $-\overline{b}\leq-\underline{a}\leq
0\leq\underline{a}\leq\overline{a}$. Now suppose that $\underline{a}\leq
0\leq\overline{a}$. Then $[0,\max\\{-\underline{a},\overline{a}\\}]=|a|\leq b$
so that $0\leq\overline{b}$. We obtain $-\overline{b}\leq 0\leq\overline{a}$
and $\underline{a}\leq 0\leq\overline{b}$. Finally assume that
$\overline{a}\leq 0$. Then $[-\overline{a},-\underline{a}]=|a|\leq b$ whence
$-\overline{a}\leq\overline{b}$. Then $-\overline{b}\leq\underline{a}$ and
$\underline{a}\leq\overline{a}\leq 0\leq-\underline{a}\leq\overline{b}$. In
all three cases we have that $0\leq\underline{|a|}\leq\overline{b}$ so that
$0\leq b$.

Now assume that $-b\leq a$, $a\leq b$ and $0\leq b$. We show that $|a|\leq b$,
again by distinguishing three cases. If $0\leq\underline{a}$, we have
$|a|=a\leq b$. Similarly, if $\overline{a}\leq 0$, we have $-b\leq a$ and
therefore $|a|=-a\leq--b=b$ using the first statement. Now assume that
$\underline{a}\leq 0\leq\overline{a}$. Then
$|a|=[0,\max\\{-\underline{a},\overline{a}\\}]\leq b$ if $0\leq\overline{b}$
which is precisely our assumption that $0\leq b$.

######  Remark 8.7.

It is in general false that $|a|\leq b$ whenever $-b\leq a\leq b$. To see
this, let $a=[-2,1]$ and $b=-1=[-1,-1]$. Then $-b=[1,1]\leq[-2,1]=a$ and
$a=[-2,-1]\leq[-1,-1]=b$. On the other hand, $|a|=[0,2]\not\leq[-1,-1]=b$.

######  Lemma 8.8.

Let $x,y\in\mathsf{I}\mathbb{R}$. If $x\sqsubseteq y$ then
$\underline{y}_{n}\leq\overline{x}_{m}$ and
$\underline{x}_{m}\leq\overline{y}_{n}$ for all $n,m\in\mathbb{N}$.

######  Proof 8.9.

Suppose that $x\sqsubseteq y$, let $m,n\in\mathbb{N}$ and fix a rational
$\epsilon>0$. Then $x_{m}\pm\epsilon\ll x_{m}$, hence there must exist
$k\in\mathbb{N}$ such that $x_{m}\pm\epsilon\ll y_{k}$. By monotonicity of
$y$, we may assume that $k\geq n,m$. But then
$\underline{x}_{m}-\epsilon=\underline{x_{m}-\epsilon}<\underline{y}_{k}\leq\overline{y}_{k}\leq\overline{y}_{n}$
as $k\geq m$. Similarly
$\underline{y}_{n}\leq\underline{y}_{k}\leq\overline{y}_{k}<\overline{x_{m}\pm\epsilon}=x_{m}+\epsilon$.
The claim follows as $\epsilon$ was arbitrary.

In the following, recall that $\ell([x,y])=y-x$ denotes interval length, and
that we identify rationals $q\in\mathbb{Q}$ with singleton intervals.

######  Lemma 8.10.

Let $w,x,y\in\mathsf{I}\mathbb{R}$ with $w\sqsubseteq x$ and $w\sqsubseteq y$.
Then $|x-y|\leq\ell(w_{n})$ for all $n\in\mathbb{N}$.

######  Proof 8.11.

Let $n,k\in\mathbb{N}$. By Lemma 8.5 it suffices to show that
$-\ell(w_{n})\leq\overline{(x-y)}_{k}=\overline{x}_{k}-\underline{y}_{k}$ and
$\underline{x}_{k}-\overline{y}_{k}=\underline{(x-y)}_{k}\leq\ell(w_{n})$.
This is a consequence of Lemma 8.8, since

$-\ell(w_{n})=\underline{w}_{n}-\overline{w}_{n}\leq\overline{x}_{k}-\overline{w}_{n}\leq\overline{x}_{k}-\underline{y}_{k}$

and similarly,

$\underline{x}_{k}-\overline{y}_{k}\leq\overline{w}_{n}-\overline{y}_{k}\leq\overline{w}_{n}-\underline{w}_{k}$

as required.

######  Lemma 8.12.

Let $x=(x_{n})_{n}\in\mathsf{I}\mathbb{R}$. Then $x\pm\ell(x_{n})\sqsubseteq
x$ for all $n\in\mathbb{N}$.

######  Proof 8.13.

Let $\alpha\in\mathsf{I}\mathbb{Q}$ and $k\in\mathbb{N}$ with $\alpha\ll
x_{k}\pm\ell(x_{n})$. We show that $\alpha\ll x_{n}$. By Lemma 8.8 we have
$\underline{x}_{k}\leq\overline{x}_{n}$ as $x\sqsubseteq x$. Therefore
$\underline{\alpha}<\underline{x}_{k}-(\overline{x}_{n}-\underline{x}_{n})\leq\overline{x}_{n}-\overline{x}_{n}+\underline{x}_{n}=\underline{x}_{n}$.
Analogously one shows that $\overline{x}_{n}<\overline{\alpha}$ so that
$\alpha\ll x_{n}$.

######  Lemma 8.14.

Let $x\in\mathsf{I}\mathbb{R}$, $y\in\mathbb{R}$ be an interval real and
$\epsilon\in\mathbb{Q}_{>0}$. Then $x\pm\epsilon\sqsubseteq y$ whenever
$|x-y|\leq\epsilon$.

######  Proof 8.15.

Let $n\in\mathbb{N}$, $a\in\mathsf{I}\mathbb{Q}$ such that
$a\ll(x\pm\epsilon)_{n}$. We show that there must exist $k\in\mathbb{N}$ such
that $a\ll y_{k}$. By characterisation of $\ll$ on $\mathsf{I}\mathbb{Q}$,
i.e. Lemma 2, there exists $\delta\in\mathbb{Q}_{>0}$ such that
$a\ll(x\pm\epsilon)_{k}\pm\delta$. As $y$ is an interval real, there must
exist $k\in\mathbb{N}$ such that $\ell(y_{k})\leq\delta$. We may assume that
$k\geq n$. As $|x-y|\leq\epsilon$, we have that

$-\epsilon\leq\overline{(x-y)}_{k}=\overline{x}_{k}-\underline{y}_{k}\mbox{
and }\underline{x}_{k}-\overline{y}_{k}=\underline{(x-y)}_{k}\leq\epsilon.$

We obtain that

$\underline{a}<\underline{x}_{n}-\epsilon-\delta\leq\underline{x}_{k}-\epsilon-\delta\leq\overline{y}_{k}-\delta\leq\overline{y}_{k}-w(y_{k})=\underline{y}_{k}$

and one analogously establishes that $\overline{y}_{k}<\overline{a}$ so that
$a\ll y_{k}$.

We characterise Scott continuous total functions in terms of their action on
total reals.

######  Definition 19.

Let $f:\mathbb{R}\to\mathbb{R}$ and $x\in\mathbb{R}$. A _modulus of non-
discontinuity_ of $f$ at $x$ is a sequence $(\delta_{n},\epsilon_{n})_{n}$ in
$\mathbb{Q}_{>0}\times(\mathbb{Q}_{\geq 0}\cup\\{\infty\\})$ such that

  1. (1)

$\forall y\in\mathbb{R}.\,|x-y|\leq\delta_{n}\to|f(x)-f(y)|\leq\epsilon_{n}$
whenever $n\in\mathbb{N}$

  2. (2)

$(\epsilon_{n})_{n}$ is a classical null-sequence.

We say that $f$ is _not discontinuous at $x$_ if there exists a modulus of
non-discontinuity of $f$ at $x$. A _modulus of intensional non-discontinuity_
for $f$ is a function $\omega:\mathsf{I}\mathbb{Q}\to\mathbb{Q}_{>0}$ such
that $(\ell(x_{n}),\omega(x_{n}))_{n}$ is a modulus of non-discontinuity at
$x$ whenever $x\in\mathbb{R}$ is total. A function $f$ is _intensionally non-
discontinuous_ if there exists a modulus of intensional non-discontinuity for
$f$. The function $f$ is _continuous_ at $x$ if, for all
$\epsilon\in\mathbb{Q}_{>0}$ there exists $\delta\in\mathbb{Q}_{>0}$ such that
for all $y$ with $|x-y|\leq\delta$ we have $|f(x)-f(y)|\leq\epsilon$.

######  Remark 8.16.

It is evident that every function that is intensionally non-discontinuous is
non-discontinuous at every $x\in\mathbb{R}$. The converse is not necessarily
due to the uniformity requirement.

######  Lemma 8.17.

If $f:\mathbb{R}\to\mathbb{R}$ is continuous at $x$, then $f$ is non-
discontinuous at $x$.

######  Proof 8.18.

As $f$ is continuous at $x$, there exists a function
$\delta:\mathbb{Q}_{>0}\to\mathbb{Q}_{\geq 0}$ such that $\forall
n\in\mathbb{N}.\,\forall
y\in\mathbb{R}.\,|y-x|\leq\delta(2^{-n})\to|f(x)-f(y)|\leq 2^{-n}$. Hence the
sequence $(\delta(2^{-n}),2^{-n})_{n}$ is a modulus of non-discontinuity for
$f$ at $x$.

######  Lemma 8.19.

If every (total) function $f:\mathbb{R}\to\mathbb{R}$ that is non-
discontinuous at $0$ is in fact continuous at $0$, then Markov’s principle
holds.

######  Proof 8.20.

Let $P(n)$ be a decidable predicate on natural numbers and assume that
$\neg\forall n\in\mathbb{N}.\,\neg P(n)$. We show that there exists
$n\in\mathbb{N}$ such that $P(n)$ under the assumption that every function
that is non-discontinuous at $0$ is in fact continuous at $0$. Consider, for
$n\in\mathbb{N}$, the function
$f_{n}:\mathsf{I}\mathbb{R}\to\mathsf{I}\mathbb{R}_{\bot}$ defined by

$f_{n}(x)=\begin{cases}\bot&\forall n\leq k.\,\neg P(k)\\\ x\cdot\min\\{k\leq
n\mid P(n)=1\\}&\exists k\leq n.\,P(k)\end{cases}$

and let $f=\bigsqcup_{n}f_{n}$. Clearly $(f_{n})_{n}$ is monotone so that
$\bigsqcup_{n}f_{n}$ exists, and $\bigsqcup_{n}f_{n}$ defines a total function
with $f(0)=0$. We claim that the sequence $(\epsilon_{n},\delta_{n})$ defined
by $\delta_{n}=\frac{1}{n^{2}}$ and

$\epsilon_{n}=\begin{cases}\infty&\forall k\leq n.\,\neg P(k)\\\
\frac{1}{n}&\exists k\leq n.\,P(k)\end{cases}$

is a modulus of non-discontinuity for $f$ at $0$. To see this, let
$n\in\mathbb{N}$. If $\forall k\leq n.\,\neg P(n)$, then $\epsilon_{n}=\infty$
and there is nothing to show. So assume that $\exists k\leq n.\,P(n)$ and
$|y-0|\leq\delta_{n}=\frac{1}{n^{2}}$. Then
$|f(y)-f(0)|=|f(y)|=|y|\cdot\min\\{k\leq n\mid P(n)\\}\leq|y|\cdot
n\leq\delta_{n}\cdot n=\frac{1}{n^{2}}\cdot n=\frac{1}{n}=\epsilon_{n}$.

By assumption, $f$ is also continuous at $0$, hence for $\epsilon=1$ there
exists $\delta$ such that for all $y$ with $|y|=|y-0|\leq\delta$ we have
$|f(y)|=|f(y)-f(0)|\leq 1$. As $\delta\in\mathbb{Q}_{>0}$ there exists $n$
such that $n\geq\frac{1}{\delta}$. We claim that there exists $k\leq n$ such
that $P(k)$. As this property is decidable, we may assume that $\neg P(k)$ for
all $k\leq n$, and establish a contradiction to prove the claim. By
assumption, we have $\neg\forall k\neg P(k)$ so that it suffices to show that
$\forall k.\,\neg P(k)$ to establish the desired contradiction. So let
$k\in\mathbb{N}$, we need to show $\neg P(k)$ to prove the claim. If $k\leq n$
then $\neg P(k)$ is given. Now let $k>n$. As $P$ is decidable, we may assume
$P(k)$ and establish a contradiction to show that $\neg P(k)$. So assume that
$P(k)$. Then $f(y)=\min\\{k^{\prime}\leq k\mid P(k^{\prime})\\}\cdot x$.

We now use that for $y=\delta$, we have that $|fy|=\min\\{k^{\prime}\leq k\mid
P(k^{\prime})\\}\cdot\delta\leq 1$ so that $\min\\{k^{\prime}\leq k\mid
P(k^{\prime})\\}\leq\frac{1}{\delta}\leq k$ so that there exists
$k^{\prime}\leq k$ with $P(k)$, contradiction.

The following lemma shows that equality is stable under adding classical null-
sequences. Again, this is a consequence of the classical formulation of
equality on reals.

######  Lemma 8.21.

Let $x=(x_{n})\in\mathsf{I}\mathbb{R}$ and let $(q_{n})$ be a classical null
sequence. If $y=(x_{n}\pm q_{n})$, then $x=y$.

######  Proof 8.22.

We establish that $(x_{n}\pm q_{n})_{n}\sqsubseteq(x_{n})_{n}$ and
$(x_{n})_{n}\sqsubseteq(x_{n}\pm q_{n})_{n}$. The first relation is immediate
using the Definition 5, for if $\alpha\ll x_{n}\pm q_{n}$, we have $\alpha\ll
x_{n}\pm q_{n}\sqsubseteq x_{n}$ whence $\alpha\ll x_{n}\pm q_{n}$ by Lemma 2.
For the second (converse) relation, assume that $\alpha\ll x_{n}$. Using Lemm
2, there exits $\epsilon\in\mathbb{Q}$ with $\epsilon>0$ and $\alpha\ll
x_{n}\pm\epsilon$. As $(q_{n})_{n}$ is a classical null sequence, there must
exist $m\in\mathbb{N}$ such that $q_{m}<\epsilon$. For $k=\max\\{n,m\\}$ we
therefore obtain that $\alpha\ll x_{n}\pm\epsilon\sqsubseteq x_{k}\pm q_{k}$
as required.

######  Lemma 8.23.

Suppose that $f:\mathsf{I}\mathbb{R}\to\mathsf{I}\mathbb{R}$ is Scott
continuous and total. Then $f\restriction\mathbb{R}$ is intensionally non-
discontinuous.

######  Proof 8.24.

Fix an antitone function $b:\mathbb{Q}_{>0}\to\mathbb{N}$ such that
$2^{-b(q)}\leq q$ and let $s(\alpha)=b(\ell(\alpha))$ for
$\alpha\in\mathsf{I}\mathbb{Q}$ with $\ell(\alpha)>0$. Then $s$ is antitone
with respect to interval length, i.e. $0<\ell(\alpha)\leq\ell(\beta)$ implies
$s(\alpha)\geq s(\beta)$ for all $\alpha,\beta\in\mathsf{I}\mathbb{Q}$.

By the approximation lemma (Lemma 5.47) we have that $f=\bigsqcup_{n}f_{n}$ is
a supremum of step functions. Define
$\omega:\mathsf{I}\mathbb{Q}\to\mathbb{Q}_{\geq 0}\cup\\{\infty\\}$ by
$\omega(\alpha)=\ell(f_{s(\alpha)}(\alpha\pm\ell(\alpha)))$. We show that
$\omega$ is a modulus of intensional non-discontinuity for $f$.

Let $x\in\mathbb{R}$ be given. We first show that $\omega(x_{n})_{n}$ is a
classical null-sequence. Let $y_{n}=x_{n}\pm\ell(x_{n})$. Then $x=y$ by Lemma
8.21 and $y=\bigsqcup_{n}y_{n}$ by Lemma 3.2. Then
$f(x)=f(\bigsqcup_{m}y_{m})=\bigsqcup_{m}f(y_{m})=\bigsqcup_{m}\bigsqcup_{n}f_{n}(y_{m})=\bigsqcup_{n}f_{n}(y_{n})$
by Corollary 4, and applying Lemma 3.2 this gives that
$f(x)=(f_{n}(y_{n}))_{n}$ as a sequence. Now let $\epsilon>0$. As $f(x)$ is
total and $f(x)=(f_{n}(y_{n}))_{n}$, there must exist $k\in\mathbb{N}$ such
that $\ell(f_{k}(y_{k}))\leq\epsilon$. By definition of $s$, there moreover
must exist $i\in\mathbb{N}$ such that $s(x_{i})\geq k$. As $s$ is antitone
with respect to interval length and $(y_{n})_{n}$ is increasing, we may assume
that $i\geq k$. Then
$\omega(x_{i})=\ell(f_{s(x_{i})}(y_{i}))\leq\ell(f_{k}(y_{i}))\leq\ell(f_{k}(y_{k}))\leq\epsilon$
as required.

We now show that $(\ell(x_{n}),\omega(x_{n}))_{n}$ is a modulus of non-
discontinuity of $f$ at $x$. So let $n\in\mathbb{N}$ and fix $y\in\mathbb{R}$
with $|x-y|\leq\ell(x_{n})$. Then $x_{n}\pm\ell(x_{n})\sqsubseteq
x\pm\ell(x_{n})\sqsubseteq y$ by Lemma 8.14, and therefore
$f(x_{n}\pm\ell(x_{n}))\sqsubseteq f(y)$. As also
$x_{n}\pm\ell(x_{n})\sqsubseteq x\pm\ell(x_{n})\sqsubseteq x$ we have, again
by monotonicity of $f$, that $f(x_{n}\pm\ell(x_{n}))\sqsubseteq f(y)$. As
$f_{s(x_{n})}\sqsubseteq f$, this gives
$f_{s(x_{n})}(x_{n}\pm\ell(x_{n}))\sqsubseteq f(x)$ and
$f_{s(x_{n})}(x\pm\ell(x_{n}))\sqsubseteq f(y)$. By Lemma 8.10 we may conclude
that $|f(x)-f(y)|\leq\ell(f_{s(x)}(x\pm\ell(x_{n}))=\omega(x_{n})$ which
finishes the proof.

######  Theorem 20.

Suppose that $f:\mathbb{R}\to\mathbb{R}$ is intensionally non-discontinuous.
Then there exists a Scott continuous function
$g:\mathsf{I}\mathbb{R}\to\mathsf{I}\mathbb{R}_{\bot}$ such that
$g\restriction\mathbb{R}=f$.

######  Proof 8.25.

Let $\omega$ be a modulus of intensional non-discontinuity for $f$ and suppose
that $\mathsf{I}\mathbb{Q}=\\{\alpha_{i}\mid i\in\mathbb{N}\\}$ is an
enumeration of $\mathsf{I}\mathbb{Q}$. For $\alpha\in\mathsf{I}\mathbb{Q}$ let
$m(\alpha)=\frac{1}{2}(\underline{\alpha}+\overline{\alpha})$ denote the
midpoint of $\alpha$. Put

$g_{n}=\bigsqcup_{i\leq n}\alpha_{i}$

and let $g=\bigsqcup_{n}g_{n}$.

We first show that $g_{n}$ is well-defined for all $n\in\mathbb{N}$, i.e.
satisfies the consistency requirement for step functions. To see this, let
$I\subseteq\mathbb{N}$ be finite and suppose that $\\{\alpha_{i}\mid i\in
I\\}$ is consistent. We show that $f(m(\alpha_{i}))_{k}\pm\omega(\alpha_{i})$
are consistent for arbitrary $k\in\mathbb{N}$. The claim follows for $k=\max
I$. By consistency of $\\{\alpha_{i}\mid i\in I\\}$ we obtain $q\in\mathbb{Q}$
such that $\alpha_{i}\sqsubseteq q$ for all $i\in I$, e.g.
$q=\\{\max\underline{\alpha}_{i}\mid i\in I\\}$. We now obtain that
$\alpha_{i}=m(\alpha_{i})\pm\frac{1}{2}\ell(\alpha_{i})\sqsubseteq q$ and
$\alpha_{i}\sqsubseteq m(\alpha_{i})$, hence by Lemma 8.10 we obtain
$|q-m(\alpha_{i})|\leq\frac{1}{2}\ell(\alpha_{i})$. As $\omega$ is a modulus
of intensional non-discontinuity for $f$, this gives
$|f(q)-f(m(\alpha_{i})|\leq\omega(\alpha_{i})$. By Lemma 8.14 this gives
$f(m(\alpha_{i}))\pm w(\alpha_{i})\sqsubseteq f(q)$. As
$f(m(\alpha_{i}))_{k}\pm\omega(\alpha_{i})\pm 2^{-n}\ll
f(m(\alpha_{i}))_{k}\pm\omega(\alpha_{i})$ and
$f(m(\alpha_{i}))\pm\omega(\alpha_{i})\sqsubseteq f(q)$, there must exist
$r(i)$ such that $f(m(\alpha_{i}))_{k}\pm\omega(\alpha_{i})\pm 2^{-n}\ll
f(q)_{r(i)}$. For $r=\max\\{r(i)\mid i\in I\\}$ we therefore have
$f(m(\alpha_{i}))\pm w(\alpha_{i})\pm 2^{-n}\ll f(q)_{r}$, that is, the set
$\\{f(m(\alpha_{i}))_{k}\pm\omega(\alpha_{i})\pm 2^{-n}\mid i\in I\\}$ is
consistent for all $n\in\mathbb{N}$. As consistency on $\mathsf{I}\mathbb{Q}$
is continuous by Lemma 2 this shows that
$\\{f(m(\alpha_{i}))_{k}\pm\omega(\alpha_{i})\mid i\in I\\}$ is consistent.

We now demonstrate that $g$ preserves total reals, that is, $g(x)$ is total
whenever $x$ is. Let $x\in\mathbb{R}$ be total and $y_{n}=x_{n}\pm 2^{-n}$.
Then, for every $n\in\mathbb{N}$ there must exist

  * $\triangleright$

$i\in\mathbb{N}$ such that $\omega(y_{i})\leq\frac{\epsilon}{4}$

  * $\triangleright$

$j\in\mathbb{N}$ such that $y_{i}\in\\{\alpha_{i}\mid i\leq j\\}$

  * $\triangleright$

$k\in\mathbb{N}$ such that $\ell(f(m(y_{i}))_{k})\leq\frac{\epsilon}{2}$

so that for $l=\max\\{i,j,k\\}$ we have:

$\displaystyle g(x)$ $\displaystyle\sqsupseteq g_{l}(x_{i})$ (as
$g_{l}=\sqsubseteq\bigsqcup_{n}g_{n}=g$ and
$x_{i}\sqsubseteq\bigsqcup_{n}x_{n}=x$) $\displaystyle\sqsupseteq(y_{i}$ (as
$y_{i}\in\\{\alpha_{i}\mid i\leq j\\}\subseteq\\{\alpha_{i}\mid i\leq k\\}$)
$\displaystyle=f(m(y_{i}))_{l}\pm\omega(y_{i})$ (definition of step functions)
$\displaystyle\sqsupseteq f(m(y_{i}))_{k}\pm\omega(y_{i})$ (monotonicity of
$f(m(y_{i}))$ and $k\leq l$)

In particular, this gives that

$\ell(g(x))\leq\ell(f(m(y_{i}))_{l}\pm\omega(y_{i}))\leq\ell(f(m(y_{i}))_{l})+2\omega(y_{i})\leq\frac{\epsilon}{2}+2\frac{\epsilon}{4}=\epsilon$

as required.

We finally demonstrate that $g(x)\sqsubseteq f(x)$ for $x\in\mathbb{R}$. As
$g(x)=\bigsqcup_{n}g_{n}(x_{n})$, it suffices to show that
$g_{n}(x_{n})\sqsubseteq f(x)$. So let $n\in\mathbb{N}$. Then
$g_{n}(x)=\bigsqcup\\{f(m(\alpha_{i}))_{n}\pm\omega(\alpha_{i})\mid 0\leq
i\leq n,\alpha_{i}\ll x_{n}\\}$ so that the claim follows once we show that
$f(m(\alpha)_{n}\pm\omega(\alpha)\sqsubseteq f(x)$ whenever
$\alpha\in\mathsf{I}\mathbb{Q}$ with $\alpha\ll x_{n}$. So assume that
$\alpha\ll x_{n}$ so that in particular $\alpha\sqsubseteq x$. As also
$\alpha\sqsubseteq m(\alpha)$ we have that $|x-\alpha|\leq\ell(\alpha)$ by
Lemma 8.10. As $\omega$ is a modulus of intensional non-discontinuity, this
gives $|f(x)-f(m(\alpha))|\leq\omega(\alpha)$ and in turn, using Lemma 8.14
that $f(m(\alpha))\pm\omega(\alpha)\sqsubseteq f(x)$. Using monotonicity of
$f(m(\alpha))$ we obtain $f(m(\alpha))_{n}\pm\omega(\alpha)\sqsubseteq f(x)$
as required.

We now finish the proof by showing that $f(x)=g(x)$ whenever $x\in\mathbb{R}$
is total. But this follows from $g(x)$ being maximal by Lemma 6.3 and the fact
that $g(x)\sqsubseteq f(x)$.

##  9\. Conclusion and Discussion

The main guiding principle of our development here was “constructive existence
with classical correctness”. The main goal was to constructively rationalise
standard practice in constructive analysis: constructions are carried out in
the universe of classical mathematics, and then a secondary argument is used
to show that they are in fact effective. This is reflected in our approach
that emphasises constructive existence, but contends itself with classical
correctness arguments. One consequence of this is that correctness assertions
have no computational content under a realisability interpretation. While this
can also be achieved by achieved using different methods (e.g. non-
computational quantifiers [Ber93a] or $\mathrm{Prop}$-valued assertions in the
calculus of constructions [CH88]), we consciously took a pragmatic approach
that aligns with computable analysis. As next step, our approach should be
benchmarked both mathematically (e.g. by establishing standard results of
computable analysis as carried out e.g. in [Sch08]) and experimentally, by
implementing our theory in a theorem prover such as Coq [BCHPM04] or Minlog
[SW12].

## Acknowledgments

The authors wish to express their gratitude to Helmut Schwichtenberg, Dieter
Spreen and Andrej Bauer for continued discussions about the topic, and to the
anonymous reviwers for their constructive suggestions to improve the paper. We
also acknowledge the support of a visiting scholarship by the Humboldt
Foundation.

## References

  * [AJ94] S. Abramsky and A. Jung.  Domain Theory.  In S. Abramsky, D. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3. Clarendon Press, 1994.
  * [BB85] E. Bishop and D. Bridges.  Constructive Analysis.  Number 279 in Grundleheren der mathematischen Wissenschaften. Springer, 1985.
  * [BCHPM04] Y. Bertot, P. Castéran, Gérard Huet, and Christine Paulin-Mohring.  Interactive theorem proving and program development : Coq’Art : the calculus of inductive constructions.  Texts in theoretical computer science. Springer, 2004.
  * [Ber93a] U. Berger.  Program extraction from normalization proofs.  In Marc Bezem and Jan Friso Groote, editors, Proc. TLCA 1993, volume 664 of Lecture Notes in Computer Science, pages 91–106. Springer, 1993.
  * [Ber93b] U. Berger.  Total Sets and Objects in Domain Theory.  Journal of Pure and Applied Logic, 60:91–117, 1993.
  * [Ber11] U. Berger.  From coinductive proofs to exact real arithmetic: theory and applications.  Logical Methods in Computer Science, 7(1), 2011.
  * [BK09] A. Bauer and I. Kavkler.  A constructive theory of continuous domains suitable for implementation.  Ann. Pure Appl. Logic, 159(3):251–267, 2009.
  * [CH88] T. Coquand and G. P. Huet.  The calculus of constructions.  Inf. Comput, 76(2/3):95–120, 1988.
  * [dG97] P. di Gianantonio.  Real number computation and domain theory.  Information and Computation, 127:11–25, 1997.
  * [ES98] A. Edalat and P. Sünderhauf.  A domain theoretic approach to computability on the real line.  Theoretical Computer Science, 210:73–98, 1998.
  * [ES99] A. Edalat and P. Sünderhauf.  A domain-theoretic approach to computability on the real line.  Theor. Comput. Sci., 210(1):73–98, 1999.
  * [HE02] R. Heckmann and A. Edalat.  Computing with real numbers: I. the LFT approach to real number computation; II. A domain framework for computational geometry.  In G. Barthe, P. Dybjer, L. Pinto, and J. Saraiva, editors, Applied Semantics - Lecture Notes from the International Summer School, volume 2395 of LNCS. Springer, 2002.
  * [Ish92] H. Ishihara.  Continuity properties in constructive mathematics.  Symbolic Logic, 57(2):557–565, 1992.
  * [ME07] J. R. Marcial-Romero and M. H. Escardó.  Semantics of a sequential language for exact real-number computation.  Theor. Comput. Sci., 379(1–2):120–141, 2007.
  * [Sch08] H. Schwichtenberg.  Realizability interpretation of proofs in constructive analysis.  Theory Comput. Syst., 43(3-4):583–602, 2008.
  * [Sch16] H. Schwichtenberg.  Constructive analysis with witnesses.  Unpublished notes, avaliable at http://www.math.lmu.de/~schwicht/seminars/semws16/constr16.pdf, 2016.
  * [SW12] H. Schwichtenberg and S. Wainer.  Proofs and Computations.  Cambridge University Press, 2012.
  * [TvD88] A. Troelstra and Dirk van Dalen.  Constructivisim in mathematics: an introduction.  North Holland, 1988.  Two volumes.
  * [Wei00] K. Weihrauch.  Computable Analysis.  Springer, 2000.