application of Section 5.1.4 wherein we show
$\mathsf{affine}(-(y^{\prime}\oplus z^{\prime}),y^{\prime}\oplus
z^{\prime})=\lambda x.(y^{\prime}*x)\oplus(z^{\prime}*x)$. Therefore, we must
now show that (1) $(y^{\prime}*-1)\oplus(z^{\prime}*-1)=-(y^{\prime}\oplus
z^{\prime})$, (2) $(y^{\prime}*+1)\oplus(z^{\prime}*+1)=(y^{\prime}\oplus
z^{\prime})$ and (3) $\mathsf{is{\text{-}}midpoint{\text{-}}hom}(\lambda
x.(y^{\prime}*x)\oplus(z^{\prime}*x)$.

For the first condition, by Section 5.1.5.(i) and (iii) we have that
$(y^{\prime}*-1)\oplus(z^{\prime}*-1)=(-y^{\prime}\oplus-z^{\prime})=-(y^{\prime}\oplus
z^{\prime})$. For the second, by Section 5.1.5.(ii) we have that
$(y^{\prime}*+1)\oplus(z^{\prime}*+1)=(y^{\prime}\oplus z^{\prime})$. The
third is again more complicated: given any $a,b\colon\mathbb{I}$, the result
is given by the following equational reasoning:

$\displaystyle(x*(a\oplus b))\oplus(y*(a\oplus b)),$ $\displaystyle=$
$\displaystyle((x*a)\oplus(x*b))\oplus(y*(a\oplus b))$ $\displaystyle\text{by
\lx@cref{creftype~refnum}{lem:mul-props}.(iii)},$ $\displaystyle=$
$\displaystyle((x*a)\oplus(x*b))\oplus((y*a)\oplus(y*b))$
$\displaystyle\text{by \lx@cref{creftype~refnum}{lem:mul-props}.(iii)},$
$\displaystyle=$ $\displaystyle((x*a)\oplus(y*a))\oplus((x*b)\oplus(y*b))$
$\displaystyle\text{by trans. of $\oplus$
(\lx@cref{creftype~refnum}{def:mpa})}.$

[ ] Multiplication on $\mathbb{I}$ satisfies $((x\oplus
y)*z)=(x*z)\oplus(y*z)$.

###### Proof.

By Sections 5.1.5 and 5.1.3.

######  Theorem 5.1.4.

[ ]  Multiplication on $\mathbb{I}$ is associative.

The proof that multiplication is associative has a similar proof technique as
the proof of commutativity (Theorem 5.1.3). For the full details, we invite
the interested reader to view the formalisation.

###  5.2 Verified ternary signed-digit encodings

####  5.2.1 Background and definition in our type theory

Boehm et al.’s early paper on exact real arithmetic explores multiple
representations of real numbers, one of which is an approach where a real
number is represented by an infinitary sequence of digits [BCRO86].

The idea is that a (base $2$) _digit encoding_ of a real number in the compact
interval $[0,d]$ (for some $d\colon\mathbb{N}$) is an infinitary seqeuence of
digits $\alpha\colon\\{0,...,d\\}^{\mathbb{N}}$. The real number represented
by such a digit encoding $\llbracket\alpha\rrbracket\colon[0,d]$ is defined
by,

$\llbracket\alpha\rrbracket:=\sum_{n=0}^{\infty}\frac{\alpha_{i}}{2^{n+1}}.$

For example, with $d:=2$, $\llbracket\\{0,2,0,2,0,...\\}\rrbracket=0.666...$
and $\llbracket\\{0,1,0,1,0,...\\}\rrbracket=0.333...$. This approach is
problematic, however, as even addition is not definable [BCRO86]. An
illuminating example is the addition of the two above realisers of $0.666...$
and $0.333...$. Computing only the first digit of the output requires the
function to look at an infinite number of digits of the input, because (for
example)
$\llbracket\\{0,2,0,2,0,...\\}\rrbracket+\llbracket\\{0,1,0,1,0,...,0,0,0,...\\}\rrbracket=0.9...$,
whereas
$\llbracket\\{0,2,0,2,0,...\\}\rrbracket+\llbracket\\{0,1,0,1,0,...,0,2,0,...\\}\rrbracket=1.0...$.

However, the _signed-digit encoding_ representation does not have this
problem. A signed-digit encoding of a real number in a compact interval
$[-d,d]$ (for some $d\colon\mathbb{N}$) is an infinitary sequence of digits
$\alpha\colon\\{-d,...,d\\}^{\mathbb{N}}$. The real number represented by such
a signed-digit encoding $\llbracket\alpha\rrbracket\colon\mathbb{R}$ is
defined by,

$\llbracket\alpha\rrbracket:=\sum_{n=0}^{\infty}\frac{\alpha_{n}}{2^{n+1}},$

which can be infinitely unfolded using a midpoint operator $x\oplus
y:=\frac{x+y}{2}$:

$\llbracket\alpha\rrbracket:=\alpha_{0}\oplus(\alpha_{1}\oplus(\alpha_{2}\oplus...)).$

This representation of the reals uses extra ‘redundant’ digits than is
necessary for representing each number in the interval. The redundant digits,
however, are what enable addition (and multiplication) to be defined at the
expense of having multiple representations for the same real number. In the
previous addition example, the second item of the sequence could have been set
as $2$ and then, if necessary, corrected by negative digits later [Plu98]
[Esc11a].

In this section, we recall the type of _ternary signed-digit encodings_ of
real numbers in the compact interval $[-1,1]$, as extensively explored in the
literature of exact real arithmetic [Di ̵93, Plu98, Ber09]. Every real number
in $[-1,1]$ can be represented by a function of type
$\mathbb{N}\to\\{-1,1\\}$, but by using the redundant representation
$\mathbb{N}\to\\{-1,0,1\\}$ we can perform exact real arithmetic on
representations of this compact interval.

Our formalisation is based on Escardó’s Haskell library for exact real
computation on ternary signed-digits [Esc11a]. We first convert his
definitions of various arithmetic functions to Agda, which is non-trivial as
we must convince Agda’s termination checker. Following this, we verify the
correctness of his algorithms using the interval object seen in Section 5.1,
showing that they encode the correct operations on the real numbers.

[ ] The type of _ternary digits_ $\mathbb{3}$, equivalent to
$\mathsf{Fin}(3)$, is defined by its elements
$\overline{1},0,1\colon\mathbb{3}$.

[ ] A _ternary signed-digit encoding_ of a real number in $[-1,1]$ is any
function $\alpha\colon\mathbb{3}^{\mathbb{N}}$.

####  5.2.2 Representation via the interval object

A _representation map_ takes a representation of a real to the real that it
represents.

[ ] [ ] [ ] Given a type of real numbers $\mathbb{R}$, a type for representing
reals $K$ and a representation map $\llbracket-\rrbracket\colon
K\to\mathbb{R}$, the $n$-ary function $\overline{f}\colon K^{n}\to K$ (for
$n\colon\mathbb{N}$) _realises_ a function
$f\colon\mathbb{R}^{n}\to\mathbb{R}$ if,

$\prod_{\left((x_{0},...,x_{n-1})\colon
K^{n}\right)}\llbracket\overline{f}\left(x_{0},...,x_{n-1}\right)\rrbracket=f\left(\llbracket
x_{0}\rrbracket,...,\llbracket x_{n-1}\rrbracket\right).$

The idea here is that in order to verify $\overline{f}\colon K^{n}\to K$
realises $f\colon\mathbb{R}\to\mathbb{R}$, using the representation map
$\llbracket-\rrbracket\colon K\to\mathbb{R}$, we show that the diagram in
Figure 5.2 commutes.

${{K^{n}}}$${{K}}$${{\mathbb{R}^{n}}}$${{\mathbb{R}}}$$\scriptstyle{\overline{f}}$$\scriptstyle{f}$$\scriptstyle{\llbracket-\rrbracket\
\times\ ...\ \times\
\llbracket-\rrbracket}$$\scriptstyle{\llbracket-\rrbracket}$ Figure 5.2:
Commutative diagram illustrating Section 5.2.2.

The identity map always has a realiser, and the composition of two realisers
is a realiser of the composition of the two realised functions; i.e. the
diagrams in Figure 5.3 commute.

floatrowfigurerowb
${{K}}$${{K}}$${{\mathbb{R}}}$${{\mathbb{R}}}$$\scriptstyle{\mathsf{id}_{K}}$$\scriptstyle{\mathsf{id}_{\mathbb{R}}}$$\scriptstyle{\llbracket-\rrbracket}$$\scriptstyle{\llbracket-\rrbracket}$
${K}$${K}$${K}$${\mathbb{R}}$${\mathbb{R}}$${\mathbb{R}}$$\scriptstyle{\overline{f}}$$\scriptstyle{f}$$\scriptstyle{\llbracket-\rrbracket}$$\scriptstyle{\llbracket-\rrbracket}$$\scriptstyle{g}$$\scriptstyle{\overline{g}}$$\scriptstyle{\llbracket-\rrbracket}$

Figure 5.3: Commutative diagrams illustrating Sections 5.2.2 and 5.2.2.

[ ] [ ] The identity map is realised by the identity map, and composition
preserves realisers.

###### Proof.

For the identity map, we need to show that for all $k\colon K$ we have
$\llbracket\mathsf{id}_{K}(k)\rrbracket=\mathsf{id}_{\mathbb{R}}\left(\llbracket
k\rrbracket\right)$; this is clearly the case by reflexivity. For composition
of functions $\overline{f},\overline{g}\colon K\to K$, which realise
$f,g\colon\mathbb{R}\to\mathbb{R}$ respectively, we want to show that
$\llbracket\overline{g}(\overline{f}(k))\rrbracket=g(f(\llbracket
k\rrbracket))$. This is the case because
$\llbracket\overline{g}(\overline{f}(k))\rrbracket=g(\llbracket\overline{f}(x)\rrbracket)$
(because $\overline{f}$ realises $f$) and then
$g(\llbracket\overline{f}(x)\rrbracket)=g(f(\llbracket k\rrbracket))$ (because
$\overline{g}$ realises $g$).

We define the _representation map_ for ternary signed-digit encodings, which
maps such encodings of reals in $[-1,1]$ to the numbers they represent on the
interval object $\mathbb{I}$, using the infinitary midpoint operator
$M\colon\mathbb{I}^{\mathbb{N}}\to\mathbb{I}$.

[ ] We define the _representation map_ from ternary digits $\mathbb{3}$ to the
interval object $\mathbb{I}$,

$\displaystyle\langle-\rangle$ $\displaystyle:\mathbb{3}\to\mathbb{I},$
$\displaystyle\langle\overline{1}\rangle$ $\displaystyle:=-1,$
$\displaystyle\langle 0\rangle$ $\displaystyle:=0,$ $\displaystyle\langle
1\rangle$ $\displaystyle:=+1,$

[ ] We define the _representation map_ from ternary signed-digit encodings
$\mathbb{3}^{\mathbb{N}}$ to the interval object $\mathbb{I}$,

$\displaystyle\langle\langle-\rangle\rangle$
$\displaystyle:{\mathbb{3}^{\mathbb{N}}}\to\mathbb{I},$
$\displaystyle\langle\langle\alpha\rangle\rangle$
$\displaystyle:=M(\mathsf{map}(\langle-\rangle,\alpha)).$

In order to verify that an operation on ternary digits
$\overline{f^{\prime}}\colon\mathbb{3}^{n}\to\mathbb{3}$ or one on ternary
signed-digit encodings
$\overline{f}\colon({\mathbb{3}^{\mathbb{N}}})^{n}\to{\mathbb{3}^{\mathbb{N}}}$
correctly realises an operation on the interval object
$f\colon\mathbb{I}^{n}\to\mathbb{I}$, we will show that the diagrams in Figure
5.4 commute.

floatrowfigurerowb
${{\mathbb{3}^{n}}}$${{\mathbb{3}}}$${{\mathbb{I}^{n}}}$${{\mathbb{I}}}$$\scriptstyle{\overline{f^{\prime}}}$$\scriptstyle{f}$$\scriptstyle{\langle-\rangle^{n}}$$\scriptstyle{\langle-\rangle}$
${(\mathbb{3}^{\mathbb{N}})^{n}}$${\mathbb{3}^{\mathbb{N}}}$${\mathbb{I}^{n}}$${\mathbb{I}}$$\scriptstyle{\overline{f}}$$\scriptstyle{f}$$\scriptstyle{\langle\langle-\rangle\rangle^{n}}$$\scriptstyle{\langle\langle-\rangle\rangle}$

Figure 5.4: Commutative diagrams illustrating Section 5.2.2 (which is itself
illustrated in Figure 5.2) using the representation maps defined in Section
5.2.2 (left) and Section 5.2.2 (right).

####  5.2.3 Exact real arithmetic

##### Negation

Negation on signed-digit encodings is straightforward to define — we simply
flip every digit of the sequence.

[ ] [ ] We first define the negation function $\mathsf{flip}$ on ternary
digits in the expected way:

$\displaystyle\mathsf{flip}$ $\displaystyle:\mathbb{3}$
$\displaystyle\to\mathbb{3},$ $\displaystyle\mathsf{flip}$
$\displaystyle(\overline{1})$ $\displaystyle:=1,$ $\displaystyle\mathsf{flip}$
$\displaystyle(0)$ $\displaystyle:=0,$ $\displaystyle\mathsf{flip}$
$\displaystyle(1)$ $\displaystyle:=\overline{1}.$

Then, the negation function $\mathsf{neg}$ on ternary signed-digit encodings
is defined as follows:

$\displaystyle\mathsf{neg}$ $\displaystyle:{\mathbb{3}^{\mathbb{N}}}$
$\displaystyle\to{\mathbb{3}^{\mathbb{N}}},$ $\displaystyle\mathsf{neg}$
$\displaystyle(x)$ $\displaystyle:=\mathsf{map}(\mathsf{flip},x).$

We then verify these operations; i.e. we show that the following diagrams
commute.

floatrowfigurerowb
${{\mathbb{3}}}$${{\mathbb{3}}}$${{\mathbb{I}}}$${{\mathbb{I}}}$$\scriptstyle{\mathsf{flip}}$$\scriptstyle{-}$$\scriptstyle{\langle-\rangle}$$\scriptstyle{\langle\langle-\rangle\rangle}$
${\mathbb{3}^{\mathbb{N}}}$${\mathbb{3}^{\mathbb{N}}}$${\mathbb{I}}$${\mathbb{I}}$$\scriptstyle{\mathsf{neg}}$$\scriptstyle{\oplus}$$\scriptstyle{\langle\langle-\rangle\rangle}$$\scriptstyle{\langle\langle-\rangle\rangle}$

Figure 5.5: Commutative diagrams illustrating Section 5.2.3 (left) and Theorem
5.2.1 (right).

[ ] The negation function on ternary digits realises the negation function on
the interval object.

###### Proof.

We prove $\langle\mathsf{flip}(t)\rangle=-\langle t\rangle$ by case splitting
on the given $t\colon\mathbb{3}$. In the $t:=0$ case, we show $\langle
0\rangle=-\langle 0\rangle$ by Section 5.1.5. In the other two cases, the
proof follows by the mapping of the endpoints in Section 5.1.5.

In order to verify negation on signed-digit encodings, we use the fact that
the $\mathsf{map}$ function preserves a realiser; this is illustrated by the
diagram in Figure 5.6.

floatrowfigurerowb
${\mathbb{3}}$${\mathbb{3}}$${\mathbb{I}}$${\mathbb{I}}$$\scriptstyle{\langle-\rangle}$$\scriptstyle{f}$$\scriptstyle{\langle-\rangle}$$\scriptstyle{\overline{f}}$
$\Longrightarrow$
${\mathbb{3}^{\mathbb{N}}}$${\mathbb{3}^{\mathbb{N}}}$${\mathbb{I}}$${\mathbb{I}}$$\scriptstyle{\langle\langle-\rangle\rangle}$$\scriptstyle{f}$$\scriptstyle{\langle\langle-\rangle\rangle}$$\scriptstyle{\mathsf{map}\
\overline{f}}$

Figure 5.6: Commutative diagram illustrating Section 5.2.3.

[ ] If a function $\overline{f}\colon\mathbb{3}\to\mathbb{3}$ on ternary
digits realises a midpoint homomorphism $f\colon\mathbb{I}\to\mathbb{I}$ on
the interval object, then
$\mathsf{map}(\overline{f})\colon{\mathbb{3}^{\mathbb{N}}}\to{\mathbb{3}^{\mathbb{N}}}$
realises $f$ on signed-digit encodings.

###### Proof.

[$\mathsf{f}$] We want to show that, for all
$\alpha\colon{\mathbb{3}^{\mathbb{N}}}$,
$\langle\langle\mathsf{map}(\overline{f},\alpha)\rangle\rangle=f(\langle\langle\alpha\rangle\rangle)$.
By function extensionality and Section 5.2.2, the left-hand side of the
equation becomes $M(\lambda n.\langle\overline{f}(\alpha_{n})\rangle)$. By the
fact that $\overline{f}$ realises $f$, it further becomes $M(\lambda
n.f(\langle\alpha_{n}\rangle))$. By Section 5.1.2, $f$ is an $M$-homomorphism,
and therefore the equation becomes $f(M(\lambda n.\langle\alpha_{n}\rangle))$;
which is definitionally equal to the conclusion by Section 5.2.2.

######  Theorem 5.2.1.

[ ]  The negation function on signed-digit encodings realises the negation
function on the interval object.

###### Proof.

[$\mathsf{f}$] By Sections 5.2.3, 5.2.3 and 5.1.5.

##### Binary midpoint

The midpoint functions — both binary and infinitary, which are intended to
realise $\oplus$ and $M$, respectively — are much more complicated to define
on signed-digit encodings. We follow the definitions Escardó gave in [Esc11a],
formalising them in Agda for our framework.

The binary midpoint defined here sums two encodings of type
$\mathbb{3}^{\mathbb{N}}$ (which encodes the interval $[-1,1]$) to achieve an
encoding of type $\mathbb{5}^{\mathbb{N}}$ (which encodes the interval
$[-2,2]$) which is then divided by two to output an encoding once again in
$\mathbb{3}^{\mathbb{N}}$.

[ ] The type of _quinary digits_ $\mathbb{5}$, equivalent to
$\mathsf{Fin}(5)$, is defined by its elements
$\overline{2},\overline{1},0,1,2\colon\mathbb{5}$.

[ ] We define the addition function on ternary digits
$\mathsf{add\mathbb{3}}\colon\mathbb{3}\to\mathbb{3}\to\mathbb{5}$ in the
expected way by pattern matching (e.g.
$\mathsf{add\mathbb{3}}(\overline{1},\overline{1}):=\overline{2})$, etc.).

Now we define the halving function
$\mathsf{div2}\colon\mathbb{5}^{\mathbb{N}}\to{\mathbb{3}^{\mathbb{N}}}$
corecursively (though, as we see in the below Section 5.2.3, we define the
function by induction in our Agda formalisation). When the first element is
$\overline{2},0$ or $2$, the output is straightforward. Otherwise, the
definition must ‘offset’ the output using the redundant digits $\overline{1}$
and $1$.

[ ] We define the halving function from quinary signed-digit encodings to
ternary signed-digit encodings as,

$\displaystyle\mathsf{div2}$ $\displaystyle:\mathbb{5}^{\mathbb{N}}$
$\displaystyle\to{\mathbb{3}^{\mathbb{N}}},$ $\displaystyle\mathsf{div2}$
$\displaystyle(\overline{2}$ $\displaystyle::\alpha)$
$\displaystyle:=\overline{1}$ $\displaystyle\ ::\mathsf{div2}$
$\displaystyle($ $\displaystyle\alpha),$ $\displaystyle\mathsf{div2}$
$\displaystyle(\overline{1}::\overline{2}$ $\displaystyle::\alpha)$
$\displaystyle:=\overline{1}$ $\displaystyle\ ::\mathsf{div2}$
$\displaystyle(0::$ $\displaystyle\alpha),$ $\displaystyle\mathsf{div2}$
$\displaystyle(\overline{1}::\overline{1}$ $\displaystyle::\alpha)$
$\displaystyle:=\overline{1}$ $\displaystyle\ ::\mathsf{div2}$
$\displaystyle(1::$ $\displaystyle\alpha),$ $\displaystyle\mathsf{div2}$
$\displaystyle(\overline{1}::0$ $\displaystyle::\alpha)$ $\displaystyle:=0$
$\displaystyle\ ::\mathsf{div2}$ $\displaystyle(\overline{2}::$
$\displaystyle\alpha),$ $\displaystyle\mathsf{div2}$
$\displaystyle(\overline{1}::1$ $\displaystyle::\alpha)$ $\displaystyle:=0$
$\displaystyle\ ::\mathsf{div2}$ $\displaystyle(\overline{1}::$
$\displaystyle\alpha),$ $\displaystyle\mathsf{div2}$
$\displaystyle(\overline{1}::2$ $\displaystyle::\alpha)$ $\displaystyle:=0$
$\displaystyle\ ::\mathsf{div2}$ $\displaystyle(0::$ $\displaystyle\alpha),$
$\displaystyle\mathsf{div2}$ $\displaystyle(0$ $\displaystyle::\alpha)$
$\displaystyle:=0$ $\displaystyle\ ::\mathsf{div2}$ $\displaystyle($
$\displaystyle\alpha),$ $\displaystyle\mathsf{div2}$
$\displaystyle(1::\overline{2}$ $\displaystyle::\alpha)$ $\displaystyle:=0$
$\displaystyle\ ::\mathsf{div2}$ $\displaystyle(0::$ $\displaystyle\alpha),$
$\displaystyle\mathsf{div2}$ $\displaystyle(1::\overline{1}$
$\displaystyle::\alpha)$ $\displaystyle:=0$ $\displaystyle\ ::\mathsf{div2}$
$\displaystyle(1::$ $\displaystyle\alpha),$ $\displaystyle\mathsf{div2}$
$\displaystyle(1::0$ $\displaystyle::\alpha)$ $\displaystyle:=0$
$\displaystyle\ ::\mathsf{div2}$ $\displaystyle(2::$ $\displaystyle\alpha),$
$\displaystyle\mathsf{div2}$ $\displaystyle(1::1$ $\displaystyle::\alpha)$
$\displaystyle:=1$ $\displaystyle\ ::\mathsf{div2}$
$\displaystyle(\overline{1}::$ $\displaystyle\alpha),$
$\displaystyle\mathsf{div2}$ $\displaystyle(1::2$ $\displaystyle::\alpha)$
$\displaystyle:=1$ $\displaystyle\ ::\mathsf{div2}$ $\displaystyle(0::$
$\displaystyle\alpha),$ $\displaystyle\mathsf{div2}$ $\displaystyle(2$
$\displaystyle::\alpha)$ $\displaystyle:=1$ $\displaystyle\ ::\mathsf{div2}$
$\displaystyle($ $\displaystyle\alpha).$

[ ] We actually define this function in Agda using an auxiliary function

$\mathsf{div2^{\prime}}\colon\mathbb{5}\times\mathbb{5}\to\mathbb{3}\times\mathbb{5}$

such that we define

$\displaystyle\mathsf{div2}$ $\displaystyle(\alpha)_{0}$
$\displaystyle:=\mathsf{pr_{1}}(\mathsf{div2^{\prime}}(\alpha_{0},\alpha_{1})),$
$\displaystyle\mathsf{div2}$ $\displaystyle(\alpha)_{n+1}$
$\displaystyle:=\mathsf{div2}(\mathsf{pr_{2}}(\mathsf{div2^{\prime}}(\alpha_{0},\alpha_{1})::\mathsf{tail}(\mathsf{tail}\
\alpha))).$

The values of $\mathsf{div2^{\prime}}$ can be seen in Section 5.2.3. For
example $\mathsf{div2^{\prime}}(\overline{1},\overline{2}):=(\overline{1},0)$.

We use this function to define the binary midpoint function.

[ ] The binary midpoint function on ternary signed-digit encodings is defined
by adding the two sequences and then halving the result:

$\displaystyle\mathsf{mid}$ $\displaystyle:{\mathbb{3}^{\mathbb{N}}}\to$
$\displaystyle{\mathbb{3}^{\mathbb{N}}}\to{\mathbb{3}^{\mathbb{N}}},$
$\displaystyle\mathsf{mid}$ $\displaystyle(\alpha,\beta)$
$\displaystyle:=\mathsf{div2}(\mathsf{zipWith}(\mathsf{add\mathbb{3}},\alpha,\beta)).$

To verify that $\mathsf{mid}$ correctly realises $\oplus$, we utilise the
following halving map $\mathsf{half}$ and prove its relationship to
$\mathsf{div2}$

[ ] We define the halving map from quinary digits to the interval object as,

$\displaystyle\mathsf{half}$ $\displaystyle:\mathbb{5}$
$\displaystyle\to\mathbb{I},$ $\displaystyle\mathsf{half}$
$\displaystyle(\overline{2})$ $\displaystyle:=-1,$
$\displaystyle\mathsf{half}$ $\displaystyle(\overline{1})$
$\displaystyle:=-1\oplus 0,$ $\displaystyle\mathsf{half}$ $\displaystyle(0)$
$\displaystyle:=0,$ $\displaystyle\mathsf{half}$ $\displaystyle(1)$
$\displaystyle:=+1\oplus 0,$ $\displaystyle\mathsf{half}$ $\displaystyle(2)$
$\displaystyle:=+1.$

floatrowfigurerowb
${{\mathbb{3}\times\mathbb{3}}}$${\mathbb{5}}$${{\mathbb{I}\times\mathbb{I}}}$${\mathbb{I}}$$\scriptstyle{\mathsf{add}\mathbb{3}}$$\scriptstyle{\oplus}$$\scriptstyle{\langle-\rangle\times\langle-\rangle}$$\scriptstyle{\mathsf{half}}$
${{\mathbb{3}^{\mathbb{N}}\times\mathbb{3}^{\mathbb{N}}}}$${\mathbb{5}^{\mathbb{N}}}$${\mathbb{3}^{\mathbb{N}}}$${{\mathbb{I}\times\mathbb{I}}}$${\mathbb{I}}$${\mathbb{I}}$$\scriptstyle{\mathsf{zipWith}(\mathsf{add}\mathbb{3})}$$\scriptstyle{\oplus}$$\scriptstyle{\langle\langle-\rangle\rangle\times\langle\langle-\rangle\rangle}$$\scriptstyle{M\circ\mathsf{map}(\mathsf{half})}$$\scriptstyle{\mathsf{div2}}$$\scriptstyle{\langle\langle-\rangle\rangle}$$\scriptstyle{\mathsf{mid}}$

Figure 5.7: Commutative diagrams illustrating Section 5.2.3 (left) and
Sections 5.2.3, 5.2.3 and 5.2.2 (right).

We first prove the following lemma about the auxiliary function
$\mathsf{div2^{\prime}}$ (Section 5.2.3).

[ ] Given any $x,y\colon\mathbb{5}$ and $z\colon\mathbb{I}$, we have

$\langle a\rangle\oplus(\mathsf{half}\ b\oplus z)=(\mathsf{half}\
x\oplus(\mathsf{half}\ y\oplus z)),$

where
$a,b\colon\mathbb{3}\times\mathbb{5}:=\mathsf{div2^{\prime}}(\alpha_{0},\alpha_{1})$.

###### Proof.

The cases where $a:=\\{\overline{2},0,2\\}$ are trivial. The ten other cases
all require slightly different approaches, but all are just the rearrangement
of elements of the midpoint algebra by idempotency, commutativity and
transpositionality (Section 5.1.1).

[ ] Given any quinary signed-digit encoding
$\alpha\colon\mathbb{5}^{\mathbb{N}}$, we have that
$\langle\langle\mathsf{div2}(\alpha)\rangle\rangle=M(\mathsf{map}(\mathsf{half},\alpha))$.

###### Proof.

[$\mathsf{f}$] By using Section 5.1.3, this is reduced to showing
$\mathsf{map}(\langle-\rangle,\mathsf{div2}(\alpha))$ and
$\mathsf{map}(\mathsf{half},\alpha)$, for any
$\alpha\colon\mathbb{5}^{\mathbb{N}}$, are $n$-approximately equal for any
$n\colon\mathbb{N}$. In the base case, when $n:=0$, the proof is trivial — we
can set $z,w\colon\mathbb{I}$ as any elements of $\mathbb{I}$, and so we only
need to consider the inductive case where $n:=n^{\prime}+1$.

Recall from Section 5.1.3 that this means we must give some
$z,w\colon\mathbb{I}$ that satisfy

$\langle\mathsf{div2}(\alpha)_{0}\rangle\oplus(\langle\mathsf{div2}(\alpha)_{1}\rangle\oplus...(\mathsf{div2}(\alpha)_{n}\oplus
w))=\mathsf{half}(x_{0})\oplus(\mathsf{half}(\alpha_{1})\oplus...(\mathsf{half}(\alpha_{n})\oplus
z)).$

By taking
$(a,b)\colon\mathbb{3}\times\mathbb{5}:=\mathsf{div2^{\prime}}(\alpha_{0},\alpha_{1})$
this reduces to

$\langle
a\rangle\oplus(\langle\mathsf{div2}(b::\alpha^{\prime})_{1}\rangle\oplus...(\mathsf{div2}(b::\alpha^{\prime})_{n}\oplus
w))=\mathsf{half}(\alpha_{0})\oplus(\mathsf{half}(\alpha_{1})\oplus...(\mathsf{half}(\alpha_{n})\oplus
z)),$

where $\alpha^{\prime}:=\mathsf{tail}(\mathsf{tail}(\alpha))$. By using the
inductive hypothesis on the sequence $b::\alpha^{\prime}$, this becomes

$\langle
a\rangle\oplus(\mathsf{half}(b)\oplus...(\mathsf{half}(\alpha_{n})\oplus
z))=\mathsf{half}(\alpha_{0})\oplus(\mathsf{half}(\alpha_{1})\oplus...(\mathsf{half}(\alpha_{n})\oplus
z)).$

Therefore, the result follows by Section 5.2.3.

We next show that halving an added sequence in the representation space
realises the midpoint operation.

[ ] Given any ternary digits $a,b\colon\mathbb{3}$, we have that
$\mathsf{half}(\mathsf{add\mathbb{3}}(a,b))=\langle a\rangle\oplus\langle
b\rangle$.

###### Proof.

[$\mathsf{f}$] By induction on $a,b\colon\mathbb{3}$, as well as the
idempotency and commutativity of $\oplus$ by Section 5.1.1.

[ ] Given any ternary signed-digit encodings
$\alpha,\beta\colon{\mathbb{3}^{\mathbb{N}}}$, we have that
$M(\mathsf{map}(\mathsf{half},\mathsf{zipWith}(\mathsf{add\mathbb{3}},\alpha,\beta)))=\langle\langle\alpha\rangle\rangle\oplus\langle\langle\beta\rangle\rangle$.

###### Proof.

[$\mathsf{f}$] By function extensionality and Section 5.2.3,
$M(\mathsf{map}(\mathsf{half},\mathsf{zipWith}(\mathsf{add\mathbb{3}},\alpha,\beta)))=M(\lambda
n.\langle\alpha\rangle\oplus\langle\beta\rangle)$. The result then follows by
Section 5.1.2.

Using the two lemmas we have proved, we can now complete our verification of
the midpoint operation.

######  Theorem 5.2.2.

[ ]  The midpoint function on signed-digit encodings realises the midpoint
operator on the interval object.

###### Proof.

[$\mathsf{f}$] By Sections 5.2.3 and 5.2.3.

##### Infinitary midpoint

The infinitary midpoint function is obviously more complicated, both to define
and verify. Escardó defines the infinitary midpoint on signed-digit encodings
by using another intermediary signed-digit representation (this time of the
interval $[-4,4]$).

[ ] The type of _nonary digits_ $\mathbb{9}$, equivalent to $\mathsf{Fin}(9)$,
is defined by its elements
$\overline{4},\overline{3},\overline{2},\overline{1},0,1,2,3,4\colon\mathbb{9}$.

[ ] We define the addition function on quinary digits
$\mathsf{add\mathbb{5}}\colon\mathbb{5}\to\mathbb{5}\to\mathbb{9}$ in the
expected way by pattern matching.

We also define the quartering function
$\mathsf{div4}\colon\mathbb{9}^{\mathbb{N}}\to{\mathbb{3}^{\mathbb{N}}}$ by
induction, and the related function
$\mathsf{quarter}\colon\mathbb{9}\to\mathbb{I}$ on nonary digits.

[ ] We define the quartering function
$\mathsf{div4}\colon\mathbb{9}^{\mathbb{N}}\to{\mathbb{3}^{\mathbb{N}}}$ from
nonary signed-digit encodings to ternary signed-digit encodings similarly to
how we defined
$\mathsf{div2}\colon\mathbb{5}^{\mathbb{N}}\to{\mathbb{3}^{\mathbb{N}}}$.

[ ] We define the quartering map
$\mathsf{quarter}\colon\mathbb{9}\to\mathbb{I}$ from nonary digits to the
interval object similarly to how we defined
$\mathsf{half}\colon\mathbb{5}\to\mathbb{I}$.

[ ] Given any ternary signed-digit encoding
$\alpha\colon{\mathbb{3}^{\mathbb{N}}}$, we have that
$\langle\langle\mathsf{div4}(\alpha)\rangle\rangle=M(\mathsf{map}(\mathsf{quarter},\alpha))$.

###### Proof.

[$\mathsf{f}$] Similar to Section 5.2.3.

We now define Adam Scriven’s infinitary midpoint function on ternary signed-
digit encodings in our framework. This definition was first given by Scriven
in his MSc thesis, and reimplemented by Escardóin his Haskell library [Scr07,
Esc11a].

[ ] The infinitary midpoint function on ternary signed-digit encodings is
defined by translating Scriven’s definition to Agda:

$\displaystyle\mathsf{bigMid}^{\prime}$
$\displaystyle:({\mathbb{3}^{\mathbb{N}}})^{\mathbb{N}}\to\mathbb{9}^{\mathbb{N}},$
$\displaystyle\mathsf{bigMid}^{\prime}$
$\displaystyle(((a::b::x)::(c::y)::\zeta))_{0}$
$\displaystyle:=\mathsf{add\mathbb{5}}(\mathsf{add\mathbb{3}}(a,a),\mathsf{add\mathbb{3}}(b,c)),$
$\displaystyle\mathsf{bigMid}^{\prime}$
$\displaystyle(((a::b::x)::(c::y)::\zeta))_{{n+1}}$
$\displaystyle:=\mathsf{bigMid}^{\prime}(\mathsf{mid}(x,y)::\zeta)_{n},$
$\displaystyle\mathsf{bigMid}$
$\displaystyle:({\mathbb{3}^{\mathbb{N}}})^{\mathbb{N}}\to K,$
$\displaystyle\mathsf{bigMid}$
$\displaystyle:=\mathsf{div4}\circ\mathsf{bigMid}^{\prime}.$

${{(\mathbb{3}^{\mathbb{N}})^{\mathbb{N}}}}$${\mathbb{9}^{\mathbb{N}}}$${\mathbb{3}^{\mathbb{N}}}$${\mathbb{I}^{\mathbb{N}}}$${\mathbb{I}}$${\mathbb{I}}$$\scriptstyle{\mathsf{bigMid^{\prime}}}$$\scriptstyle{M}$$\scriptstyle{\mathsf{map}\
\langle\langle-\rangle\rangle}$$\scriptstyle{M\circ\mathsf{map}(\mathsf{quarter})}$$\scriptstyle{\langle\langle-\rangle\rangle}$$\scriptstyle{\mathsf{div4}}$$\scriptstyle{\mathsf{bigMid}}$
Figure 5.8: Commutative diagram illustrating Theorem 5.2.3.

This operation does indeed realise the iteration operator
$M\colon\mathbb{I}^{\mathbb{N}}\to\mathbb{I}$ on the interval object; i.e. the
diagram in Figure 5.8 commutes. We prove this by using the following lemmas.

[ ] Given any ternary digits $a,b,c\colon\mathbb{3}$, we have that
$\mathsf{quarter}(\mathsf{add\mathbb{5}}(\mathsf{add\mathbb{3}}(a,a),\mathsf{add\mathbb{3}}(b,c)))=\langle
a\rangle\oplus(\langle b\rangle\oplus\langle c\rangle)$.

###### Proof.

By induction on $a,b,c\colon\mathbb{3}$, as well as the idempotency,
commutativity and transpositionality of $\oplus$ by Section 5.1.1.

[ ] Given any ternary signed-digit encodings
$\alpha,\beta\colon{\mathbb{3}^{\mathbb{N}}}$ and real number
$z\colon\mathbb{I}$ in the interval object, we have,

$\langle\langle\alpha\rangle\rangle\oplus(\langle\langle\beta\rangle\rangle\oplus
z)=(\langle a\rangle\oplus(\langle b\rangle\oplus\langle
c\rangle))\oplus(\langle\langle\mathsf{mid}(\alpha^{\prime},\beta^{\prime})\rangle\rangle\oplus
z),$

where $(a::b::\alpha^{\prime}):=\alpha$ and $(c::\beta^{\prime}):=\beta$.

###### Proof.

[$\mathsf{f}$] By the following equational reasoning, (i) idempotency of $M$
(Section 5.1.2), (ii) commutativity and (iii) transpositionality of $\oplus$
(Section 5.1.1), and (iv) the correctness of the binary midpoint operation
(Theorem 5.2.2),

$\displaystyle\langle\langle\alpha\rangle\rangle$ $\displaystyle\oplus\ $
$\displaystyle(\langle\langle\beta\rangle\rangle\oplus z),$ $\displaystyle:=$
$\displaystyle\langle\langle(a::(b::\alpha^{\prime}))\rangle\rangle$
$\displaystyle\oplus\ $
$\displaystyle(\langle\langle(c::\beta^{\prime})\rangle\rangle\oplus z),$
$\displaystyle=$ $\displaystyle\langle
a\rangle\oplus\langle\langle(b::\alpha^{\prime})\rangle\rangle$
$\displaystyle\oplus\ $
$\displaystyle(\langle\langle(c::\beta^{\prime})\rangle\rangle\oplus z),$
$\displaystyle\text{by (i)},$ $\displaystyle=$ $\displaystyle(\langle
a\rangle\oplus(\langle
b\rangle\oplus\langle\langle\alpha^{\prime}\rangle\rangle))$
$\displaystyle\oplus\ $
$\displaystyle(\langle\langle(c::\beta^{\prime})\rangle\rangle\oplus z),$
$\displaystyle\text{by (i)},$ $\displaystyle=$ $\displaystyle(\langle
a\rangle\oplus(\langle
b\rangle\oplus\langle\langle\alpha^{\prime}\rangle\rangle))$
$\displaystyle\oplus\ $ $\displaystyle((\langle
c\rangle\oplus\langle\langle\beta^{\prime}\rangle\rangle)\oplus z),$
$\displaystyle\text{by (i)},$ $\displaystyle=$ $\displaystyle((\langle
b\rangle\oplus\langle\langle\alpha^{\prime}\rangle\rangle)\oplus\langle
a\rangle)$ $\displaystyle\oplus\ $ $\displaystyle((\langle
c\rangle\oplus\langle\langle\beta^{\prime}\rangle\rangle)\oplus z),$
$\displaystyle\text{by (ii)},$ $\displaystyle=$ $\displaystyle((\langle
b\rangle\oplus\langle\langle\alpha^{\prime}\rangle\rangle)\oplus(\langle
c\rangle\oplus\langle\langle\beta^{\prime}\rangle\rangle))$
$\displaystyle\oplus\ $ $\displaystyle(\langle a\rangle\oplus z),$
$\displaystyle\text{by (iii)},$ $\displaystyle=$ $\displaystyle((\langle
b\rangle\oplus\langle
c\rangle)\oplus(\langle\langle\alpha^{\prime}\rangle\rangle\oplus\langle\langle\beta^{\prime}\rangle\rangle))$
$\displaystyle\oplus\ $ $\displaystyle(\langle a\rangle\oplus z),$
$\displaystyle\text{by (iii)},$ $\displaystyle=$ $\displaystyle((\langle
b\rangle\oplus\langle c\rangle)\oplus(\langle a\rangle)$ $\displaystyle\oplus\
$
$\displaystyle(\langle\langle\alpha^{\prime}\rangle\rangle\oplus\langle\langle\beta^{\prime}\rangle\rangle)\oplus
z),$ $\displaystyle\text{by (iii)},$ $\displaystyle=$ $\displaystyle(\langle
a\rangle\oplus(\langle b\rangle\oplus\langle c\rangle)$ $\displaystyle\oplus\
$
$\displaystyle(\langle\langle\alpha^{\prime}\rangle\rangle\oplus\langle\langle\beta^{\prime}\rangle\rangle)\oplus
z),$ $\displaystyle\text{by (iii)},$ $\displaystyle=$ $\displaystyle(\langle
a\rangle\oplus(\langle b\rangle\oplus\langle c\rangle)$ $\displaystyle\oplus\
$ $\displaystyle(\mathsf{mid}(\alpha^{\prime},\beta^{\prime})\oplus z)),$
$\displaystyle\text{by (iv)}.$

[ ] Given any ternary signed-digit encodings
$\alpha,\beta\colon{\mathbb{3}^{\mathbb{N}}}$ and real number
$z\colon\mathbb{I}$ in the interval object, we have,

$\langle\langle\alpha\rangle\rangle\oplus(\langle\langle\beta\rangle\rangle\oplus
z)=\mathsf{quarter}(\mathsf{add\mathbb{5}}(\mathsf{add\mathbb{3}}(a,a),\mathsf{add\mathbb{3}}(b,c)))\oplus(\langle\langle\mathsf{mid}(\alpha^{\prime},\beta^{\prime})\rangle\rangle\oplus
z),$

where $(a::b::\alpha^{\prime}):=\alpha$ and $(c::\beta^{\prime}):=\beta$.

###### Proof.

[$\mathsf{f}$] By Sections 5.2.3 and 5.2.3.

Thus, it turns out that the $\mathsf{bigMid}$ operation provides an
$n$-approximation of $M$ for every $n\colon\mathbb{N}$.

[ ] The functions $\mathsf{map}(\langle\langle-\rangle\rangle)$ and
$\mathsf{map}(\mathsf{quarter})\circ\mathsf{bigMid^{\prime}}$ — both of type
$({\mathbb{3}^{\mathbb{N}}})^{\mathbb{N}}\to\mathbb{I}^{\mathbb{N}}$ — are
$n$-approximately equal for all $n\colon\mathbb{N}$.

###### Proof.

[$\mathsf{f}$] By induction and Section 5.2.3.

######  Theorem 5.2.3.

[ ]  The infinitary midpoint function on ternary signed-digit encodings
realises the iteration operator on the interval object; i.e. given any
sequence of ternary signed-digit encodings
$\zeta\colon({\mathbb{3}^{\mathbb{N}}})^{\mathbb{N}}$, we have
$\langle\langle\mathsf{bigMid}(\zeta)\rangle\rangle=M(\mathsf{map}(\langle\langle-\rangle\rangle,\zeta))$.

###### Proof.

[$\mathsf{f}$] By Theorems 5.1.1, 5.2.3 and 5.2.3.

##### Multiplication

Finally, we define and verify multiplication. In the Haskell library, Escardó
defined a variety of multiplication functions on signed-digit encodings; we
choose to define and verify mul_version0, which uses the $\mathsf{bigMid}$
function [Esc11a].

[ ] The auxiliary multiplication function, which multiplies a ternary signed-
digit encoding by a ternary digit, is defined as follows:

$\displaystyle\mathsf{digitMul}$ $\displaystyle:\mathbb{3}\to$
$\displaystyle{\mathbb{3}^{\mathbb{N}}}\to{\mathbb{3}^{\mathbb{N}}},$
$\displaystyle\mathsf{digitMul}$ $\displaystyle(\overline{1},\beta)$
$\displaystyle:=\mathsf{neg}(\beta),$ $\displaystyle\mathsf{digitMul}$
$\displaystyle(0,\beta)$ $\displaystyle:=\lambda n.0,$
$\displaystyle\mathsf{digitMul}$ $\displaystyle(1,\beta)$
$\displaystyle:=\beta.$

[ ] The multiplication function on ternary signed-digit encodings is defined
by multiplying the first argument against each individual digit of the second,
and then taking the infinitary midpoint:

$\displaystyle\mathsf{mul}$ $\displaystyle:{\mathbb{3}^{\mathbb{N}}}\to$
$\displaystyle{\mathbb{3}^{\mathbb{N}}}\to{\mathbb{3}^{\mathbb{N}}},$
$\displaystyle\mathsf{mul}$ $\displaystyle(\alpha,\beta)$
$\displaystyle:=\mathsf{bigMid}(\mathsf{zipWith}(\mathsf{digitMul},\alpha,\mathsf{repeat}\
\beta)).$

This function realises the multiplication function on the interval object;
i.e. the diagrams in Figure 5.9 commute.

floatrowfigurerowb
${{\mathbb{3}\times\mathbb{3}^{\mathbb{N}}}}$${K}$${{\mathbb{I}\times\mathbb{I}}}$${\mathbb{I}}$$\scriptstyle{\mathsf{digitMul}}$$\scriptstyle{*}$$\scriptstyle{\langle-\rangle\times\langle\langle-\rangle\rangle}$$\scriptstyle{\langle\langle-\rangle\rangle}$
${{\mathbb{3}^{\mathbb{N}}\times\mathbb{3}^{\mathbb{N}}}}$${{(\mathbb{3}^{\mathbb{N}})^{\mathbb{N}}}}$${\mathbb{3}^{\mathbb{N}}}$${{\mathbb{I}\times\mathbb{I}}}$${{\mathbb{I}^{\mathbb{N}}}}$${\mathbb{I}}$$\scriptstyle{\mathsf{repeat}\
\circ\ *}$$\scriptstyle{\mathsf{map}\
\langle\langle-\rangle\rangle}$$\scriptstyle{\mathsf{digitMul^{\prime}}}$$\scriptstyle{\langle\langle-\rangle\rangle\times\langle\langle-\rangle\rangle}$$\scriptstyle{M}$$\scriptstyle{\mathsf{bigMid}}$$\scriptstyle{\mathsf{mul}}$$\scriptstyle{\langle\langle-\rangle\rangle}$$\scriptstyle{*}$

Figure 5.9: Commutative diagrams illustrating Section 5.2.3 (left) and Theorem
5.2.4 (right). In the diagram,
$\mathsf{digitMul^{\prime}}:=\lambda\alpha\beta.\mathsf{zipWith}(\mathsf{digitMul},\alpha,\mathsf{repeat}\
\beta)$.

[ ] The auxiliary multiplication operator realises multiplication on the
interval object; i.e. given any ternary digit $t\colon\mathbb{3}$ and a
ternary signed-digit encodings $\beta\colon{\mathbb{3}^{\mathbb{N}}}$, we have
$\langle\langle\mathsf{digitMul}(t,\beta)\rangle\rangle=\langle
t\rangle*\langle\langle\beta\rangle\rangle$.

###### Proof.

[$\mathsf{f}$] By induction on $t\colon\mathbb{3}$.

In the case where $t:=\overline{1}$, we must show that
$\langle\langle\mathsf{neg}(\beta)\rangle\rangle=-1*\langle\langle\beta\rangle\rangle$.
By the negation realiser (Theorem 5.2.1),
$\langle\langle\mathsf{neg}(\beta)\rangle\rangle=-\langle\langle\beta\rangle\rangle$.
The result follows by Section 5.1.5.

In the case where $t:=0$, we must show that $\langle\langle\lambda
n.0\rangle\rangle=0*\langle\langle\beta\rangle\rangle$. By the idempotency of
$M$ (Section 5.1.2), $\langle\langle\lambda
n.0\rangle\rangle:=M(\mathsf{map}(\langle-\rangle,\lambda n.0))=\langle
0\rangle=0$. The result follows by Section 5.1.5.

In the case where $t:=1$, we must show that
$\langle\langle\beta\rangle\rangle=1*\langle\langle\beta\rangle\rangle$. The
result follows by Section 5.1.5.

######  Theorem 5.2.4.

[ ]  The multiplication function on ternary signed-digit encodings realises
the multiplication operation on the interval object.

###### Proof.

[$\mathsf{f}$] By the following equational reasoning, (i) the correctness of
the infinitary midpoint operation (Theorem 5.2.3), (ii) the correctness of the
auxiliary multiplication operation (Section 5.2.3), (iii) the fact right-
multiplication — i.e. $\lambda y.x*y$ for a given $x\colon\mathbb{I}$ — is a
midpoint homomorphism (Section 5.1.5), and (iv) the fact that midpoint
homomorphisms are $M$-homomorphisms (Section 5.1.2),

$\displaystyle\langle\langle\mathsf{mul}(\alpha,\beta)\rangle\rangle,$
$\displaystyle:=$
$\displaystyle\langle\langle\mathsf{bigMid}(\mathsf{zipWith}(\mathsf{digitMul},\alpha,\mathsf{repeat}\
\beta))\rangle\rangle,$ $\displaystyle=$ $\displaystyle
M(\mathsf{map}(\langle\langle-\rangle\rangle,\mathsf{zipWith}(\mathsf{digitMul},\alpha,\mathsf{repeat}\
\beta)))$ $\displaystyle\text{by (i)},$ $\displaystyle:=$ $\displaystyle
M(\lambda n.\langle\langle\mathsf{digitMul}(\alpha_{n},\beta)\rangle\rangle),$
$\displaystyle=$ $\displaystyle M(\lambda
n.\langle\alpha_{n}\rangle*\langle\langle\beta\rangle\rangle)$
$\displaystyle\text{by (ii)},$ $\displaystyle=$ $\displaystyle M(\lambda
n.\langle\alpha_{n}\rangle)*\langle\langle\beta\rangle\rangle$
$\displaystyle\text{by (iii) and (iv)},$ $\displaystyle:=$
$\displaystyle\langle\langle\alpha\rangle\rangle*\langle\langle\beta\rangle\rangle.$

###  5.3 Ternary Boehm encodings

We shall see in Chapter 6 that the ternary signed-digit encodings are an ideal
type for formalising the convergence of what we call ‘exact real search’.
However, in that section it will also become clear that the efficiency of the
algorithms extracted from the convergence theorems of search, optimisation and
regression on that type leave much to be desired. For this reason, we
introduce another type — ternary Boehm encodings — that yield more efficient
algorithms at the expense of being more difficult to formalise in our Agda
framework333Hence, we have not verified the ternary Boehm encodings to the
same extent as the ternary signed-digit encodings..

In the 1990s, Hans-J. Boehm produced a practical Java library for exact real
arithmetic [Boe99]. Since then, Boehm’s library has been developed to become
the underpinning of Google’s bespoke Android calculator mobile phone
application [Boe17, Boe20]. The star of the library is the class CR, objects
of which Boehm calls _constructive reals_. Objects $x$ of CR have a single
private method approximate, which takes a (small) integer and outputs an
(effectively unbounded) integer. The input integer $n$ denotes the requested
_precision-level_ of the constructive real, while the output integer $x_{n}$
denotes an integer approximation — scaled relative to the given precision-
level — of the real number $\llbracket x\rrbracket\colon\mathbb{R}$ which $x$
encodes.

Every object of CR is therefore a bi-infinite sequence of integer
approximations of a real number, which is constructed and manipulated to
ensure that the following condition about its relationship to the real number
it encodes always holds:

$d_{\mathbb{R}}(\llbracket x\rrbracket,2^{n}x_{n})<2^{n}.$

In this section, we will show how we re-rationalise this class — adapted
slightly for the purposes of exact real search — within our Agda framework as
the type $\mathbb{T}$. We will then verify the structure of the type by
defining the representation map
$\llbracket-\rrbracket\colon\mathbb{T}\to\mathbb{R}$; for this purpose, we
utilise the Dedekind reals rather than the interval object, both for the sake
of variety and because elements of $\mathbb{T}$ represent reals without
reference to a particular compact interval. However, following this, we will
show how we use subtypes of $\mathbb{T}$ to represent only reals in particular
compact intervals, as this is required for search. Finally, we will discuss
how Boehm defines exact real arithmetic on CR by using interval arithmetic.

####  5.3.1 Definition in our type theory

In order to define CR in our type theory, we start off by representing the
class as functions $x\colon\mathbb{Z}\to\mathbb{Z}$. It is helpful to think of
the integer approximation $x_{n}\colon\mathbb{Z}$, at any precision-level
$n\colon\mathbb{Z}$, as an _interval approximation_ of $\llbracket
x\rrbracket$ — namely, $x_{n}$ represents to the open interval
$\left(2^{n}(x_{n}-1),2^{n}(x_{n}+1)\right),$ which clearly contains
$\llbracket x\rrbracket$.

As we wish to use these encodings for search, the open interval structure is
not ideal. Therefore, we alter CR by changing the order used in the
relationship above from _strict_ to _non-strict_. This is done because we
require the use of compact intervals for search, though it makes little
difference to the way CR objects are manipulated algorithmically. Furthermore,
for stylistic reasons we make two further changes. Firstly, with the ternary
signed-digits we used higher precision-levels $n$ to mean _more_ precise
integer approximations, rather than less, and so we alter CR so that we can do
the same. Furthermore, we slightly reposition the interval codes to avoid
unnecessary subtraction in our formalisation.

By making the two changes above, the functions
$x\colon\mathbb{Z}\to\mathbb{Z}$ we define for CR in our type theory must
satisfy

$d_{\mathbb{R}}(\llbracket x\rrbracket,2^{-n}(x_{n}+1))\leq 2^{-n},$

meaning that they are an infinitary sequence of integers, with each input-
output pair $(x_{n},n)\colon\mathbb{Z}^{2}$ representing the compact interval
with dyadic rational endpoints

$\left[\frac{x_{n}}{2^{n}},\frac{x_{n}+2}{2^{n}}\right].$

We illustrate the structure of these encodings in Figure 5.10, which shows
some possible interval approximations of real numbers in $[-3,3]$ at
precision-levels $0$, $1$ and $2$ — note that the intervals halve in size as
the precision-level increases further down the illustration. We refer to this
as the _ternary structure_ , because each interval represented by
$(n,m)\colon\mathbb{Z}^{2}$ in the structure is perfectly trisected into three
representations $(2n,m+1)$, $(2n+1,m+1)$ and $(2n+2,m+1)$ on the next
precision-level.

Figure 5.10: Ternary structure underlying the Boehm encodings. Each interval
approximation is represented by an integer pair. The coloured arrows
illustrate how the structural operations
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{downLeft}}$,
$\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathsf{downMid}}$,
$\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}{\mathsf{downRight}}$,
$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{upLeft}}$
and
$\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\pgfsys@color@cmyk@stroke{0.64}{0}{0.95}{0.40}\pgfsys@color<EMAIL_ADDRESS>work.

This structure can be ‘navigated’ by the following operations on integer
approximations. The operations
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{downLeft}}$,
$\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathsf{downMid}}$
and
$\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}{\mathsf{downRight}}$
take an integer that refers to an interval on an arbitrary precision-level and
return one which refers, respectively, to one of the three possible
trisections on the next precision-level. Meanwhile,
$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{upLeft}}$
and
$\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\pgfsys@color@cmyk@stroke{0.64}{0}{0.95}{0.40}\pgfsys@color<EMAIL_ADDRESS>do the reverse. The names here are colour coded with respect to the colours in
Figure 5.10, which illustrate how the operations work for particular
intervals.

$\displaystyle\mathsf{downLeft},$
$\displaystyle\mathsf{downMid},\mathsf{downRight},\mathsf{upLeft},\mathsf{upRight}:\mathbb{Z}\to\mathbb{Z},$
$\displaystyle\mathsf{downLeft}(k)$ $\displaystyle:=2k,$
$\displaystyle\mathsf{downMid}(k)$ $\displaystyle:=2k+1,$
$\displaystyle\mathsf{downRight}(k)$ $\displaystyle:=2k+2,$
$\displaystyle\mathsf{upRight}(\mathsf{pos}\ k)$ $\displaystyle:=\mathsf{pos}\
(k/2),$ $\displaystyle\mathsf{upRight}(\mathsf{negsucc}\ k)$
$\displaystyle:=\mathsf{negsucc}\ (k/2),$ $\displaystyle\mathsf{upLeft}(k)$
$\displaystyle:=\mathsf{upRight}(k-1).$

[ ] [ ] Given two integers $n,m\colon\mathbb{Z}$, we say that $n$ is _below_
$m$ if the interval represented by $(n,i+1)\colon\mathbb{Z}^{2}$ is a strict
subinterval of that which is represented by $(m,i)\colon\mathbb{Z}^{2}$ for
any $i\colon\mathbb{Z}$:

$\displaystyle\mathsf{below}$
$\displaystyle:\mathbb{Z}\to\mathbb{Z}\to\Omega,$ $\displaystyle n\ $
$\displaystyle\mathsf{below}\ m$ $\displaystyle:=\mathsf{downLeft}\ m\leq
n\leq\mathsf{downRight}\ m.$

Equivalently, this can be defined as follows:

$\displaystyle\mathsf{below}^{\prime}$
$\displaystyle:\mathbb{Z}\to\mathbb{Z}\to\Omega,$ $\displaystyle n\ $
$\displaystyle\mathsf{below}^{\prime}\ m$
$\displaystyle:=(n=\mathsf{downLeft}\ m)+(n=\mathsf{downMid}\
m)+(n=\mathsf{downRight}\ m).$

To further illustrate how ternary Boehm encodings work, let us now give an
example encoding $x\colon\mathbb{Z}\to\mathbb{Z}$ which is intended to
represent the real number $2\colon\mathbb{R}$; $x$ could be defined in a
variety of ways:

  * •

$x_{0}=1$, $x_{1}=2$, …

  * •

$x_{0}=1$, $x_{1}=3$, …

  * •

$x_{0}=1$, $x_{1}=4$, …

  * •

$x_{0}=0$, $x_{1}=2$, …

  * •

$x_{0}=0$, $x_{1}=3$, …

All of these are valid representations of $2$ as a ternary Boehm encoding
because the two interval approximations _intersect_. However, we wish in our
type theory to restrict ourselves to only those encodings that follow the
ternary structure — the last item in the above list would not, therefore, be
valid.

[ ] A sequence of integers $x\colon\mathbb{Z}\to\mathbb{Z}$ is _ternary_ if,

$\mathsf{ternary}(x):=\prod_{\left(n\colon\mathbb{Z}\right)}\left(x_{n+1}\
\mathsf{below}\ x_{n}\right).$

Restricting ourselves in this way will allow us to remove cases that are
difficult to reason about, and to define continuity and search similarly to
how we defined it for the ternary signed-digit encodings.

[ ] The type of _ternary Boehm encodings_ is defined as the collection of
ternary sequences:

$\mathbb{T}:=\sum_{\left(x\colon\mathbb{Z}\to\mathbb{Z}\right)}{\mathsf{ternary}(x)}.$

Returning to our illustration, we show one possible map that takes any integer
to a ternary Boehm encoding that represents it.

The function that maps any integer to a ternary Boehm encodings is defined as
follows:

$\displaystyle\mathsf{\mathbb{Z}{\text{-}}to{\text{-}}\mathbb{T}}$
$\displaystyle:\mathbb{Z}\to\mathbb{T},$
$\displaystyle\mathsf{\mathbb{Z}{\text{-}}to{\text{-}}\mathbb{T}}$
$\displaystyle(n)(\mathsf{pos}\ \ 0)$ $\displaystyle:=n,$
$\displaystyle\mathsf{\mathbb{Z}{\text{-}}to{\text{-}}\mathbb{T}}$
$\displaystyle(n)(\mathsf{pos}\ \ (i+1))$
$\displaystyle:=\mathsf{downLeft}^{i+1}(n),$
$\displaystyle\mathsf{\mathbb{Z}{\text{-}}to{\text{-}}\mathbb{T}}$
$\displaystyle(n)(\mathsf{negsucc}\ \ i)$
$\displaystyle:=\mathsf{upRight}^{i+1}(n).$

Before proceeding, we invite the reader to verify in their minds that this map
is indeed correct.

####  5.3.2 Verification of Boehm encodings via Dedekind reals

In this subsection, we will formally verify that the above definition of
ternary Boehm encodings does indeed represent real numbers. The application of
this work is for the future verification of exact real arithmetic on the Boehm
encodings (discussed in Sections 5.3.3 and 7.2.2).

We first quickly recap the Dedekind reals, which we use for the type of real
numbers $\mathbb{R}$ in this section. The work of implementing and formalising
the Dedekind reals (as well as the rationals and dyadic rationals) for the
Agda library TypeTopology was performed by Andrew Sneap in his M.Sci. project
[Sne21].

The Dedekind reals can be defined over any dense subset of the real numbers,
and are usually defined over the rationals $\mathbb{Q}$. We choose to instead
define them over the _dyadic rationals_ $\mathbb{Z}[\nicefrac{{1}}{{2}}]$ —
i.e. those rational numbers of form $\frac{z}{2^{n}}$ for
$z,n\colon\mathbb{Z}$ — as this will be more convenient when verifying the
structure of $\mathbb{T}$, whose interval approximations have dyadic
endpoints. We use the dyadics informally in this thesis; simply noting they
are a discrete set with a partial order, and that there is a function
$\iota\colon\mathbb{Z}\times\mathbb{Z}\to\mathbb{Z}[\nicefrac{{1}}{{2}}]$
which map pairs of integers $(z,n)\colon\mathbb{Z}\times\mathbb{Z}$ to the
dyadic rational $\frac{z}{2^{n}}$.

[ ] A _Dedekind real number_ $(L,R)\colon\mathbb{R}$ consists of two
predicates on dyadics $L,R\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]\to\Omega$ (the
_left cut_ and the _right cut_ respectively) that satisfy,

  1. 1.

$\exists_{\left(p\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]\right)}{L(p)}$,

  2. 2.

$\exists_{\left(q\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]\right)}{R(p)}$,

  3. 3.

$\prod_{\left(p\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]\right)}\left(L(p)\Leftrightarrow\exists_{\left(p^{\prime}\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]\right)}\left(L(p^{\prime})\times
p<p^{\prime}\right)\right)$,

  4. 4.

$\prod_{\left(q\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]\right)}\left(R(q)\Leftrightarrow\exists_{\left(q^{\prime}\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]\right)}\left(R(q^{\prime})\times
q^{\prime}<q\right)\right)$,

  5. 5.

$\prod_{\left(p,q\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]\right)}\left(L(p)\times
R(q)\to p<q\right)$,

  6. 6.

$\prod_{\left(p,q\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]\right)}\left(p<q\to
L(p)\vee R(q)\right)$.

Now recall the definitions of representation maps in Section 5.2.2. In order
to define the representation map
$\llbracket-\rrbracket\colon\mathbb{T}\to\mathbb{R}$ on ternary Boehm
encodings, we first look at how one can represent real numbers as sequences of
dyadic rational intervals that satisfy the _nested_ and _positioned_
properties (defined below). We will then show that — as we illustrated in the
previous subsection — every ternary Boehm real $\chi\colon\mathbb{T}$ can be
transformed into such a sequence of dyadic intervals, and therefore that we
can indeed define $\llbracket\chi\rrbracket\colon\mathbb{R}$.

[ ] The type of _valid representations of dyadic intervals_
$\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}$ is defined as the type of pairs of
dyadics such that the first is smaller than the second:

$\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}:=\sum_{\left((l,r)\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]\times\mathbb{Z}[\nicefrac{{1}}{{2}}]\right)}\left(l\leq
r\right).$

For convenience, we simply refer to elements of this type as _dyadic
intervals_.

[ ] One dyadic interval _covers_ another if,

$\displaystyle\ \mathsf{covers}\ $
$\displaystyle:\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}\to\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}\to\Omega,$
$\displaystyle(l_{1},r_{1})$ $\displaystyle\ \mathsf{covers}\ $
$\displaystyle(l_{2},r_{2}):=(l_{1}\leq l_{2})\times(r_{2}\leq r_{1}).$

[ ] A sequence of dyadic intervals
$\chi\colon\mathbb{Z}\to\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}$ is _nested_ if
every interval in the sequence covers the next:

$\displaystyle\mathsf{nested}$
$\displaystyle:(\mathbb{Z}\to\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I})\to\Omega,$
$\displaystyle\mathsf{nested}$
$\displaystyle(\chi):=\Pi_{\left(n\colon\mathbb{N}\right)}\left(\chi_{n}\
\mathsf{covers}\ \chi_{{n+1}}\right).$

[ ] A sequence of dyadic intervals
$\chi\colon\mathbb{Z}\to\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}$ is _positioned_
if it contains arbitrary small intervals,

$\displaystyle\mathsf{positioned}$
$\displaystyle:(\mathbb{Z}\to\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I})\to\Omega,$
$\displaystyle\mathsf{positioned}$
$\displaystyle(\chi):=\Pi_{\left(\varepsilon\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]\right)}(\varepsilon>0)\to\Sigma_{\left(n\colon\mathbb{N}\right)}\left(r_{n}-l_{n}\leq\varepsilon\right)\
\ \emph{(where $(l_{n},r_{n}):=\chi_{n}$)}.$

[ ] 444In Agda, the formalisation of this proof currently requires the use of
a number of unformalised lemmas about dyadic numbers. If a sequence of dyadic
intervals $\chi\colon\mathbb{Z}\to\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}$ is
nested and positioned, there is a real number
$\llparenthesis\chi\rrparenthesis\colon\mathbb{R}$ which it represents.

###### Proof.

[$\mathsf{t}$] The proof is due to Andrew Sneap. The Dedekind cuts
$L,R\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]\to\Omega$ are defined as follows:

$\displaystyle L$ $\displaystyle(p)$
$\displaystyle:=\exists_{\left(n\colon\mathbb{Z}\right)}\left(p<\mathsf{pr_{1}}(\chi_{n})\right),$
$\displaystyle R$ $\displaystyle(q)$
$\displaystyle:=\exists_{\left(n\colon\mathbb{Z}\right)}\left(\mathsf{pr_{2}}(\chi_{n})<q\right).$

The idea of $L$ is that a rational number is less than the represented number
if there is an interval in the sequence that it is smaller than the lower
endpoint of. The idea of $R$ is the opposite of this. The first four
properties of the cuts (Section 5.3.2) are proved by properties of the
dyadics, while the fifth is by the nested property and the sixth is by the
positioned property.

Any interval that has dyadic endpoints with the same denominator can be
represented as a triple of integers.

[ ] We call a triple of integers $(k,c,p)\colon\mathbb{Z}^{3}$ such that
$k\leq c$ (the proof term of which we leave implicit) a _dyadic interval code_
when we use it for the purpose of representing the dyadic interval
$\mathsf{\mathbb{Z}^{3}{\text{-}}to{\text{-}}\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}}(k,c,p):=(\iota(k,p),\iota(c,p))\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}$
(which has width $\frac{c-k}{2^{p}}$).

Given a sequence of dyadic interval codes
$\chi\colon\mathbb{Z}\to\mathbb{Z}^{3}$, we overload terminology by saying
$\chi$ is nested/positioned to mean that
$\mathsf{map}(\mathsf{\mathbb{Z}^{3}{\text{-}}to{\text{-}}\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}},\chi)$
is nested/positioned.

[ ] If a sequence of dyadic interval codes
$\chi\colon\mathbb{Z}\to\mathbb{Z}^{3}$ is nested and positioned, it
represents the real number
$\llparenthesis\chi\rrparenthesis^{\prime}:=\llparenthesis\mathsf{map}(\mathsf{\mathbb{Z}^{3}{\text{-}}to{\text{-}}\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}},\chi)\rrparenthesis\colon\mathbb{R}$.

###### Proof.

[$\mathsf{t}$] By Section 5.3.2.

The dyadic intervals underlying the structure of $\mathbb{T}$ (illustrated in
Figure 5.10) can be represented by pairs of integers.

[ ] We call a pair of integers $(k,p)\colon\mathbb{Z}^{2}$ a _ternary interval
code_ when we use it for the purpose of representing the interval
$\mathsf{\mathbb{Z}^{2}{\text{-}}to{\text{-}}\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}}(k,p):=(\iota(k,p),\iota(k+2,p))\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}$
(which has width $\frac{1}{2^{p-1}}$).

Furthermore, every ternary interval code $(k,p)$ gives a dyadic interval code

$\mathsf{\mathbb{Z}^{2}{\text{-}}to{\text{-}}\mathbb{Z}^{3}}(k,p):=(k,k+2,p),$

such that the below diagram commutes.

${\mathbb{Z}^{2}}$${\mathbb{Z}^{3}}$${\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}}$$\scriptstyle{\mathsf{\mathbb{Z}^{2}{\text{-}}to{\text{-}}\mathbb{Z}^{3}}}$$\scriptstyle{\mathsf{\mathbb{Z}^{2}{\text{-}}to{\text{-}}\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}}}$$\scriptstyle{\mathsf{\mathbb{Z}^{3}{\text{-}}to{\text{-}}\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}}}$

Given a sequence of ternary interval codes
$\chi\colon\mathbb{Z}\to\mathbb{Z}^{2}$, we overload terminology by saying
$\chi$ is nested/positioned to mean that
$\mathsf{map}(\mathsf{\mathbb{Z}^{2}{\text{-}}to{\text{-}}\mathbb{Z}[\nicefrac{{1}}{{2}}]^{I}},\chi)$
is nested/positioned.

[ ] If sequence of ternary interval codes
$\chi\colon\mathbb{Z}\to\mathbb{Z}^{2}$ is nested and positioned, it
represents the real number
$\llparenthesis\chi\rrparenthesis^{\prime\prime}:=\llparenthesis\mathsf{map}(\mathsf{\mathbb{Z}^{2}{\text{-}}to{\text{-}}\mathbb{Z}^{3}},\chi)\rrparenthesis^{\prime}\colon\mathbb{R}$.

###### Proof.

[$\mathsf{t}$] By Section 5.3.2.

For sequences of ternary interval codes, being positioned is implied by a
stronger property we call the _normalised_ property. A sequence of such
interval codes is normalised if the precision-level of the output interval is
always identical to that which was requested.

[ ] A sequence of ternary interval codes is _normalised_ if the precision-
level of the code at every point $n\colon\mathbb{N}$ is always exactly $n$.

$\displaystyle\mathsf{normalised}$
$\displaystyle:(\mathbb{Z}\to\mathbb{Z}^{2})\to\Omega,$
$\displaystyle\mathsf{normalised}$
$\displaystyle(\chi):=\Pi_{\left(n\colon\mathbb{N}\right)}\left(\mathsf{pr_{2}}(\chi_{n})=n\right).$

[ ] 555In Agda, the formalisation of this proof currently requires the use of
a number of unformalised lemmas about dyadic numbers. If a sequence of ternary
interval codes is normalised, then it is positioned.

###### Proof.

Recall from Section 5.3.2 that, given some
$\varepsilon\colon\mathbb{Z}[\nicefrac{{1}}{{2}}]>0$ we wish to find an
interval in the sequence whose width is at most $\varepsilon$.

We define $q\colon\mathbb{Z}$ to be any integer such that
$\frac{2}{2^{q}}<\varepsilon$. By the normalised property,
$q=pr_{2}(\chi_{q})$ and, by definition of ternary interval codes, $\chi_{q}$
has width $\frac{2}{2^{q}}$, which is smaller than $\varepsilon$.

If a sequence of ternary interval codes
$\chi\colon\mathbb{Z}\to\mathbb{Z}^{2}$ is normalised, we can effectively
discard the precision-level information in the output and simply consider it
as an integer sequence
$\mathsf{map}(\mathsf{pr_{1}},\chi)\colon\mathbb{Z}\to\mathbb{Z}$. Further, if
$\chi$ is nested, then $\mathsf{map}(\mathsf{pr_{1}},\chi)$ is ternary
(Section 5.3.1).

[ ] 666In Agda, the formalisation of the proof of this lemma currently
requires the use of a number of unformalised lemmas about dyadic numbers.
Given a normalised sequence of ternary interval codes, it is nested if and
only if it is ternary.

As the resulting integer sequence is ternary, it is clearly a ternary Boehm
encoding (Section 5.3.1). Indeed, the type of ternary interval codes that are
nested and positioned are _equivalent_ to the type of ternary Boehm encodings
$\mathbb{T}$.

[ ] We define the inclusion map from ternary Boehm encodings to sequences of
ternary interval codes by the following:

$\displaystyle\mathsf{to{\text{-}}interval{\text{-}}seq}$
$\displaystyle:\mathbb{T}\to(\mathbb{Z}\to\mathbb{Z}^{2}),$
$\displaystyle\mathsf{to{\text{-}}interval{\text{-}}seq}$
$\displaystyle(\chi)_{n}:=(\chi_{n},n).$

[ ] The type of nested and normalised sequences of ternary interval codes that
are equivalent to the type of ternary Boehm encodings:

$\sum_{\left(\chi\colon\mathbb{Z}\to\mathbb{Z}^{2}\right)}\left(\mathsf{nested}(\mathsf{map}(\mathsf{pr_{1}},\chi))\times\mathsf{normalised}(\chi)\right)\simeq\mathbb{T}.$

###### Proof.

[$\mathsf{f}$] Converting from $\mathbb{T}\to(\mathbb{Z}\to\mathbb{Z}^{2})$ is
done by $\mathsf{to{\text{-}}interval{\text{-}}seq}$, while converting in the
other direction is done by $\mathsf{map}(\mathsf{pr_{1}})$; in both cases, we
prove the necessary properties of the constructed representation using Section
5.3.2. It is then trivial to see that these two functions yield identities.

[ ] Any given ternary Boehm encoding $x\colon\mathbb{T}$ represents the real
number

$\llbracket x\rrbracket:=\llparenthesis\lambda
n.(x_{n},n)\rrparenthesis^{\prime\prime}\colon\mathbb{R}.$

###### Proof.

[$\mathsf{ft}$] By Sections 5.3.2 and 5.3.2.

####  5.3.3 Exact real arithmetic

Boehm defines arithmetic operations on CR by looking to the interval
arithmetic on the dyadic rational intervals [Boe20]. In this subsection we
follow this same process in order to informally define negation, addition and
multiplication on $\mathbb{T}$. The definitions here differ to those on CR
because elements of $\mathbb{T}$ are different to those of CR (for example we
must satisfy the ternary property, Section 5.3.1); furthermore, we give
simpler, more convenient definitions than Boehm’s, though this is at the
expense of some efficiency.

Note that the definitions of this subsection are informal — we do not define
these operations in our formal library and have not verified their
correctness; indeed, this is ongoing work as discussed in Section 7.2.2. We
will, however, use these definitions in our own proof-of-concept Java library
for exact real search on ternary Boehm encodings in Chapter 6.

##### Negation

Negation on dyadic intervals is defined by

$-\left[\frac{k}{2^{p}},\frac{c}{2^{p}}\right]:=\left[\frac{-c}{2^{p}},\frac{-k}{2^{p}}\right].$

Hence, negation on dyadic interval codes $\mathbb{Z}^{3}$ is defined by
$-(k,c,p):=(-c,-k,p)$. The width of the output interval is the same as that of
the input interval, meaning that if the input was in fact a ternary interval
code $\mathbb{Z}^{2}$, then the output also would be a ternary interval code
on the same precision-level. Therefore, we can easily define negation on
ternary Boehm encodings.

_Negation_ on ternary Boehm encodings is defined by the following:

$\displaystyle-$ $\displaystyle:\mathbb{T}\to\mathbb{T},$ $\displaystyle-$
$\displaystyle x:=\lambda n.-x_{n}-2.$

##### Addition

Addition on dyadic intervals is defined by

$\left[\frac{k_{1}}{2^{p_{1}}},\frac{c_{1}}{2^{p_{1}}}\right]+\left[\frac{k_{2}}{2^{p_{2}}},\frac{c_{2}}{2^{p_{2}}}\right]:=\\\
\left[\frac{2^{p_{2}-\mathsf{min}(p_{1},p_{2})}k_{1}+2^{p_{1}-\mathsf{min}(p_{1},p_{2})}k_{2}}{2^{\mathsf{max}(p_{1},p_{2})}},\frac{2^{p_{2}-\mathsf{min}(p_{1},p_{2})}c_{1}+2^{p_{1}-\mathsf{min}(p_{1},p_{2})}c_{2}}{2^{\mathsf{max}(p_{1},p_{2})}}\right].$

As we are looking to define this operation on $\mathbb{T}$, whereon we can
approximate the elements to any precision-level we like, we can consider the
simpler case where the precision-levels of the inputs are identical. Hence,
addition on dyadic interval codes $\mathbb{Z}^{3}$ in the case where the
precision-levels of the inputs is identical is defined by
$(k_{1},c_{1},p)+(k_{2},c_{2},p):=(k_{1}+k_{2},c_{1}+c_{2},p)$. The width of
the output interval in this case is

$\frac{(c_{1}+c_{2})-(k_{1}+k_{2})}{2^{p}},$

meaning that given two ternary interval codes on precision-level $p$ the width
would be

$\frac{(k_{1}+2+k_{2}+2)-(k_{1}+k_{2})}{2^{p}}=\frac{1}{2^{p-2}}.$

In order to achieve an output interval approximation of a ternary Boehm
encoding at a requested precision-level $p\colon\mathbb{Z}$, therefore, the
input ternary Boehm encodings must be evaluated to precision-level $p+2$.

_Addition_ on ternary Boehm encodings is defined by the following:

$\displaystyle+$ $\displaystyle:\mathbb{T}\to\mathbb{T}\to\mathbb{T},$
$\displaystyle x$ $\displaystyle+y$ $\displaystyle:=\lambda
n.(x_{n+2}+y_{n+2}).$

##### Multiplication

Multiplication on dyadic intervals is defined by

$\left[\frac{k_{1}}{2^{p_{1}}},\frac{c_{1}}{2^{p_{1}}}\right]*\left[\frac{k_{2}}{2^{p_{2}}},\frac{c_{2}}{2^{p_{2}}}\right]:=\left[\frac{\mathsf{min}(k_{1}k_{2},k_{1}c_{2},c_{1}k_{2},k_{2}c_{2})}{2^{p_{1}+p_{2}}},\frac{\mathsf{max}(k_{1}k_{2},k_{1}c_{2},c_{1}k_{2},k_{2}c_{2})}{2^{p_{1}+p_{2}}}\right].$

As with addition, we can consider the simpler case where the precision-levels
of the inputs are identical. Hence, multiplication on dyadic interval codes
$\mathbb{Z}^{3}$ in the case where the precision-levels of the inputs is
identical is defined by
$(k_{1},c_{1},p)*(k_{2},c_{2},p):=(\mathsf{min}(k_{1}k_{2},k_{1}c_{2},c_{1}k_{2},k_{2}c_{2}),\mathsf{max}(k_{1}k_{2},k_{1}c_{2},c_{1}k_{2},k_{2}c_{2}),2p)$.
The width of the output interval varies based on the inputs — this is related
to the fact that multiplication is continuous but not uniformly continuous. In
the case where both intervals are positive, for example, the width of the
output interval is

$\frac{((k_{1}+2)(k_{2}+2))-k_{1}k_{2}}{2^{2p}}=\frac{k1+k2+2}{2^{2p-1}}=\frac{1}{2^{2p-1-\mathsf{log2}(k1+k2+2)}}.$

This case in fact supercedes all others, and so in order to achieve an output
interval approximation of a ternary Boehm encoding at a requested precision-
level $p\colon\mathbb{Z}$, the input ternary Boehm encodings must be evaluated
to precision-level
$(p+\mathsf{log2}(\mathsf{abs}(k_{1})+\mathsf{abs}(k_{2})+2)+1)/2$.

_Multiplication_ on ternary Boehm encodings is defined by the following:

$\displaystyle*$ $\displaystyle:\mathbb{T}\to\mathbb{T}\to\mathbb{T},$
$\displaystyle x$ $\displaystyle*y$ $\displaystyle:=\lambda
n.(x_{(n+\mathsf{log2}(\mathsf{abs}(x_{n})+\mathsf{abs}(y_{n})+2)+1)/2}+y_{(n+\mathsf{log2}(\mathsf{abs}(x_{n})+\mathsf{abs}(y_{n})+2)+1)/2}).$

####  5.3.4 Representing compact intervals

A key difference between ternary Boehm encodings $\mathbb{T}$ and ternary
signed-digit encodings ${\mathbb{3}^{\mathbb{N}}}$ is that with the former we
can represent real numbers across the real line, whereas with the latter we
can only represent reals in a given compact interval (in this thesis, we use
the example of $[-1,1]$). However, $\mathbb{T}$ is not a uniformly continuous
searchable type — in order to search the ternary Boehm encodings, we will have
to restrict ourselves to particular compact intervals. In this subsection, we
define three subtypes of $\mathbb{T}$ that can be used to represent real
numbers that are in the compact interval
$[\frac{k}{2^{i}},\frac{k+2}{2^{i}}]$, which is represented by the ternary
interval code $(k,i)\colon\mathbb{Z}^{2}$.

The first subtype $\mathbb{T}(k,i)_{1}$ is straightforward to define: it is
simply the type of ternary Boehm encodings which ‘pass through’ the interval
encoded by $(k,i)$ at precision-level $i$.

[ ] For every ternary interval code $(k,i)\colon\mathbb{Z}^{2}$ there is a
subtype $\mathbb{T}(k,i)_{1}$ of _ternary Boehm encodings in the compact
interval $[\frac{k}{2^{i}},\frac{k+2}{2^{i}}]$_ defined as the collection of
ternary Boehm encodings that feature the interval approximation $(k,i)$:

$\mathbb{T}(k,i)_{1}:=\sum_{\left(x\colon\mathbb{T}\right)}\left(x_{i}=k\right).$

This subtype is useful because it is easy to map back to elements of
$\mathbb{T}$ by simply taking the first projection.

The second subtype $\mathbb{T}(k,i)_{2}$ is a little less convenient to work
with directly, but is more convenient for the purpose of defining a closeness
function (which we will do in Chapter 6). Elements
$x\colon\mathbb{T}(k,i)_{2}$ are $\mathbb{N}$-indexed sequences that only give
the interval approximations of the represented real number $\llbracket
x\rrbracket$ for precision-levels greater than $i$ — i.e. for any
$n\colon\mathbb{N}$, an interval approximation of $\llbracket x\rrbracket$ is
represented by the interval code $(x_{n},i+1+n)\colon\mathbb{Z}^{2}$.

[ ] For every ternary interval code $(k,i)\colon\mathbb{Z}^{2}$ there is a
subtype $\mathbb{T}(k,i)_{2}$ of _ternary Boehm encodings in the compact
interval $[\frac{k}{2^{i}},\frac{k+2}{2^{i}}]$_ defined as the collection of
sequences of type $\mathbb{Z}^{\mathbb{N}}$ that locate, after the interval
approximation $(k,i)$, any ternary Boehm encoding:

$\mathbb{T}(k,i)_{2}:=\sum_{\left(\chi\colon\mathbb{Z}^{\mathbb{N}}\right)}\left(\chi_{0}\
\mathsf{below}\ k\times\Pi_{\left(n\colon\mathbb{N}\right)}\left(\chi_{n+1}\
\mathsf{below}\ \chi_{n}\right)\right).$

We can convert from each of these definitions to the other.

[ ] Given any ternary interval code $(k,i)\colon\mathbb{Z}^{2}$, the function

$\mathbb{T}(k,i)_{1}\mathsf{{\text{-}}to{\text{-}}}\mathbb{T}(k,i)_{2}:\mathbb{T}(k,i)_{1}\to\mathbb{T}(k,i)_{2}$

is defined for every $((x,b),e)\colon\mathbb{T}(k,i)_{1}$ where

  * •

$x\colon\mathbb{Z}\to\mathbb{Z}$,

  * •

$b\colon\mathsf{ternary}(x)$,

  * •

$e\colon x_{i}=k$.

We first define the sequence

$\displaystyle\chi$ $\displaystyle:\mathbb{Z}^{\mathbb{N}},$
$\displaystyle\chi$ ${}_{n}:=x_{i+1+n}.$

The proof that $(\chi_{0}\ \mathsf{below}\ k)$ is then by
$b_{i}\colon(x_{i+1}\ \mathsf{below}\ x_{i})$ and $e$; the proof that
$\Pi_{\left(n\colon\mathbb{N}\right)}\left(\chi_{n+1}\ \mathsf{below}\
\chi_{n}\right)$ is by $b$.

[ ] Given any ternary interval code $(k,i)\colon\mathbb{Z}^{2}$, the function

$\mathbb{T}(k,i)_{2}\mathsf{{\text{-}}to{\text{-}}}\mathbb{T}(k,i)_{1}:\mathbb{T}(k,i)_{2}\to\mathbb{T}(k,i)_{1}$

is defined for every $(\chi,b_{0},b_{s})\colon\mathbb{T}(k,i)_{2}$ where

  * •

$\chi\colon\mathbb{Z}^{\mathbb{N}}$,

  * •

$b_{0}\colon\chi_{0}\ \mathsf{below}\ k$,

  * •

$b_{s}\colon\Pi_{\left(n\colon\mathbb{N}\right)}\left(\chi_{n+1}\
\mathsf{below}\ \chi_{n}\right)$.

We first define the sequence

$\displaystyle x$ $\displaystyle:\mathbb{Z}\to\mathbb{Z},$ $\displaystyle x$
${}_{n}:=k\ \ $ $\displaystyle\text{\emph{(when $n=i$)}},$ $\displaystyle x$
${}_{n}:=\chi_{n-1-i}\ \ $ $\displaystyle\text{\emph{(when $n>i$)}},$
$\displaystyle x$ ${}_{n}:=\mathsf{upRight}(k)\ \ $
$\displaystyle\text{\emph{(when $n<i$)}}.$

The proof that $(\mathsf{ternary}(x))$ is then by $b_{0}$ and $b_{s}$; the
proof that $x_{n}=k$ is immediate.

Despite the fact that, given a particular interval code
$(k,i)\colon\mathbb{Z}^{2}$, the types $\mathbb{T}(k,i)_{1}$ and
$\mathbb{T}(k,i)_{2}$ can represent the same real numbers, the types are not
equivalent. This is because $\mathbb{T}(k,i)_{1}$ contains more information
about locating the represented real number than $\mathbb{T}(k,i)_{2}$, and
this information cannot be recovered when converting from the latter to the
former — indeed, in Section 5.3.4 we used the $\mathsf{upRight}$ function to
prepend arbitrary interval approximations of the real number for precision-
levels higher than $i$. Despite this, it _is_ the case that the composition of
the two functions defined above preserves the represented real number. The
informal idea of this is that from precision-level $i\colon\mathbb{Z}$ the
ternary Boehm encoding (and thus, the underlying dyadic interval
approximations) are identical — hence, the limit of the two sequences is the
same real number.

We now connect the two representations of real numbers in compact intervals
that we use in this thesis, and show that the second subtype defined in this
subsection is equivalent to the type of ternary Boehm encodings.

[ ] Given any ternary interval code $(k,i)\colon\mathbb{Z}^{2}$, it is the
case that $\mathbb{T}(k,i)_{2}\simeq{\mathbb{3}^{\mathbb{N}}}$.

###### Proof (Sketch)..

[$\mathsf{f}$] Although the formalisation is rather involved, the intuition
here is clear. We convert any ternary Boehm encoding in a compact interval
$\chi\colon\mathbb{T}(k,i)_{2}$ into a ternary signed-digit encoding
$\alpha\colon{\mathbb{3}^{\mathbb{N}}}$ by using the values of
$b_{0}\colon\chi_{0}\ \mathsf{below}\ k$ and
$b_{s}\colon\prod_{\left(n\colon\mathbb{N}\right)}\chi_{n+1}\ \mathsf{below}\
\chi_{n}$. If, at any point $n\colon\mathbb{N}$ in the sequence, $\chi_{n}$
goes $\mathsf{downLeft}$ then $\alpha_{n}=\overline{1}$; if $\chi_{n}$ goes
$\mathsf{downMid}$ then $\alpha_{n}=0$; and else if $\chi_{n}$ goes
$\mathsf{downRight}$ then $\alpha_{n}=1$. Following the opposite method, we
can also convert in the other direction; and clearly either composition of
these conversions gives an identity.

Finally, we give the third subtype for representing compact intervals using
$\mathbb{T}$. We can remove the redundant interval approximations from the
structure of $\mathbb{T}(k,i)_{2}$, which reflects the ability to represent
the same real number as any ternary signed-digit encoding
${\mathbb{3}^{\mathbb{N}}}$ as a function $\mathbb{N}\to\mathbbm{2}$
(discussed in Section 5.2.1).

[ ] Given two integers $n,m\colon\mathbb{Z}$, we say that $n$ is _split-below_
$m$ if $n$ is either $\mathsf{downLeft}\ m$ or $\mathsf{downRight}\ m$:

$\displaystyle\mathsf{split{\text{-}}below}$
$\displaystyle:\mathbb{Z}\to\mathbb{Z}\to\Omega,$ $\displaystyle n\ $
$\displaystyle\mathsf{split{\text{-}}below}\ m$
$\displaystyle:=(n=\mathsf{downLeft}\ m)+(n=\mathsf{downRight}\ m).$

[ ] For every ternary Boehm interval code $(k,i)\colon\mathbb{Z}^{2}$ there is
a subtype $\mathbb{T}(k,i)_{3}$ of _ternary Boehm encodings in the compact
interval $[\frac{k}{2^{i}},\frac{k+2}{2^{i}}]$_ defined as the collection of
sequences of type $\mathbb{Z}^{\mathbb{N}}$ that locate, after the interval
approximation $(k,i)$, only those ternary Boehm encodings that never use
$\mathsf{downMid}$:

$\mathbb{T}(k,i)_{3}:=\sum_{\left(\chi\colon\mathbb{N}\to\mathbb{Z}\right)}\left(\chi_{0}\
\mathsf{split{\text{-}}below}\
k\times\Pi_{\left(n\colon\mathbb{N}\right)}\left(\chi_{n+1}\
\mathsf{split{\text{-}}below}\ \chi_{n}\right)\right).$

Therefore, this subtype defined is equivalent to the Cantor type
$\mathbbm{2}^{\mathbb{N}}$, as at each interval approximation there are two
choices for the next.

[ ] Given any ternary Boehm interval code $(k,i)\colon\mathbb{Z}^{2}$, it is
the case that $\mathbb{T}(k,i)_{3}\simeq\mathbbm{2}^{\mathbb{N}}$.

###### Proof.

[$\mathsf{f}$] Similar to Section 5.3.4.

Split-belowness trivially implies belowness, and hence every element of
$\mathbb{T}(k,i)_{3}$ can be mapped to one in $\mathbb{T}(k,i)_{2}$ — and,
hence, one in $\mathbb{T}(k,i)_{3}$ — all of which represent the same real
number.

As discussed in Section 5.2.1, there is a problem when using the Cantor type
$\mathbbm{2}^{\mathbb{N}}$ for representing real numbers: namely, it is
unsuitable for computation due to its lack of redundant digits. This problem
extends to the equivalent subtype $\mathbb{T}(k,i)_{3}$, and so it is
important to understand that we do not (and indeed cannot) use this type for
computation in our framework. The reason for its introduction here is instead
for the purposes of _search_ — in Section 6.2.1, we will see that it is this
subtype which is most suitable for searching the type of ternary Boehm
encodings in the given compact interval
$\left[\frac{k}{2^{i}},\frac{k+2}{2^{i}}\right]$ (for any
$(k,i)\colon\mathbb{Z}^{2}$). Indeed, this further means that the type
$\mathbbm{2}^{\mathbb{N}}$ is suitable for searching ternary signed-digit
encodings, as we explore in Section 6.1.1.

## Chapter 6 Exact Real Search

Our generalised framework for search, optimisation and regression introduced
in Chapters 3 and 4 has been shown to operate on a wide class of types.
Optimisation takes place on totally bounded (Section 3.2.4) closeness spaces
(Section 3.2.2) equipped with a preorder (Section 4.1.1) and approximate
linear preorder (Section 4.1.1); whereas search takes place on uniformly
continuously searchable (Section 3.3.1) closeness spaces — further, recall
that totally boundedness implies uniformly continuous searchability (Theorem
3.3.1). Regression can take place on either of the above classes of closeness
space, depending on whether we perform it via optimisation (Theorem 4.2.1) or
search (Theorems 4.2.2 and 4.2.3).

In this thesis’ final chapter, we bring this generalised framework full circle
by instantiating it on the two representations of real numbers we explored and
verified in Chapter 5: ternary signed-digits and ternary Boehm encodings. In
order to achieve this, we formalise that each type’s representations of real
numbers in compact intervals — i.e. ${\mathbb{3}^{\mathbb{N}}}$ itself for the
former and the subtype $\mathbb{T}(k,i)_{3}$ for any given
$(k,i)\colon\mathbb{Z}^{2}$ (Section 5.3.4) for the latter — are members of
the aforementioned class of types, in that we can perform search, optimisation
and regression on them. We then formalise, only for
${\mathbb{3}^{\mathbb{N}}}$, that the exact real arithmetic functions we wish
to search, optimise and regress are indeed uniformly continuous functions —
proofs that are required for the algorithms to run. Finally, we give a variety
of toy, proof-of-concept examples of search, optimisation and regression using
these functions.

On signed-digit encodings, our example Haskell algorithms are compiled
directly from instantiations of the formal Agda proofs of convergence (we
explain how in the final paragraph of Appendix A). This means that, while the
extracted computation is relatively inefficient, we have formalised the fact
that it will compute a correct answer. Meanwhile, our examples of the
framework working on ternary Boehm encodings are written in a Java library
which informally reflects the ideas of the formal framework; we sacrifice
direct proofs of convergence in order to attain more efficient proof-of-
concept algorithms.

###  6.1 Exact Real Search using signed-digit encodings

Some of the work of this section was previously published as part of a joint
paper with Dan R. Ghica at the _Logic in Computer Science (LICS) 2021_
conference [GA21].

####  6.1.1 Suitability for search, optimisation and regression

In this subsection, we show that the type of ternary signed digit encodings
${\mathbb{3}^{\mathbb{N}}}$ — explored in Section 5.2 — is a member of our
class of types in that we can perform search, optimisation and regression upon
it. We show, therefore, that ${\mathbb{3}^{\mathbb{N}}}$ is a totally bounded
and uniformly continuously searchable closeness space with a preorder and
approximate linear preorder.

#####  ${\mathbb{3}^{\mathbb{N}}}$ is a continuously searchable closeness
space

The closeness space on ${\mathbb{3}^{\mathbb{N}}}$ is a discrete-sequence
closeness space (Section 3.2.5), as the type $\mathbb{3}$ is finite and,
therefore, discrete. Further, by the finiteness of $\mathbb{3}$, this
closeness space is totally bounded.

[ ] The type of ternary signed-digit encodings ${\mathbb{3}^{\mathbb{N}}}$ is
a totally bounded closeness space.

###### Proof.

[$\mathsf{f}$] Because $\mathbb{3}$ is finite and discrete, the result follows
from Section 3.2.5.

There are two proofs of uniformly continuous searchability we can employ for
${\mathbb{3}^{\mathbb{N}}}$. The first is directly from the above fact that
${\mathbb{3}^{\mathbb{N}}}$ is totally bounded: this yields the _totally
bounded uniformly continuous searcher_.

[ ] [ ] The closeness space of ternary signed-digit encodings
${\mathbb{3}^{\mathbb{N}}}$ is uniformly continuously searchable.

###### Proof 1.

By Sections 6.1.1 and 3.3.1.

The second proof is inspired instead by Berger’s searcher on the Cantor space
and Escardó’s on countable product spaces (which we formalised in Section
3.3.3): this yields the _decreasing-modulus uniformly continuous searcher_.

###### Proof 2.

By Section 3.3.2.

In the examples given in Section 6.1.3, it will become apparent that the
totally bounded searcher is almost always more efficient than the decreasing-
modulus searcher; specifically, the decreasing-modulus searcher is only better
in Section 6.1.3.

By combining the proofs of Section 6.1.1 with the examples in Sections 3.2.5,
3.3.2 and 3.3.3, we further have (among other things) that arbitrary products
of ${\mathbb{3}^{\mathbb{N}}}$ are uniformly continuously searchable and
totally bounded closeness spaces. However, we do not usually wish to search
${\mathbb{3}^{\mathbb{N}}}$ _directly_ , because (as discussed in Section 5.2)
there are infinitely-many redundant representations of any number that
features a $0$, and so a direct searcher will have inherent inefficiencies.
Instead, we search ${\mathbb{3}^{\mathbb{N}}}$ _indirectly_ using the Cantor
type $\mathbbm{2}^{\mathbb{N}}$. Recall that every real number in $[-1,1]$ can
be represented as a sequence $\mathbb{N}\to\\{-1,1\\}$ and, hence, by using
$0$ for $-1$, as a sequence $\mathbbm{2}^{\mathbb{N}}$. We can therefore
trivially define the following inclusion map from $\mathbbm{2}^{\mathbb{N}}$
to ${\mathbb{3}^{\mathbb{N}}}$:

[ ] We define the inclusion map
$-^{\uparrow}\colon\mathbbm{2}^{\mathbb{N}}\to{\mathbb{3}^{\mathbb{N}}}$ that
converts representations of $[-1,1]$ as Cantor sequences
$\mathbbm{2}^{\mathbb{N}}$ to ternary signed-digit encodings of the same
number by mapping every $0$ to $\overline{1}$.

Using this map, which is trivially uniformly continuous, we can convert a
uniformly continuous function $f\colon{\mathbb{3}^{\mathbb{N}}}\to X$, for any
closeness space $X$, into a uniformly continuous function
$f^{\uparrow}\colon\mathbbm{2}^{\mathbb{N}}\to X$ with the same modulus of
uniform continuity. For our examples, therefore, we usually convert the
uniformly continuous predicates and functions on ${\mathbb{3}^{\mathbb{N}}}$
that we wish to search, optimise and regress into ones on
$\mathbbm{2}^{\mathbb{N}}$ that we can search, optimise and regress indirectly
using uniformly continuous searchers on $\mathbbm{2}^{\mathbb{N}}$.

[ ] The Cantor type $\mathbbm{2}^{\mathbb{N}}$ is a totally bounded closeness
space.

###### Proof.

[$\mathsf{f}$] Because $\mathbbm{2}$ is finite and discrete, the result
follows from Section 3.2.5.

[ ] [ ] The Cantor closeness space $\mathbbm{2}^{\mathbb{N}}$ is uniformly
continuously searchable.

###### Proof 1.

By Sections 6.1.1 and 3.3.1.

###### Proof 2.

By Section 3.3.2.

#####  ${\mathbb{3}^{\mathbb{N}}}$ has an approximate linear preorder

A preorder on ${\mathbb{3}^{\mathbb{N}}}$ is given by the lexicographic order
(Section 4.1.1), whereas an approximate linear preorder is given by the
approximate lexicographic order (Section 4.1.1). Recall that these are defined
by the following:

$\displaystyle\alpha$ $\displaystyle\leq_{\mathbb{3}^{\mathbb{N}}}\beta$
$\displaystyle:=\Pi_{\left(n\colon\mathbb{N}\right)}\left(\alpha\sim^{n}\beta\to\alpha_{n}\leq_{D}\beta_{n}\right),$
$\displaystyle\alpha$
$\displaystyle\leq^{\varepsilon}_{\mathbb{3}^{\mathbb{N}}}\beta$
$\displaystyle:=\Pi_{\left(n\colon\mathbb{N}\right)}\left(n<\varepsilon\to\alpha\sim^{n}\beta\to\alpha_{n}\leq_{D}\beta_{n}\right).$

However, it is not appropriate to use these orders for optimisation and
regression on ternary signed-digit encodings, because the lexicographic
ordering of the representations of type ${\mathbb{3}^{\mathbb{N}}}$ does not
amount to the numerical ordering of the real numbers of type $\mathbb{I}$. As
an example, consider the following different representations
$z\alpha,z\beta\colon{\mathbb{3}^{\mathbb{N}}}$ of $0\colon\mathbb{I}$:

$z\alpha:=01\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\ldots\text{
and
}z\beta:=1\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\ldots.$

By the above lexicographic order on ${\mathbb{3}^{\mathbb{N}}}$, it is the
case that $z\alpha\leq z\beta$ but $\neg(z\beta\leq z\alpha)$. This issue also
propagates to the approximate ordering. Escardó has shown that the
lexicographic ordering on signed-digit encodings and the ordering on the
encoded numbers can indeed coincide by introducing a normalisation operator
$\mathsf{onorm}\colon{\mathbb{3}^{\mathbb{N}}}\times{\mathbb{3}^{\mathbb{N}}}\to{\mathbb{3}^{\mathbb{N}}}\times{\mathbb{3}^{\mathbb{N}}}$
[Esc98]. The idea is that the normalised pair represents the same numbers
(i.e.
$\langle\langle\alpha\rangle\rangle=\langle\langle\mathsf{pr_{1}}(\mathsf{onorm}(\alpha,\beta))\rangle\rangle$
and
$\langle\langle\beta\rangle\rangle=\langle\langle\mathsf{pr_{2}}(\mathsf{onorm}(\alpha,\beta))\rangle\rangle$)
but that, on the normalised pair, the lexicographic and numerical orderings
coincide.

We take a simpler approach to the problem, and utilise the equivalence between
${\mathbb{3}^{\mathbb{N}}}$ and the type $\mathbb{T}(-1,0)_{2}$ of ternary
Boehm encodings used for representing the interval $[-1,1]$. This equivalence,
given in Section 5.3.4, yields a ‘normalisation’ map

$\mathsf{integer{\text{-}}approx}\colon{\mathbb{3}^{\mathbb{N}}}\to(\mathbb{N}\to\mathbb{Z}),$

where the $n$th integer $k$ of the sequence
$\mathsf{integer{\text{-}}approx}(\alpha)$, for any
$\alpha\colon{\mathbb{3}^{\mathbb{N}}}$, refers to the $n$th ternary interval
code (Section 5.3.2) approximation of $\alpha$ — i.e., the interval
$\left[\frac{k}{2^{n}},\frac{k+2}{2^{n}}\right]$, in which
$\langle\langle\alpha\rangle\rangle$ lies. Any two signed-digit encodings
whose $n$-prefixes evaluate to the same interval approximations will therefore
have the same value of $k$.

Figure 6.1: Illustration of the interval approximation evaluations of
$z\alpha:=01\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\ldots$
and
$z\beta:=1\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\ldots$
at the first three precision-levels.

The formal definition of the normalisation map is given in Section 6.1.1, and
its use is informally visualised in Figure 6.1, which shows the relationship
between the evaluations of $z\alpha$ and $z\beta$ and their normalised
interval approximations. From this illustration, we can read off that

$\mathsf{integer{\text{-}}approx}(z\alpha):=-1,-1,0,0,\ldots\text{ and
}\mathsf{integer{\text{-}}approx}(z\beta):=-1,0,0,0,\ldots.$

[ ] The _normalisation map_
$\mathsf{integer{\text{-}}approx}\colon{\mathbb{3}^{\mathbb{N}}}\to(\mathbb{N}\to\mathbb{Z})$,
which maps every ternary signed-digit encoding
$\alpha\colon{\mathbb{3}^{\mathbb{N}}}$ to a sequence of integers such that,
for any $\alpha\colon{\mathbb{3}^{\mathbb{N}}}$,
$\mathsf{integer{\text{-}}approx}(\alpha)_{n}$ refers to the $n$th ternary
interval code (Section 5.3.2) approximation of $\alpha$ is defined as follows:

$\displaystyle\mathsf{\mathbb{3}{\text{-}}to{\text{-}}down}$
$\displaystyle:\mathbb{3}$ $\displaystyle\to(\mathbb{Z}\to\mathbb{Z}),$
$\displaystyle\mathsf{\mathbb{3}{\text{-}}to{\text{-}}down}$ $\displaystyle\
\overline{1}$ $\displaystyle:=\mathsf{downLeft},$
$\displaystyle\mathsf{\mathbb{3}{\text{-}}to{\text{-}}down}$ $\displaystyle\
0$ $\displaystyle:=\mathsf{downMid},$
$\displaystyle\mathsf{\mathbb{3}{\text{-}}to{\text{-}}down}$ $\displaystyle\
1$ $\displaystyle:=\mathsf{downRight},$
$\displaystyle\mathsf{integer{\text{-}}approx}^{\prime}$
$\displaystyle:\mathbb{Z}\to{\mathbb{3}^{\mathbb{N}}}\to$ $\displaystyle\
\mathbb{N}\to\mathbb{Z},$
$\displaystyle\mathsf{integer{\text{-}}approx}^{\prime}$
$\displaystyle(k,\alpha,0)$ $\displaystyle:=k,$
$\displaystyle\mathsf{integer{\text{-}}approx}^{\prime}$
$\displaystyle(k,\alpha,n+1)$
$\displaystyle:=\mathsf{integer{\text{-}}approx}^{\prime}(\mathsf{\mathbb{3}{\text{-}}to{\text{-}}down}(\mathsf{head}\
\alpha,k),\mathsf{tail}\ \alpha,n),$
$\displaystyle\mathsf{integer{\text{-}}approx}$ $\displaystyle:$
$\displaystyle{\mathbb{3}^{\mathbb{N}}}\to\mathbb{N}\to\mathbb{Z},$
$\displaystyle\mathsf{integer{\text{-}}approx}$ $\displaystyle\ \alpha$
$\displaystyle:=\mathsf{integer{\text{-}}approx}^{\prime}(\alpha,-1).$

Using the normalisation map, we define the following preorder and approximate
linear preorder on ternary signed-digit encodings ${\mathbb{3}^{\mathbb{N}}}$,
which _are_ correct with respect to the numerical ordering on the interval
object $\mathbb{I}$. However, the order on $\mathbb{I}$ is not well
established, and we have not formalised its notion or verified the correctness
of the preorder — we discuss this as further work in Section 7.2.1.

[ ] We define the _real-order preserving linear preorder_ on
${\mathbb{3}^{\mathbb{N}}}$ by using the normalisation map
$\mathsf{integer{\text{-}}approx}\colon{\mathbb{3}^{\mathbb{N}}}\to(\mathbb{N}\to\mathbb{Z})$:

$\displaystyle\leq_{\mathbb{3}^{\mathbb{N}}}$
$\displaystyle:{\mathbb{3}^{\mathbb{N}}}\to{\mathbb{3}^{\mathbb{N}}}\to\Omega,$
$\displaystyle\alpha$ $\displaystyle\leq_{\mathbb{3}^{\mathbb{N}}}\beta$
$\displaystyle:=\exists_{\left(n\colon\mathbb{N}\right)}\left(\Pi_{\left(i\colon\mathbb{N}\right)}\left(n\leq
i\to\mathsf{integer{\text{-}}approx}(\alpha)_{i}\leq\mathsf{integer{\text{-}}approx}(\beta)_{i}\right)\right).$

[ ] The real-order preserving preorder is indeed a preorder (Section 4.1.1).

###### Proof.

[$\mathsf{t}$] Using propositional truncation (recall this from Section
2.3.6), we prove both reflexivity and transitivity of the real-order
preserving preorder:

  1. (i)

For any $\alpha\colon{\mathbb{3}^{\mathbb{N}}}$, we have that
$\mathsf{integer{\text{-}}approx}(\alpha)_{i}\leq\mathsf{integer{\text{-}}approx}(\beta)_{i}$
by reflexivity of the order on the integers. Therefore, by setting $n:=0$ we
have a proof term
$(0,p)\colon\Sigma_{\left(n\colon\mathbb{N}\right)}\left(\Pi_{\left(i\colon\mathbb{N}\right)}\left(n\leq
i\to\mathsf{integer{\text{-}}approx}(\alpha)_{i}\leq\mathsf{integer{\text{-}}approx}(\beta)_{i}\right)\right)$.
The result then follows by truncating this proof term; i.e.
$|(0,p)|\colon\exists_{\left(n\colon\mathbb{N}\right)}\left(\Pi_{\left(i\colon\mathbb{N}\right)}\left(n\leq
i\to\mathsf{integer{\text{-}}approx}(\alpha)_{i}\leq\mathsf{integer{\text{-}}approx}(\beta)_{i}\right)\right)$.

  2. (ii)

Given $\alpha,\beta,\zeta\colon{\mathbb{3}^{\mathbb{N}}}$ such that
$\alpha\leq_{\mathbb{3}^{\mathbb{N}}}\beta$ and
$\beta\leq_{\mathbb{3}^{\mathbb{N}}}\zeta$, we wish to show that
$\alpha\leq_{\mathbb{3}^{\mathbb{N}}}\zeta$. To do this, we define a function
$f\colon\Sigma_{\left((n,m)\colon\mathbb{N}\times\mathbb{N}\right)}{(\Pi_{\left(i\colon\mathbb{N}\right)}\left(n\leq
i\to\mathsf{integer{\text{-}}approx}(\alpha)_{i}\leq\mathsf{integer{\text{-}}approx}(\beta)_{i}\right)}$
$\times(m\leq
i\to\mathsf{integer{\text{-}}approx}(\beta)_{i}\leq\mathsf{integer{\text{-}}approx}(\zeta)_{i}))\to\exists_{\left(k\colon\mathbb{N}\right)}{}(\Pi_{\left(i\colon\mathbb{N}\right)}(k\leq
i\to$
${\mathsf{integer{\text{-}}approx}(\alpha)_{i}\leq\mathsf{integer{\text{-}}approx}(\zeta)_{i}}))$,
and the conclusion is given by the truncation of $f$. To define this function,
we simply set $k:=\mathsf{max}(n,m)$, and the proof that
$\mathsf{integer{\text{-}}approx}(\alpha)_{i}\leq\mathsf{integer{\text{-}}approx}(\zeta)_{i}$
follows by transitivity of the order on the integers.

[ ] We define the _real-order preserving approximate linear preorder_ on
${\mathbb{3}^{\mathbb{N}}}$ by using the normalisation map
$\mathsf{integer{\text{-}}approx}\colon{\mathbb{3}^{\mathbb{N}}}\to(\mathbb{N}\to\mathbb{Z})$:

$\displaystyle\leq^{-}_{\mathbb{3}^{\mathbb{N}}}$
$\displaystyle:\mathbb{N}\to{\mathbb{3}^{\mathbb{N}}}\to{\mathbb{3}^{\mathbb{N}}}\to\Omega,$
$\displaystyle\alpha$ $\displaystyle\leq^{n}_{\mathbb{3}^{\mathbb{N}}}\beta$
$\displaystyle:=\mathsf{integer{\text{-}}approx}(\alpha)_{n}\leq\mathsf{integer{\text{-}}approx}(\beta)_{n}.$

[ ] The real-order preserving approximate linear preorder is indeed an
approximate linear preorder (Section 4.1.1).

###### Proof.

The proof that, given any $\varepsilon\colon\mathbb{N}$, the relation
$\leq^{\varepsilon}_{\mathbb{3}^{\mathbb{N}}}\colon{\mathbb{3}^{\mathbb{N}}}\to{\mathbb{3}^{\mathbb{N}}}\to\Omega$
is decidable and a linear preorder is immediate from the fact that the order
on the integers is a linear preorder.

To prove that if $C_{\varepsilon}(\alpha,\beta)$ then
$\alpha\leq^{\varepsilon}_{\mathbb{3}^{\mathbb{N}}}\beta$ for all
$\alpha,\beta\colon{\mathbb{3}^{\mathbb{N}}}$, we need to show that
$\mathsf{integer{\text{-}}approx}(\alpha)_{\varepsilon}\leq\mathsf{integer{\text{-}}approx}(\beta)_{\varepsilon}$.
We first prove the following lemma:

$\alpha\sim^{\varepsilon}\beta\to\Pi_{\left(k\colon\mathbb{Z}\right)}\left(\mathsf{integer{\text{-}}approx}^{\prime}(k,\alpha,\varepsilon)=\mathsf{integer{\text{-}}approx}^{\prime}(k,\beta,\varepsilon)\right).$

We prove this lemma by induction on the given $\varepsilon$. In the base case
where $\varepsilon:=0$, then by definition of
$\mathsf{integer{\text{-}}approx}^{\prime}$ (see Section 6.1.1) we simply have
to show that $k=k$. In the inductive case where
$\varepsilon:=\varepsilon^{\prime}+1$ for some
$\varepsilon^{\prime}\colon\mathbb{N}$, then from
$\alpha\sim^{\varepsilon^{\prime}+1}\beta$ we have that $\mathsf{head}\
\alpha=\mathsf{head}\ \beta$ and therefore
$\mathbb{3}\mathsf{{\text{-}}to{\text{-}}down}(\mathsf{head}\
\alpha,k)=\mathbb{3}\mathsf{{\text{-}}to{\text{-}}down}(\mathsf{head}\
\beta,k)$; the result then follows by the inductive hypothesis.

Now that we have proved the lemma, the result follows from it, Section 3.2.5
and the reflexivity of the order on the integers.

[ ] The real-order preserving approximate linear preorder relates (by Section
4.1.1) to the real-order preserving preorder.

###### Proof.

[$\mathsf{t}$] The first condition, that if
$\alpha\leq_{\mathbb{3}^{\mathbb{N}}}\beta$ then
$\exists_{\left(n\colon\mathbb{N}\right)}{\Pi_{\left(\varepsilon\colon\mathbb{N}\right)}(n<\varepsilon\to\alpha\leq^{\varepsilon}_{\mathbb{3}^{\mathbb{N}}}\beta)}$,
is immediate, because the types are identical. The second condition, that if
$x\leq^{n}_{\mathbb{3}^{\mathbb{N}}}y$ holds for all $n\colon\mathbb{N}$ then
$x\leq_{\mathbb{3}^{\mathbb{N}}}y$ follows by truncating the proof term of
type
$\Sigma_{\left(n\colon\mathbb{N}\right)}\Pi_{\left(\varepsilon\colon\mathbb{N}\right)}(n<i\to\alpha\leq^{i}_{\mathbb{3}^{\mathbb{N}}}\beta)$,
which is constructed by setting $n:=0$ and using the proof $f(i)\colon
x\leq^{i}_{\mathbb{3}^{\mathbb{N}}}y$.

####  6.1.2 Uniformly continuous exact real arithmetic

In order to perform exact real search on ternary signed-digit encodings, we
must prove the uniform continuity of the exact real arithmetic operations. In
this subsection, we prove that negation, binary midpoint, infinitary midpoint
and multiplication functions (all defined in Section 5.2.3) are uniformly
continuous via the closeness space ${\mathbb{3}^{\mathbb{N}}}$.

##### Sequence uniform continuity

Recall that discrete-sequence closeness spaces satisfy, for all
$n\colon\mathbb{N}$, $C_{n}(\alpha,\beta)\Leftrightarrow\alpha\sim^{n}\beta$
(Section 3.2.5); a fact which we use to give the following bespoke definitions
of uniform continuity on sequence functions and predicates on discrete types.

[ ] Given discrete types $X$ and $Y$, a unary sequence function $f\colon
X^{\mathbb{N}}\to Y^{\mathbb{N}}$ is _uniformly continuous_ if for all
$\varepsilon\colon\mathbb{N}$ there is some $\delta\colon\mathbb{N}$ such that
sequences that agree in their $\delta$-prefixes map by $f$ to sequences that
agree in their $\varepsilon$-prefixes:

$\mathsf{seq{\text{-}}f{\text{-}}ucontinuous}^{1}(f):=\\\
\Pi_{\left(\varepsilon\colon\mathbb{N}\right)}\Sigma_{\left(\delta\colon\mathbb{N}\right)}\Pi_{\left(x_{1},x_{2}\colon
X^{\mathbb{N}}\right)}(x_{1}\sim^{\delta}x_{2})\to(f(x_{1})\sim^{\varepsilon}f(x_{2})).$

[ ] Given discrete types $X$ and $Y$, a unary sequence function $f\colon
X^{\mathbb{N}}\to Y^{\mathbb{N}}$ is uniformly continuous by Section 6.1.2 if
and only if it is uniformly continuous by Section 3.2.3 from the discrete-
sequence closeness space yielded by $X$ to the discrete-sequence closeness
space yielded by $Y$.

###### Proof.

By Section 3.2.5.

We next define the binary version of discrete-sequence uniform continuity.

[ ] Given discrete types $X$, $Y$ and $Z$, a binary sequence function $f\colon
X^{\mathbb{N}}\to Y^{\mathbb{N}}\to Z^{\mathbb{N}}$ is _uniformly continuous_
if for all $\varepsilon\colon\mathbb{N}$ there are some
$\delta_{1},\delta_{2}\colon\mathbb{N}$ such that, given two pairs of sequence
arguments, if the first pair agree in their $\delta_{1}$-prefixes and the
second pair agree in their $\delta_{2}$-prefixes then together they map by $f$
to sequences that agree in their $\varepsilon$-prefixes:

$\mathsf{seq{\text{-}}f{\text{-}}ucontinuous}^{2}(f):=\Pi_{\left(\varepsilon\colon\mathbb{N}\right)}\Sigma_{\left((\delta_{1},\delta_{2})\colon\mathbb{N}\times\mathbb{N}\right)}\Pi_{\left(x_{1},x_{2}\colon
X^{\mathbb{N}}\right)}\Pi_{\left(y_{1},y_{2}\colon Y^{\mathbb{N}}\right)}\\\
\hskip
56.9055pt(x_{1}\sim^{\delta_{1}}x_{2})\to(y_{1}\sim^{\delta_{2}}y_{2})\to(f(x_{1},y_{1})\sim^{\varepsilon}f(x_{2},y_{2})).$

Note that although the proof of uniform continuity of binary sequence
functions by the above definition is logically equivalent to that using the
definition of uniform continuity on the binary product (Section 3.2.5) of two
discrete-sequence closeness functions, the former has two moduli of continuity
(one for each argument) whereas the latter has only one (i.e. the maximum of
the two). This means that the computational content of the proofs differ.

[ ] Given discrete types $X$, $Y$ and $Z$, a binary sequence function $f\colon
X^{\mathbb{N}}\to Y^{\mathbb{N}}\to Z^{\mathbb{N}}$ is uniformly continuous by
Section 6.1.2 if and only if it is uniformly continuous by Section 3.2.3 from
the binary product of the discrete-sequence closeness spaces yielded by $X$
and $Y$ to the discrete-sequence closeness space yielded by $Z$.

###### Proof.

Once again we use the equivalence of $C_{n}(\alpha,\beta)$ and
$\alpha\sim^{n}\beta$ for all $\alpha,\beta\colon D^{\mathbb{N}}$ (where $D$
is discrete) and $n\colon\mathbb{N}$; i.e. Section 3.2.5.

We first show sequence uniform continuity implies closeness uniform
continuity. By the former, given $\varepsilon\colon\mathbb{N}$,
$x_{1},x_{2}\colon X^{\mathbb{N}}$ and $y_{1},y_{2}\colon Y^{\mathbb{N}}$, we
have that there are $\delta_{1},\delta_{2}\colon\mathbb{N}$ such that if
$C_{\delta_{1}}(x_{1},x_{2})$ and $C_{\delta_{2}}(y_{1},y_{2})$ then
$C_{\varepsilon}(f(x_{1},y_{1}),f(x_{2},y_{2}))$. Therefore we take the
modulus of uniform continuity for the closeness space definition to be
$\delta:=\mathsf{max}(\delta_{1},\delta_{2})\colon\mathbb{N}$, because (by
Sections 3.2.5 and 3.2.3) $C_{\delta}((x_{1},y_{1}),(x_{2},y_{2}))$ implies
$C_{\delta_{1}}(x_{1},x_{2})$ and $C_{\delta_{2}}(y_{1},y_{2})$ and, hence,
$C_{\varepsilon}(f(x_{1},y_{1}),f(x_{2},y_{2}))$ as desired.

The other direction is more straightforward. Given
$\varepsilon\colon\mathbb{N}$, $x_{1},x_{2}\colon X^{\mathbb{N}}$ and
$y_{1},y_{2}\colon Y^{\mathbb{N}}$, we have that there is
$\delta\colon\mathbb{N}$ such that if
$C_{\delta}((x_{1},y_{1}),(x_{2},y_{2}))$ then
$C_{\varepsilon}(f(x_{1},y_{1}),f(x_{2},y_{2}))$. Therefore we take the moduli
of uniform continuity for the sequence definition to be
$(\delta,\delta)\colon\mathbb{N}\times\mathbb{N}$, because (by Section 3.2.5)
$C_{\delta}((x_{1},y_{1}),(x_{2},y_{2}))$ implies $C_{\delta}(x_{1},x_{2})$
and $C_{\delta}(y_{1},y_{2})$ and, hence,
$C_{\varepsilon}(f(x_{1},y_{1}),f(x_{2},y_{2}))$ as desired.

Lastly, we define a specialisation of uniform continuity on certain infinitary
sequence functions that on discrete types is logically equivalent to uniform
continuity on the dependent product (Section 3.2.5) of a discrete-sequence
closeness type.

[ ] Given discrete types $X$ and $Y$, an infinitary sequence function
$f\colon(X^{\mathbb{N}})^{\mathbb{N}}\to Y^{\mathbb{N}}$ is _uniformly
continuous_ if for all $\varepsilon\colon\mathbb{N}$ there are
$d,\delta\colon\mathbb{N}$ such that infinitary sequences whose $d$-prefixes
agree in their respective $\delta$-prefixes map by $f$ to sequences that agree
in their $\varepsilon$-prefixes:

$\mathsf{seq{\text{-}}f{\text{-}}ucontinuous}^{\mathbb{N}}(f):=\Pi_{\left(\varepsilon\colon\mathbb{N}\right)}\Sigma_{\left((d,\delta)\colon\mathbb{N}\times\mathbb{N}\right)}\\\
\big{(}(d\leq\delta)\times(\Pi_{\left(\alpha,\beta\colon(X^{\mathbb{N}})^{\mathbb{N}}\right)}\Pi_{\left(n\colon\mathbb{N}\right)}(n<d)\to(\alpha_{n}\sim^{\delta}\beta_{n})\to(f(\alpha)\sim^{\varepsilon}f(\beta)))\big{)}.$

[ ] Given discrete types $X$ and $Y$, an infinitary sequence function
$f\colon(X^{\mathbb{N}})^{\mathbb{N}}\to Y^{\mathbb{N}}$ is uniformly
continuous by Section 6.1.2 if and only if it is uniformly continuous by
Section 3.2.3 from the countable product of the discrete-sequence closeness
space yielded by $X$ to the discrete-sequence closeness space yielded by $Y$.

###### Proof.

We first require a relationship similar to Section 3.2.5 but for sequences
$\alpha,\beta\colon(X^{\mathbb{N}})^{\mathbb{N}}$. Recall from the definition
of countable product closeness functions (Section 3.2.5) and the accompanying
visualisation of the diagonalisation argument (Figure 3.1) that for all
$\delta\colon\mathbb{N}$ having $C_{\delta}(\alpha,\beta)$ means we have
$\alpha_{0}\sim^{\delta}\beta_{0}$, $\alpha_{1}\sim^{\delta-1}\beta_{1}$,
$\alpha_{2}\sim^{\delta-2}\beta_{2}$, etc.; i.e., for all $n\colon\mathbb{N}$
such that $n<\delta$ we have $\alpha_{n}\sim^{\delta-n}\beta_{n}$. Therefore,
we conclude the following relationship:

  1. (i)

$C_{2\delta}(\alpha,\beta)\to\Pi_{\left(n\colon\mathbb{N}\right)}\left(n<\delta\to\alpha_{n}\sim^{\delta}\beta_{n}\right)$,

  2. (ii)

$\Pi_{\left(n\colon\mathbb{N}\right)}\left(n<\delta\to\alpha_{n}\sim^{\delta}\beta_{n}\right)\to
C_{\delta}(\alpha,\beta)$.

From this relationship, we prove the logical equivalence between the two
definitions of uniform continuity.

We first show sequence uniform continuity implies closeness uniform
continuity. By the former, given $\varepsilon\colon\mathbb{N}$,
$\alpha,\beta\colon(X^{\mathbb{N}})^{\mathbb{N}}$ we have that there are
$d,\delta^{\prime}\colon\mathbb{N}$ such that $d\leq\delta^{\prime}$ and such
that if $\alpha_{n}\sim^{\delta^{\prime}}\beta_{n}$ for all $n<d$ then (by
Section 3.2.5) $C_{\varepsilon}(f(\alpha),f(\beta))$. To show that closeness
uniform continuity is satisfied, we need to give some $\delta\colon\mathbb{N}$
such that if $C_{\delta}(\alpha,\beta)$ then
$C_{\varepsilon}(f(\alpha),f(\beta))$. We set $\delta:=2{\delta^{\prime}}$, as
by (i) this means we have $\alpha_{n}\sim^{\delta^{\prime}}\beta_{n}$ for all
$n<\delta^{\prime}$, and therefore for all $n<d\leq\delta^{\prime}$. By
sequence uniform continuity as described, we hence have
$C_{\varepsilon}(f(\alpha),f(\beta))$.

The other direction is again more straightforward. Given
$\alpha,\beta\colon(X^{\mathbb{N}})^{\mathbb{N}}$ we have by closeness uniform
continuity that there is some $\delta^{\prime}\colon\mathbb{N}$ such that if
$C_{\delta}(\alpha,\beta)$ then $C_{\epsilon}(f(\alpha),f(\beta))$. To show
that sequence uniform continuity is satisfied, we need to give some
$d,\delta\colon\mathbb{N}$ such that $d\leq\delta$ and such that if
$\alpha_{n}\sim^{\delta}\beta_{n}$ for all $n<d$ then
$C_{\varepsilon}(f(\alpha),f(\beta))$. We set both
$d,\delta:=\delta^{\prime}$, as by (ii) this means we have
$C_{\delta}(\alpha,\beta)$. By closeness continuity as described, we hence
have $C_{\varepsilon}(f(\alpha),f(\beta))$.

Now we have specialised definitions of uniform continuity for discrete-
sequence types which will aid us in proving our operations on
${\mathbb{3}^{\mathbb{N}}}$ are uniformly continuous. Before doing this, we
note some expected facts about discrete-sequence uniform continuity.

The identity function on discrete-sequences is uniformly continuous and
composition of discrete-sequence functions preserves discrete-sequence uniform
continuity.

###### Proof (Sketch)..

Similar to Section 3.2.3.

[ ] For any discrete types $X$ and $Y$, given any function $f\colon X\to Y$,
the function $\mathsf{map}(f)\colon X^{\mathbb{N}}\to Y^{\mathbb{N}}$ is
discrete-sequence uniformly continuous.

###### Proof.

For every $\varepsilon\colon\mathbb{N}$ the modulus of uniform continuity is
$\varepsilon$ itself, because $\alpha_{\varepsilon}=\beta_{\varepsilon}$ gives
$\left(\mathsf{map}(f,\alpha)_{\varepsilon}=\mathsf{map}(f,\beta)_{\varepsilon}\right):=\left(f(\alpha_{\varepsilon})=f(\beta_{\varepsilon})\right)$
using $\mathsf{ap}$.

[ ] For any discrete types $X$, $Y$ and $Z$, given any function $f\colon X\to
Y\to Z$, the function $\mathsf{zipWith}(f)\colon X^{\mathbb{N}}\to
Y^{\mathbb{N}}\to Z^{\mathbb{N}}$ is discrete-sequence uniformly continuous.

###### Proof.

Similar to Section 6.1.2.

We now explicitly prove the uniform continuity, via the above discrete-
sequence definitions (and hence, by the logical equivalences set out above and
the discreteness of $\mathbb{3}$, via the necessary closeness space
definitions) of the functions $\mathsf{neg}$, $\mathsf{mid}$,
$\mathsf{bigMid}$ and $\mathsf{mul}$. This task takes up the rest of this
subsection.

##### Negation

First, we prove the uniform continuity of negation.

[ ] Negation on signed-digits encodings is a uniformly continuous function.

###### Proof.

Recall from Section 5.2.3 that negation is defined
$\mathsf{neg}:=\mathsf{map}(\mathsf{flip})$; therefore this is immediately
uniformly continuous by Section 6.1.2.

##### Binary midpoint

Next, the uniform continuity of binary midpoint is slightly more complex.

[ ] The function
$\mathsf{div2}\colon\mathbb{5}^{\mathbb{N}}\to{\mathbb{3}^{\mathbb{N}}}$ is
uniformly continuous.

###### Proof.

By its recursive definition (Section 5.2.3), it can be seen that determining
the value of $\mathsf{div2}(\alpha)_{\varepsilon}$ relies only on
$\alpha_{\varepsilon}$ and $\alpha_{{\varepsilon+1}}$. Therefore,
${\varepsilon+1}$ is the modulus of uniform continuity for a given
$\varepsilon$.

[ ] Binary midpoint on signed-digit encodings is a uniformly continuous
function.

###### Proof.

Recall from Section 5.2.3 that binary midpoint is defined
$\mathsf{mid}(\alpha,\beta):=\mathsf{div2}(\mathsf{zipWith}(\mathsf{add\mathbb{3}}(\alpha,\beta)))$.
The $\mathsf{zipWith}$ function is uniformly continuous by Section 6.1.2 and
the $\mathsf{div2}$ function is uniformly continuous by Section 6.1.2.
Therefore, the composed function $\mathsf{mid}$ is uniformly continuous by
Section 6.1.2.

##### Infinitary midpoint

Before we come to multiplication, we must first prove the infinitary midpoint
function is uniformly continuous.

[ ] The function
$\mathsf{bigMid^{\prime}}\colon({\mathbb{3}^{\mathbb{N}}})^{\mathbb{N}}\to\mathbb{9}^{\mathbb{N}}$
is uniformly continuous.

###### Proof.

By induction on the requested precision $\varepsilon\colon\mathbb{N}$. In the
base case, recall from Section 5.2.3 that
$\mathsf{bigMid}^{\prime}(\zeta)_{0}$ only uses $(\zeta_{0})_{0}$,
$(\zeta_{0})_{1}$ and $(\zeta_{1})_{0}$; therefore $d,\delta:=2$. In the
inductive case, recall from Section 5.2.3 that
$\mathsf{bigMid}^{\prime}(\zeta)_{{\varepsilon+1}}:=\mathsf{bigMid}^{\prime}(\mathsf{mid}(\mathsf{tail}(\mathsf{tail}\
\zeta_{0}),\mathsf{tail}\ \zeta_{1})::(\mathsf{tail}(\mathsf{tail}\ \zeta)))$.
The argument is the composition of the successor, composition and binary
midpoint functions, all of which are uniformly continuous (for binary
midpoint, see Section 6.1.2); therefore, the function is uniformly continuous
by the inductive hypothesis and Section 6.1.2.

[ ] The function
$\mathsf{div4}\colon\mathbb{9}^{\mathbb{N}}\to{\mathbb{3}^{\mathbb{N}}}$ is
uniformly continuous.

###### Proof.

Similar argument to Section 6.1.2.

[ ] Infinitary midpoint on signed-digit encodings is a uniformly continuous
function.

###### Proof.

Recall from Section 5.2.3 that infinitary midpoint is defined
$\mathsf{bigMid}:=\mathsf{div4}\circ\mathsf{bigMid}^{\prime}$. The result
follows by Sections 6.1.2 and 6.1.2.

##### Multiplication

Finally, the uniform continuity of multiplication follows from the above.

[ ] Multiplication on signed-digit encodings is a uniformly continuous
function.

###### Proof.

Recall from Section 5.2.3 that multiplication is defined
$\mathsf{mul}(\alpha,\beta):=\mathsf{bigMid}(\mathsf{zipWith}(\mathsf{digitMul},\alpha,\lambda
n.\beta))$. This is uniformly continuous by Sections 6.1.2, 6.1.2 and 6.1.2.

####  6.1.3 Agda-extracted examples

We have developed, within the TypeTopology library, a large framework of Agda
proofs concerning searchable types, generalised optimisation and regression
and ternary signed-digit encodings. The true test of this framework is in
extracting some proof-of-concept computational algorithms of our generalised
framework on ${\mathbb{3}^{\mathbb{N}}}$. The Agda code is compiled into
Haskell as described in Appendix A, which allows it to run faster than if we
ran it directly in Agda — though the extracted algorithms are still slow. The
reader can try these examples themselves by following the instructions in
Appendix A.

Whether we are searching for an answer to a predicate or optimising/regressing
a function up to a given precision $\varepsilon\colon\mathbb{N}$, our
algorithms will — using the witness of uniform continuity — effectively
compute a finite prefix of a sequence such that any sequence with that prefix
will be a correct answer, approximate minimum or satisfactory parameter of the
model function.

For each example, we give a table which notes the answer
$x\colon{\mathbb{3}^{\mathbb{N}}}$ computed for the requested precision-level
$\varepsilon\colon\mathbb{N}$. In the few cases where we search
${\mathbb{3}^{\mathbb{N}}}$ _directly_ 111Recall the discussion on direct and
indirect search from Section 6.1.1 each answer is given as a finite prefix and
then an ellipses ‘$\ldots$’ to notate the infinitely many $0$s our algorithm
repeats after the computed prefix. In the usual case where we search
${\mathbb{3}^{\mathbb{N}}}$ _indirectly_ , and hence $x$ is mapped from a
sequence of type $\mathbbm{2}^{\mathbb{N}}$ using the map defined in Section
6.1.1), the ellipses ‘$\ldots$’ instead denotes the infinitely-many
$\overline{1}$s that the algorithm repeats after the computed prefix. To aid
illustration, we also note which real $\langle\langle
x\rangle\rangle\colon\mathbb{R}$ it is that $x$ represents and we often give
further such information, such as the represented value $\langle\langle
f(x)\rangle\rangle$ when we are minimising a particular function $f$. We note
any times above one second taken to compute this answer222For reference, all
of our examples are computed using a MacBook Air M1 laptop., which grows
quickly due to the inefficiency of our underlying arithmetic and the
exhaustive nature of our search (further discussions on this folllow in
Section 6.2).

Note that, for ease of reading, we abuse notation and often write functions
and representations on ${\mathbb{3}^{\mathbb{N}}}$ as if they are those
numbers they represent on the reals $\mathbb{I}$. For example, we write
$\frac{1}{4}$ instead of $\overline{1}::(1::(\overline{1}::\mathsf{repeat}\
1))$ — but recall that all of these algorithms operate on the representations
of the reals.

##### Uniformly continuous search

Search on ternary signed-digit encodings has been performed previously, for
example by Escardó in Haskell [Esc11a]. However, we still provide four
examples of uniformly continuous search as proof-of-concept examples of our
explicit-continuity assumptions.

######  Example 6.1.0.

[ ] We search for a ternary signed-digit encoding
$x\colon{\mathbb{3}^{\mathbb{N}}}$ that satisfies

$p(x):=\frac{-x}{2}\leq^{\varepsilon}\frac{1}{4},$

for a variety of requested precision values $\varepsilon\colon\mathbb{N}$
indirectly using the uniformly continuous searcher derived from the totally
boundedness of $\mathbbm{2}^{\mathbb{N}}$ (i.e. the first proof of Section
6.1.1).

The decidability and uniform continuity of the predicate
$p\colon{\mathbb{3}^{\mathbb{N}}}\to\Omega$ is ensured by that of the
approximate linear preorder (Section 4.1.1), the uniform continuity of
$\mathsf{mid}$ (Sections 6.1.2 and 6.1.2) and the composition of these
(Section 3.2.3).

$\varepsilon$ | $x$ | $\langle\langle x\rangle\rangle$ | $\frac{-\langle\langle x\rangle\rangle}{2}$ | Time (s)
---|---|---|---|---
$5$ | $1\ldots$ | $0$ | $0$ |
$10$ | $1\ldots$ | $0$ | $0$ |
$15$ | $1\ldots$ | $0$ | $0$ | 1.09
$20$ | $1\ldots$ | $0$ | $0$ | 24.88

Not long after this, the searcher causes a stack overflow. This was not
unexpected: recall that the totally bounded searcher in must compute a
$2^{\delta}$-sized $\delta$-net of $\mathbbm{2}^{\mathbb{N}}$ in advance of
the search.

We next try using the indirect uniformly continuous searcher derived from the
decreasing-modulus uniformly continuous searcher of $\mathbbm{2}^{\mathbb{N}}$
(i.e. the second proof of Section 6.1.1).

$\varepsilon$ | $x$ | $\langle\langle x\rangle\rangle$ | $\frac{-\langle\langle x\rangle\rangle}{2}$ | Time (s)
---|---|---|---|---
$3$ | $\overline{1}1\ldots$ | $-0.5$ | $0.25$ |
$6$ | $\overline{1}\overline{1}1\ldots$ | $-0.515625$ | $0.2578125$ |
$9$ | $\overline{1}\overline{1}11\ldots$ | $-0.501953125$ | $0.25097656$ | 35.68

This searcher doesn’t have the overflow problem, but is in this case less
efficient than the totally bounded searcher (likely because the proof of the
decreasing-modulus searcher is more computationally expensive). Note also that
the two searchers computed different answers; this is because the order in
which they evaluate candidate solutions differs — though of course, both are
correct up to the requested precision.

The totally bounded searcher in these examples is usually more efficient, but
sometimes (due to the difference in search strategy) the decreasing-modulus
searcher is better. As in this section we wish to illustrate the correctness
of our algorithms, and not their efficiency, from now on we use whichever
searcher allows us to produce better results for the given example.

######  Example 6.1.0.

[ ] We search for a ternary signed-digit encoding
$x\colon{\mathbb{3}^{\mathbb{N}}}$ that satisfies

$p(x):=C_{\varepsilon}(\mathsf{mul}(x,x),\frac{1}{2}),$

for a variety of requested precision values $\varepsilon\colon\mathbb{N}$
indirectly using the totally bounded uniformly continuous searcher on
$\mathbbm{2}^{\mathbb{N}}$.

The decidability and uniform continuity of the predicate
$p\colon{\mathbb{3}^{\mathbb{N}}}\to\Omega$ is ensured by that of the
closeness relation (Section 3.2.3), the uniform continuity of $\mathsf{mul}$
(Section 6.1.2) and the composition of these (Section 3.2.3).

$\varepsilon$ | $x$ | $\langle\langle x\rangle\rangle$ | $\langle\langle\mathsf{mul}(x,x)\rangle\rangle$ | Time (s)
---|---|---|---|---
$1$ | $\ldots$ | $-1$ | $1$ |
$2$ | $\overline{1}\overline{1}1\ldots$ | $-0.75$ | $0.5625$ |
$3$ | $\overline{1}\overline{1}1\ldots$ | $-0.75$ | $0.5625$ |
$4$ | $11\overline{1}11\ldots$ | $0.6875$ | $0.47265625$ |
$5$ | $\overline{1}\overline{1}1\overline{1}\overline{1}1\ldots$ | $-0.71875$ | $0.516601563$ | 3.32
$6$ | $11\overline{1}11\overline{1}1\ldots$ | $0.703125$ | $0.494384766$ | 24.19

The answer correctly converges towards $\pm\sqrt{0.5}=\pm
0.707106781187\ldots$; indeed, it flips between approximations of the two
answers for different levels of precision.

At $\varepsilon:=7$, there was a stack overflow. But the decreasing-modulus
searcher did not produce an answer in two minutes for $n:=4$. Therefore, this
search is much less efficient than that in Section 6.1.3; this is because
multiplication requires much higher degrees of input precision than negation
and binary midpoint.

######  Example 6.1.0.

[ ] We search for a pair of ternary signed-digit encodings
$(x,y)\colon{\mathbb{3}^{\mathbb{N}}}\times{\mathbb{3}^{\mathbb{N}}}$ that
satisfy

$p(x,y):=C_{\varepsilon}(\mathsf{mid}(x,y),0),$

for a variety of requested precision values $\varepsilon\colon\mathbb{N}$
indirectly using the totally bounded uniformly continuous searcher on
$\mathbbm{2}^{\mathbb{N}}\times\mathbbm{2}^{\mathbb{N}}$.

The decidability and uniform continuity of the predicate
$p\colon{\mathbb{3}^{\mathbb{N}}}\to\Omega$ is ensured by that of the
closeness relation (Section 3.2.3), the uniform continuity of $\mathsf{mid}$
(Section 6.1.2) and the composition of these (Section 3.2.3).

$\varepsilon$ | $x,y$ | $\langle\langle x\rangle\rangle,\langle\langle y\rangle\rangle$ | $\langle\langle\mathsf{mid}(x,y)\rangle\rangle$ | Time (s)
---|---|---|---|---
$5$ | $11111\ldots,$ | $0.9375,$ | $-0.03125$ | 9.84
| $\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\ldots$ | $-1$ |  |
$10$ | $1111111111\ldots,$ | $0.998046875,$ | $-0.000976563$ |
| $\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\overline{1}\ldots$ | $-1$ |  | 75.5

We have shown we can search for two answers in parallel; although this
predicate was particularly well-suited to the search strategy of our
exhaustive searcher.

##### Global optimisation

Using the optimisation algorithm (Theorem 4.1.1), we can optimise any function
of ternary signed-digit encodings composed from $\mathsf{neg}$,
$\mathsf{mid}$, $\mathsf{bigMid}$ and $\mathsf{mul}$ — including multivariable
and stream functions — to any degree of precision. We give two examples of
this.

As global optimisation must evaluate a $\delta$-net of candidates (for a
required degree of input precision $\delta\colon\mathbb{N}$ for the requested
output precision) in advance of the optimisation process _and_ must check each
one of these candidates, we find that it very quickly becomes inefficient.

######  Example 6.1.0.

[ ] We compute an $\varepsilon$-global minimum of the function

$f(x):=\mathsf{neg}(x)$

for a variety of requested precision values $\varepsilon\colon\mathbb{N}$
indirectly using the totally bounded property of $\mathbbm{2}^{\mathbb{N}}$.

The continuity of the function $f$ is by Section 6.1.2.

$\varepsilon$ | $x$ | $\langle\langle x\rangle\rangle$ | $\langle\langle f(x)\rangle\rangle$ | Time (s)
---|---|---|---|---
$10$ | $1111111111\ldots$ | $0.998046875$ | $-0.999511719$ | 7.68
$11$ | $11111111111\ldots$ | $0.999023438$ | $-0.999511719$ | 30.23
$12$ | $111111111111\ldots$ | $0.999511719$ | $-0.999511719$ | 117.18

######  Example 6.1.0.

[ ] We compute an $\varepsilon$-global minimum of the function

$f(x):=\mathsf{mul}(x,x)$

for a variety of requested precision values $\varepsilon\colon\mathbb{N}$
indirectly using the totally bounded property of $\mathbbm{2}^{\mathbb{N}}$.

The continuity of the function $f$ is by Section 6.1.2.

$\varepsilon$ | $x$ | $\langle\langle x\rangle\rangle$ | $\langle\langle f(x)\rangle\rangle$ | Time (s)
---|---|---|---|---
$1$ | $\overline{1}\ldots$ | $-1$ | $1$ |
$2$ | $1\overline{1}\ldots$ | $0$ | $0$ | 1.54
$3$ | $1\overline{1}\ldots$ | $0$ | $0$ | 81.33

Although the same answer is returned each time, the larger $\varepsilon$
values means, especially due to the modulus of uniform continuity of
exponentiation, an exponentially larger $\delta$-net to exhaust; hence the
large jump between the time taken for $\varepsilon:=2$ and $\varepsilon:=3$.

##### Parametric regression

For regression on ternary signed-digits, we follow the model outlined in
Section 4.2.1. This means that we will be performing regression where the
oracle $\mathcal{O}$ is a function and the loss function used is the least-
closeness pseudocloseness (Section 3.2.6) function defined from a given vector
$v\colon({\mathbb{3}^{\mathbb{N}}})^{n}$ of $n$-many predictor observations.
Recall that this means the algorithm will only have access to the oracle at
the outcomes of the given observations.

Using the regression-as-_optimisation_ algorithm (Theorem 4.2.1), we can find
an $\varepsilon$-best choice parameter for any uniformly continuous function.

######  Example 6.1.0.

[ ] By fixing the predictor observations
$v:=\\{-1,0,1\\}\colon({\mathbb{3}^{\mathbb{N}}})^{3}$, we define the least-
closeness pseudocloseness function $L_{v}\colon(X\to Y)\to(X\to
Y)\to\mathbb{N}_{\infty}$ between functions, which compares their values at
the points in $v$. For the oracle function

$\mathcal{O}(x):=\mathsf{mid}(\frac{1}{3},x),$

we compute an $\varepsilon$-best choice parameter
$p\colon{\mathbb{3}^{\mathbb{N}}}$ of the parameterised model function

$M(p,x):=\mathsf{mid}(\mathsf{neg}(p),x)$

for a variety of requested precision values $\varepsilon\colon\mathbb{N}$
indirectly by maximising the function $\left(\lambda
p.L_{v}(\mathcal{O},M(p^{\uparrow}))\right)\colon\mathbbm{2}^{\mathbb{N}}\to\mathbb{N}_{\infty}$.The
shape of the model function matches the oracle function exactly, except for
the fact that the parameter is negated – we therefore expect the computed
parameter to be close to $-\frac{1}{3}$.

The continuity of the model function is by Sections 6.1.2, 6.1.2 and 6.1.2.

$\varepsilon$ | $p$ | $\langle\langle p\rangle\rangle$ | Time (s)
---|---|---|---
$2$ | $\overline{1}1\overline{1}\ldots$ | $-0.25$ |
$4$ | $\overline{1}1\overline{1}1\overline{1}\ldots$ | $-0.3125$ |
$6$ | $\overline{1}1\overline{1}1\overline{1}1\overline{1}\ldots$ | $-0.328125$ |
$8$ | $\overline{1}1\overline{1}1\overline{1}1\overline{1}1\overline{1}\ldots$ | $-0.33203125$ | 1.26
$10$ | $\overline{1}1\overline{1}1\overline{1}1\overline{1}1\overline{1}1\overline{1}\ldots$ | $-0.333007813$ | 13.79

The optimisation has returned the value that best connects the observations;
with this parameter, the regressed function clearly matches the true oracle up
to the requested precision.

It is often more practical to use _search_ for regression; i.e. to use the
algorithms derived from Theorems 4.2.2 and 4.2.3, depending on whether or not
there is distortion present in the oracle function.

######  Example 6.1.0.

[ ] For the same predictor observations $v$, oracle $\mathcal{O}$ and
parameterised model function $M$ as in Section 6.1.3, we search for a
parameter $p\colon{\mathbb{3}^{\mathbb{N}}}$ such that

$\underline{\varepsilon}\preceq L_{v}(\mathcal{O},M(p)),$

for a variety of requested precision values $\varepsilon\colon\mathbb{N}$
indirectly using the totally bounded uniformly continuous searcher on
$\mathbbm{2}^{\mathbb{N}}$.

$\varepsilon$ | $p$ | $\langle\langle p\rangle\rangle$ | Time (s)
---|---|---|---
$4$ | $\overline{1}1\overline{1}\ldots$ | $-0.25$ |
$8$ | $\overline{1}1\overline{1}1\overline{1}1\overline{1}\ldots$ | $-0.328125$ | 2.20
$12$ | $\overline{1}1\overline{1}1\overline{1}1\overline{1}1\overline{1}1\overline{1}\ldots$ | $-0.333007813$ | 9.07
$16$ | $\overline{1}1\overline{1}1\overline{1}1\overline{1}1\overline{1}1\overline{1}1\overline{1}1\overline{1}\ldots$ | $-0.333343506$ | 37.18

Although the parameter is not necessarily $\varepsilon$-best choice, compared
to Section 6.1.3 the search routine is quicker and (due to lack of distortion
in the oracle) the regressed function still matches the true oracle up to the
requested precision.

We continue this example by exploring what happens when we receive outcome
observations that are distorted from the true oracle.

######  Example 6.1.0.

[ ] For the same predictor observations $v$, oracle $\mathcal{O}$ and
parameterised model function $M$ as in Section 6.1.3, we search for a
parameter $p\colon{\mathbb{3}^{\mathbb{N}}}$ such that

$\underline{\varepsilon}\preceq L_{v}(\Psi(\mathcal{O}),M(p)),$

directly using the decreasing-modulus uniformly continuous searcher on
${\mathbb{3}^{\mathbb{N}}}$, for a variety of requested precision values
$\varepsilon\colon\mathbb{N}$.
$\Psi\colon({\mathbb{3}^{\mathbb{N}}}\to{\mathbb{3}^{\mathbb{N}}})\to({\mathbb{3}^{\mathbb{N}}}\to{\mathbb{3}^{\mathbb{N}}})$
is a distortion function that distorts the oracle like so:

$\Psi(\mathcal{O}):=\lambda x.\mathcal{O}(\mathsf{mid}(x,\frac{1}{4})).$

The graph below shows the true oracle function $\mathcal{O}$ (in red) plotted
against the distorted oracle function $\Psi(\mathcal{O})$ (in brown), the
latter of which the searcher can query at points $-1$, $0$ and $1$.

$-1$$-0.5$$0.5$$1$$-0.6$$-0.4$$-0.2$$0.2$$x$$f(x)$

$\varepsilon$ | $p$ | $\langle\langle p\rangle\rangle$
---|---|---
$1$ | $0\overline{1}\ldots$ | $-0.25$
$2$ | $0\overline{1}\ldots$ | $-0.25$
$3$ | $1111\ldots$ | $0.9375$

After precision-level $\varepsilon:=2$, the searcher cannot find a parameter
$p$ that allows the least-close points (either $M(p,-1)$ and
$\Psi(\mathcal{O}(-1))$, $M(p,0)$ and $\Psi(\mathcal{O}(0))$, or $M(p,1)$ and
$\Psi(\mathcal{O}(1))$) to become $\varepsilon$-close.

However, we could instead simply use optimisation to find the
$\varepsilon$-best choice parameter.

######  Example 6.1.0.

[ ] For the same predictor observations $v$, oracle $\mathcal{O}$,
parameterised model function $M$ and distortion function $\Psi$ as in Section
6.1.3, we compute an $\varepsilon$-best choice parameter
$p\colon{\mathbb{3}^{\mathbb{N}}}$ of $M$ for a variety of requested precision
values $\varepsilon\colon\mathbb{N}$ directly using the totally bounded
property of ${\mathbb{3}^{\mathbb{N}}}$.

$\varepsilon$ | $p$ | $\langle\langle p\rangle\rangle$ | Time (s)
---|---|---|---
$1$ | $\overline{1}1\ldots$ | $-0.25$ |
$2$ | $\overline{1}11\ldots$ | $-0.125$ |
$3$ | $\overline{1}111\ldots$ | $-0.0625$ |
$7$ | $\overline{1}1111111\ldots$ | $-0.00390625$ | 138.13

The graph below shows the true oracle function $\mathcal{O}$ (in red) plotted
against the distorted oracle function $\Psi(\mathcal{O})$ (in brown) and the
function $M(p^{7})$ (in blue) where $p^{7}$ is the $p$ computed when
$\varepsilon:=7$, for the interval $[-1,1]$

$-1$$-0.5$$0.5$$1$$-0.6$$-0.4$$-0.2$$0.2$$0.4$$x$$f(x)$

Our final example for this section is inspired by linear regression.

######  Example 6.1.0.

[ ] By fixing the predictor observations
$v:=\\{-\frac{1}{2},\frac{1}{2}\\}\colon({\mathbb{3}^{\mathbb{N}}})^{2}$, we
define the least-closeness pseudocloseness function $L_{v}\colon(X\to
Y)\to(X\to Y)\to\mathbb{N}_{\infty}$ between functions, which compares their
values at the points in $v$. We employ the parameterised model function

$M((p_{1},p_{2}),x):=\mathsf{mid}(p_{1},\mathsf{mul}(p_{2},x))$

to search for a parameters $p_{1},p_{2}\colon{\mathbb{3}^{\mathbb{N}}}$ such
that

$\underline{\varepsilon}\preceq L_{v}(\mathcal{O},M(p_{1},p_{2})),$

for a variety of precision values $\varepsilon\colon\mathbb{N}$ where
$\mathcal{O}$ is the synthetically-constructed oracle function (Section 4.2.2)

$\mathcal{O}:=M(\frac{1}{3},-1).$

The continuity of the model function is by Sections 6.1.2, 6.1.2 and 6.1.2.

$\varepsilon$ | $p_{1}$ | $p_{2}$ | $\langle\langle p_{1}\rangle\rangle$ | $\langle\langle p_{2}\rangle\rangle$ | Time (s)
---|---|---|---|---|---
$3$ | $1\overline{1}\ldots$ | $11\ldots$ | $0.5$ | $0.5$ |
$4$ | $1\overline{1}1\overline{1}\ldots$ | $11\ldots$ | $0.375$ | $0.5$ | 2.30
$5$ | $1\overline{1}1\overline{1}1\overline{1}\ldots$ | $11\ldots$ | $0.34375$ | $0.5$ | 15.65

The graph below shows the oracle function $\mathcal{O}$ (in red) plotted
against the function $M((p_{i})^{5})$ (in blue) where $(p_{i})^{5}$ are the
$p_{i}$ computed when $\varepsilon:=5$, for the interval $[-1,1]$

$-1$$-0.5$$0.5$$1$$0.1$$0.2$$0.3$$0.4$$x$$f(x)$

Thus we have concluded that we can indeed perform uniformly continuous search
and generalised global optimisation and parametric regression on ternary
signed-digits. The correctness of the algorithms are immediate, because they
are extracted from our formal Agda framework, but we enjoyed illustrating this
fact. Unfortunately, but not unexpectedly, the efficiency of the algorithms
leaves a lot to be desired.

###  6.2 Exact Real Search using ternary Boehm encodings

The signed-digits have provided a proof-of-concept for applying our
generalised perspective of optimisation and regression to types for
representing real numbers. Furthermore, we have verified the signed-digits, so
that we are genuinely optimising/regressing representations of functions on
the compact interval we are searching.

There are, however, clear problems with using signed-digits for potential
practical applications of exact real search, which can be summed up in two
points. Firstly, the arithmetic defined on the signed-digits is not user-
friendly in the same way that, say, arithmetic on the floating-point numbers
are — we cannot even perform addition using signed-digit numbers without
utilising multiple representations of different intervals. Secondly,