# Limits of real numbers in the binary signed digit representation

Franziskus Wiesnet  University of Trento, Via Sommarive 14, 38123 Povo and
Ludwig-Maximilians Universität, Theresienstr. 39, 80333 München
<EMAIL_ADDRESS>Nils Köpp  Ludwig-Maximilians Universität,
Theresienstr. 39, 80333 München<EMAIL_ADDRESS>
###### Abstract

We extract verified algorithms for exact real number computation from
constructive proofs. To this end we use a coinductive representation of reals
as streams of binary signed digits. The main objective of this paper is the
formalisation of a constructive proof that real numbers are closed with
respect to limits. All the proofs of the main theorem and the first
application are implemented in the Minlog proof system and the extracted terms
are further translated into Haskell. We compare two approaches. The first
approach is a direct proof. In the second approach we make use of the
representation of reals by a Cauchy-sequence of rationals. Utilizing
translations between the two represenation and using the completeness of the
Cauchy-reals, the proof is very short.

In both cases we use Minlog’s program extraction mechanism to automatically
extract a formally verified program that transforms a converging sequence of
reals, i.e. a sequence of streams of binary signed digits together with a
modulus of convergence, into the binary signed digit representation of its
limit. The correctness of the extracted terms follows directly from the
soundness theorem of program extraction.

As a first application we use the extracted algorithms together with Heron’s
method to construct an algorithm that computes square roots with respect to
the binary signed digit representation. In a second application we use the
convergence theorem to show that the signed digit representation of real
numbers is closed under multiplication.

###### keywords:

signed digit code, exact real number computation, coinduction, corecursion,
program extraction, realizability, Minlog, Haskell

##  1 Introduction and motivation

###  1.1 Real numbers

Real numbers can be represented in several ways. One of the best-known
representations is as Cauchy sequences of rational numbers together with a
Cauchy modulus. Namely a _Cauchy real_ is a pair $((a_{n})_{n},M)$ consisting
of a sequence $(a_{n})_{n}$ of real numbers and a modulus
$M:\mathbb{Z}^{+}\to\mathbb{N}$ such that
$\forall_{p}\forall_{n,m>M(p)}|a_{n}-a_{m}|\leq 2^{-p}$, i.e. $(a_{n})_{n}$ is
a Cauchy sequence with modulus $M$.

However, in this paper the representation of real numbers as Cauchy reals will
be just a tool. The main theorems of this paper are concerned with the signed
digit representation of real numbers.

###  1.2 Binary representation vs. signed digit representation

The binary representation of a real number $x$ in $[-1,1]$ is given by

$x=s\sum_{i=1}^{\infty}a_{i}2^{-i},$

where $s\in\\{-1,1\\}$ and $a_{i}\in\\{0,1\\}$ for every $i$. Here and further
on, by equality $=$ between two reals we mean an equivalence relation that is
compatible with the usual operations and relations on the reals. In reality
the specific of the real equality depends on the representation of real
numbers. The binary representation of some concrete real number corresponds to
a sequence of nested intervals. Reading the digits one after the other the
interval is halved in each step. Hence from the binary code we can approximate
a real number to arbitrary precision.

Figure 1: Visualization of the binary code

Now consider the other direction, i.e. given a real number, compute the binary
representation. This is not always possible, since the $\leq$-relation is not
decidable. Further it is not possible to e.g. compute the binary
representation of $\frac{x+y}{2}$ given representation of $x$ and $y$. Here
“compute” means that there is an algorithm which takes as input the binary
streams of $x$ and $y$ and generates the binary stream representing
$\frac{x+y}{2}$. In particular, the algorithm can only use finitely many
binary digits of $x$ and $y$ in order to generate finitely many binary digits
of $\frac{x+y}{2}$. For example, it is not possible to compute even the first
digit (i.e. + or -) of the average of $+\vec{0}???\cdots$ and
$-\vec{0}???\cdots$, where $\vec{0}$ is a list with entries $0$ of arbitrary
length and $?$ stands for an unknown digit. This is not possible due to the
“gaps” in the binary representation. They are illustrated in Figure 1 at $0$,
$\frac{1}{2}$, $-\frac{1}{2}$, $\frac{1}{4}$ and so on. From the first digit
of a representation of a real $x$, we can decide $0\leq x$ or $x\leq 0$, which
in general can not be done if reasoning constructively about reals. The signed
digit code fills these gaps. For a real number $x\in[-1,1]$ it is defined by

$x=\sum_{i=1}^{\infty}d_{i}2^{-i},$

where $d_{i}\in\\{\overline{1},0,1\\}$ for every $i$.

Figure 2: Visualization of the signed digit code

As the illustration in Figure 2 makes clear, to compute the first signed digit
of a real number $x\in[-1,1]$ we have to decide which of the cases $x\leq 0$,
$-\frac{1}{2}\leq 0\leq\frac{1}{2}$ or $0\leq x$ holds. Now this is possible
by application of the comparability theorem

$\forall_{x,y,z}\left(x<y\to z\leq y\vee x\leq z\right).$

Figure 2 also shows that the SD code of a real number (except $-1$ and $1$) is
not unique, whereas the binary code is “almost” everywhere unique.

A stream of signed digits is an infinite list $d_{1}d_{2}d_{3}\dots$ of
elements in

$\textbf{Sd}:=\\{\overline{1},0,1\\}.$

We will not use the signed digit streams directly, rather we use a
coinductively defined predicate ${{}^{co}\textbf{I}}$, which is given in the
next section. For a real number $x$ a realiser of $x\in{{}^{co}\textbf{I}}$ is
a signed digit stream representing $x$. The desired algorithms are given by
the extracted terms of the proofs. The soundness theorem of program extraction
[Sch21a, SW12, Wie17] gives correctness of these algorithms.

###  1.3 Historical background

One of the first paper where signed digits are used to represent real numbers,
was published by Edwin Wiedmer in 1980 [Wie80]. The idea to use coinductive
algorithms to describe the operators on the reals goes back to Alberto
Ciaffaglione and Pietro Di Gianantonio [CG06] and was revised by Ulrich Beger
and Tie Hou [BH08]. The idea to use coinductively defined predicates together
with the soundness theorem in this context is due to Ulrich Berger and Monika
Seisenberger [BS12]. The notation and definitions in this paper are taken from
[MS15] written by Kenji Miyamoto and Helmut Schwichtenberg. For the
implementation of the translations between signed-digit and cauchy-
representations in Minlog see [K1̈8].

###  1.4 Implementation in Minlog

For computing the extraced terms and verifying the correctness of the proofs,
the proof assistant Minlog [Miy17] is used. An introduction to Minlog can be
found in [Wie18] or doc/tutor.pdf in the Minlog directory. The implementation
of the proofs can be found in the file examples/analysis/sdlim.scm in the
directory of Minlog. After each proof we state its computational content not
in the notation of Minlog but in the notation of Haskell, since the runtime of
the programs in Haskell is shorter, and the terms can be defined in a more
readable way. So after each proof we give the extracted term of the proof
which was translated to Haskell using the command terms-to-haskell-program.

###  1.5 Procedure of this paper

In the next section we define a coinductively defined predicate
${{}^{co}\mathbf{I}}$ on reals. Its computational interpretation is that a
real number $x\in{{}^{co}\mathbf{I}}$ has a signed digit representation. Then
we prove some basic properties about it. In the second part of this chapter,
we introduce the predicate $\mathbf{R}$ on reals. The computational
interpretation $\mathbf{R}x$ is the existence of a sequence $as$ of rationals
and a modulus $M$ such that $as$ converges to $x$ with modulus $M$. We
conclude the second section by showing that $[-1,1]\cap\mathbf{R}$ and
${{}^{co}\mathbf{I}}$ are equivalent.

The third section contains two proofs of the main theorem. We show that the
limit of a converging sequence in ${{}^{co}\mathbf{I}}$ is again in
${{}^{co}\mathbf{I}}$. The first proof is a direct proof. Computationally it
operates on the signed digit stream of real numbers only. In the second proof
we use the equivalence between ${{}^{co}\mathbf{I}}$ and $\mathbf{R}$ and that
$\mathbf{R}$ is closed under limit, which is known as the completeness of
Cauchy-reals. In both cases the computational content of the proof is a
function which takes a stream of signed digit streams and a modulus and
returns a new signed digit stream.

The last section contains two applications of the convergence theorem. To show
the square root of a real number in ${{}^{co}\mathbf{I}}$ is again in
${{}^{co}\mathbf{I}}$ we use Heron’s method and the convergence theorem.
Lastly we consider the multiplication of two reals numbers in
${{}^{co}\mathbf{I}}$. By representing one factor as a limit of reals we
obtain a multiplication program for signed digit streams as a simple iteration
of the average function.

##  2 Formalisation

###  2.1 Notations

We use the formal theory TCF [SW12, Wie17] to formalize statements like “$x$
is represented by some signed digit stream”. In TCF all variables are typed.
The following table shows which variables have which type.

$\displaystyle m,n:\mathbb{N}\qquad\qquad$ $\displaystyle
a,b:\mathbb{Q}\qquad\qquad$ $\displaystyle M,N:\mathbb{Z}^{+}\to\mathbb{N}$
$\displaystyle d,e,k:\mathbb{Z}\qquad\qquad$ $\displaystyle
x,y:\mathbb{R}\qquad\qquad$ $\displaystyle as,bs:\mathbb{N}\to\mathbb{Q}$
$\displaystyle p,q:\mathbb{Z}^{+}\qquad\qquad$ $\displaystyle
v,u:\mathbb{S}\qquad\qquad$ $\displaystyle xs,ys:\mathbb{N}\to\mathbb{R}$

If other variables are used, their type is either not relevant or we declare
their type individually.

Here $\mathbb{N}$ are the unary natural numbers, $\mathbb{Z}$ is defined as
positive binary numbers and $\mathbb{Q}$ is given by one constructor
$\\#:\mathbb{Z}\to\mathbb{Z}^{+}\to\mathbb{Q}$. In the actual implementation
in Minlog the type of real numbers $\mathbb{R}$ is explicitly defined as the
type $(\mathbb{N}\to\mathbb{Q})\times(\mathbb{Z}^{+}\to\mathbb{N})$. In the
following proofs the concrete representation of real numbers is not important.
Therefore in the following we view $\mathbb{R}$ as an abstract datatype and
assume that we have abstract axiomatized reals with the usual operations
including addition, multiplication, less-than and an equivalence. We will
refer to explicit representation by e.g. $x\in\mathbf{R}$ and the
computational content of a proof of this statement is a witness that $x$ has
an $\mathbf{R}$-representation. Then we only have to make sure that the axioms
do not carry computational content. Axioms carrying computational content, if
needed, have to be proven for explicit representations, e.g. a statement like
$\forall_{x}(x\in\mathbf{R}\to\exists_{n}(n\in\mathbf{T}\to x\leq 2^{n}))$.

Furthermore, for an unary predicate $A$, we write $t\in A$ for $At$ and
$\forall_{t\in A}B$, $\exists_{t\in A}B$ are short for $\forall_{t}(At\to B)$
and $\exists_{t}(At\wedge B)$, respectively. Examples for these abbreviations
that we later use include $x\in{{}^{co}\mathbf{I}}$, $x\in\mathbf{R}$,
$d\in\mathbf{SD}$.

Further, $t\in\mathbf{T}$ for some term $t:\tau$ means that $t$ is “total” in
the obvious way for types $\tau$ of $lev(\tau)\leq 1$, e.g. for a sequence of
natural numbers $ns:\mathbb{N}\to\mathbb{N}$ we have
$ns\in\mathbf{T}:=\forall_{n\in\mathbf{T}}(ns\ n)\in\mathbf{T}$ where
$n\in\mathbf{T}$ is the inductive predicate given by the clauses
$0\in\mathbf{T}$ and $n\in\mathbf{T}\to(n+1)\in\mathbf{T}$. The elimination
rule of $n\in\mathbf{T}$ is induction over natural numbers. We assume that
$\leq$ on natural numbers or (positive) integers is defined for total objects
only. In particular, if we write something like $\forall_{n\geq M(p)}A(n)$, we
implicitly assume $n\in\mathbf{T}$.

###  2.2 Program extraction from proofs

We give a sketch of the concept of program extraction from proofs, which we
use in this paper to get verified algorithms for exact real number
computation. For a detailed description we refer to [Wie17, SW12, Sch21a,
K1̈8].

The starting point of formal program extraction is a constructive proof of a
theorem $A$ in TCF. The proof must be available as a formal proof term $M$.

In a first step from the formula we define its type $\tau(A)$ and realizer
predicate $A^{\mathbf{r}}$. Both are defined by recursion on the structure of
the formula. The realiser predicate is a predicate which takes a term of the
type of the formula and states that a term is a realizer of the formula, i.e.
it adheres to the computational requirements stated in the formula. Important
for the computational interpretation of a formula are the inductively and
coinductively defined predicates. Note that the all- and exists-quantifier by
themselves will not carry computational content. But we will use the
abbreviations $\forall_{t\in A}$ and $\exists_{t\in A}$, where $t\in A$ is
computationally relevant (as long as $A$ is).

In a second step we compute the extracted term $\operatorname{et}(M)$ of the
formalized proof. The extracted term is a $\lambda$-term with the type of the
formula and is defined by recursion over proofs. It represents the extracted
algorithm from the formal proof. In our case we will state this term after
each proof which was formalized in Minlog, translated to the notation of
Haskell.

In the last step of program extraction we generate a proof that the extracted
term is indeed a realizer of the realizer predicate, i.e.
$A^{\mathbf{r}}\operatorname{et}(M)$. This is the so-called soundness proof.

In a nutshell, the result of formal program extraction is an algorithm in the
form of a $\lambda$-term and the proof of its correctness. However, as it is
hardly possible to describe a formal proof on paper, we use the proof
assistant Minlog. In Minlog the last three steps above can be done
automatically, so the laborious part is to find the right formulation of the
theorem and the implementation of the constructive proof in Minlog. For the
right formulation, we use the predicate ${{}^{co}\mathbf{I}}$ which is given
in the next section.

###  2.3 Coinductive definition of the signed digit representation

[sd-code representation] We define ${{}^{co}\textbf{I}}$ as the greatest fixed
point of the operator

$\Phi(X):=\left\\{x\ \middle|\
\exists_{d\in\mathbf{SD},x^{\prime}}\left(Xx^{\prime}\wedge|x^{\prime}|\leq
1\wedge x=\frac{d+x^{\prime}}{2}\right)\right\\}.$

A realiser of ${{}^{co}\textbf{I}}x$ has the type

$\tau({{}^{co}\textbf{I}})=\mu_{\tau(X)}(\tau(\Phi(X))\rightarrow\tau(X))=\mu_{\xi}(\textbf{Sd}\rightarrow\xi\rightarrow\xi).$

Here we have identified $\tau(\textbf{Sd})=\mu_{\xi}(\xi,\xi,\xi)$ with Sd
itself. We define $\texttt{Str}:=\tau({{}^{co}\textbf{I}})$ and by
$\mathrm{C}$ we denote the only constructor of Str. In Haskell notation Str is
given by

      data Sd = SdR  | SdM  | SdL
      data Str = C Sd Str

In this notation we easily see that an element $\mathrm{C}dv$ is a
$\mathbf{Sd}$-stream with first digit $d$ and tail $v$. Sometimes we
abbreviate $\mathrm{C}dv$ by just writing $dv$. We will also use this notation
for reals: If we write something like $dx$ for a real number $x$ and a signed
digit $d$, we mean $\frac{d+x}{2}$.

The definition of ${{}^{co}\textbf{I}}$ as greatest fixpoint of $\Phi$ can be
expressed by the two axioms

$\displaystyle{{}^{co}\textbf{I}}^{-}:\ $
$\displaystyle{{}^{co}\textbf{I}}\subseteq\Phi({{}^{co}\textbf{I}})$
$\displaystyle{{}^{co}\textbf{I}}^{+}:\ $ $\displaystyle
X\subseteq\Phi({{}^{co}\textbf{I}}\cup X)\rightarrow
X\subseteq{{}^{co}\textbf{I}},$

where $X$ is an unary predicate variable on real numbers. It is called
_competitor predicate_. The first axiom ${{}^{co}\textbf{I}}^{-}$ says that
${{}^{co}\textbf{I}}$ is a fixpoint of $\Phi$. Expressed in elementary
formulas it is given by

$\forall_{x\in{{}^{co}\textbf{I}}}\exists_{d\in\mathbf{Sd},x^{\prime}}\left(x^{\prime}\in{{}^{co}\textbf{I}}\wedge|x^{\prime}|\leq
1\wedge x=\frac{d+x^{\prime}}{2}\right).$

The type of this axiom is
$\tau({{}^{co}\textbf{I}}^{-})=\texttt{Str}\rightarrow\textbf{Sd}\times\texttt{Str}$
and a realiser is the destructor $\mathcal{D}$ given by the computation rule

$\mathcal{D}(\mathrm{C}dv):=\langle d,v\rangle.$

The destructor takes a stream and returns a pair consisting of its first digit
and its tail. Using the projectors $\pi_{0}$ and $\pi_{1}$ one gets the first
digit and the tail, respectively. E.g. consider a formula of the form
$x\in{{}^{co}\mathbf{I}}\to A$ of type $\texttt{Str}\to\tau(A)$. Now assume
that in its proof, ${{}^{co}\mathbf{I}}^{-}$ is used with
$x\in{{}^{co}\mathbf{I}}$ at some point. On the computational level this
corresponds to reading the head of the input stream and storing its tail.

The second axiom ${{}^{co}\textbf{I}}^{+}$ expresses that
${{}^{co}\textbf{I}}$ is the greatest fixpoint in a strong sense. It is
explicitly given by:

$\forall_{x}\left(Xx\to\forall_{x}\left(Xx\to\exists_{d\in\mathbf{Sd},x^{\prime}}\left(x^{\prime}\in\left({{}^{co}\textbf{I}}\cup
X\right)\wedge|x^{\prime}|\leq 1\wedge
x=\dfrac{d+x^{\prime}}{2}\right)\right)\rightarrow
x\in{{}^{co}\textbf{I}}\right)$

The type depends on the type of the predicate variable $X$, namely

$\tau({{}^{co}\textbf{I}}^{+})=\tau(X)\rightarrow\left(\tau(X)\rightarrow\textbf{Sd}\times(\texttt{Str}+\tau(X))\right)\rightarrow\texttt{Str}$

A realiser of ${{}^{co}\textbf{I}}^{+}$ is the corecursion operator
${}^{co}\mathcal{R}$ which is given by the computation rule

${}^{co}\mathcal{R}tf:=\begin{cases}\mathrm{C}(\pi_{0}(ft))v&\text{if\
}\pi_{1}(ft)=\text{in}_{0}(v)\\\
\mathrm{C}(\pi_{0}(ft))^{co}\mathcal{R}t^{\prime}f&\text{if\
}\pi_{1}(ft)=\text{in}_{1}(t^{\prime}).\end{cases}$

Here $\text{in}_{0}$ and $\text{in}_{1}$ are the two constructors of the type
sum $\texttt{Str}+\tau(X)$. If $\pi_{1}(ft)$ has the form $\text{in}_{0}v$,
the corecursion stops and we have $\mathrm{C}(\pi_{0}(ft))v$ as signed digit
representation. If it has the form $\text{in}_{1}t^{\prime}$, the corecursion
continues with the new argument $t^{\prime}$. In both cases we have obtained
at least the first digit of the stream. By iterating the corecursion we can
generate each digit of the stream one by one. In Haskell we have

      strDestr :: (Str -> (Sd, Str))
      strDestr (C s u) = (s , u)

      strCoRec :: (alpha -> ((alpha -> (Sd, (Either Str alpha))) -> Str))
      strCoRec g h = (C (fst (h g))
                        (case (snd (h g)) of
    Ψ                      { Left u0 -> u0 ;
    ΨΨ                        Right g1 -> (strCoRec g1 h) })).

Moreover we sometimes use the following functions.

      hd :: (Str -> Sd)
      hd u = fst(strDestr u)

      tl :: (Str -> Str)
      tl u = snd(strDestr u)

      sdtoint :: Sd -> Integer
      sdtoint SdR = 1
      sdtoint SdM = 0
      sdtoint SdL = -1

      id :: Pos -> Nat
      id p = p

Here fst and snd are the pair-projections.

###  2.4 Basic lemmas

We prove two basic lemmas, which will often occur in the proofs following:

######  Lemma 1 (CoICompat).

The predicate ${{}^{co}\mathbf{I}}$ is compatible with real equality, i.e.

$\forall_{x\in{{}^{co}\mathbf{I}}}\forall_{y}\left(x=y\rightarrow
y\in{{}^{co}\textbf{I}}\;\right)$

######  Proof 2.1.

We apply (2.3) to the predicate $Px:=\exists_{y\in{{}^{co}\mathbf{I}}}(x=y)$:

$\forall_{x}\left(Px\rightarrow\forall_{x}\left(Px\rightarrow\exists_{d\in\mathbf{Sd},x^{\prime}}\left(x^{\prime}\in\left({{}^{co}\textbf{I}}\cup
P\right)\wedge|x^{\prime}|\leq 1\wedge
x=\dfrac{d+x^{\prime}}{2}\right)\right)\rightarrow
x\in{{}^{co}\textbf{I}}\right)$

It is sufficient to prove the second premise. So assume $x$ and
$y\in{{}^{co}\textbf{I}}$ with $x=y$ are given. Using
$y\in{{}^{co}\textbf{I}}$ with ${{}^{co}\mathbf{I}}^{-}$ we get
$e\in\textbf{Sd}$ and $y^{\prime}\in{{}^{co}\textbf{I}}$ with
$|y^{\prime}|\leq 1$ and $y=\frac{e+y^{\prime}}{2}$. Hence $d:=e$ and
$x^{\prime}:=y^{\prime}$ have the desired properties.

In the following proofs, this theorem is used tacitly. In Minlog it has the
name CoICompat. The extracted term of this theorem is given by

      cCoICompat :: (Str -> Str)
      cCoICompat u0 = strCoRec u0 (\ su1 -> (case su1 of
                                              {s2 u2 -> (s2,Left u2)}))

Assume f is the costep-function above, then for C s u some stream we have f(C
s u) = (s,Left u). So if we unfold the strCoRec we get

      cCoICompat (C s u) = C s u,

i.e. the computational content of this lemma is actually the identity. Hence
to increase readability, we will leave it out in the following.

######  Lemma 2 (CoIClosureInv).

$\forall_{x\in{{}^{co}\mathbf{I}},d\in\mathbf{Sd}}\frac{d+x}{2}\in{{}^{co}\mathbf{I}}$

######  Proof 2.2.

We use (2.3) with the predicate

$Px:=\exists_{d\in\mathbf{Sd},x^{\prime}\in{{}^{co}\textbf{I}}}x=\frac{d+x^{\prime}}{2},$

Again, in order to prove the goal formula, it is sufficient to prove the
second premise. Therefore our goal is

$\forall_{x}\left(\exists_{d\in\mathbf{Sd},x^{\prime}\in{{}^{co}\mathbf{I}}}\left(x=\frac{d+x^{\prime}}{2}\right)\rightarrow\exists_{d\in\mathbf{Sd},x^{\prime}}\left(x^{\prime}\in\left({{}^{co}\mathbf{I}}\cup
P\right)\wedge|x^{\prime}|\leq 1\wedge
x=\dfrac{d+x^{\prime}}{2}\right)\right).$

But this follows immediately from
${{}^{co}\mathbf{I}}\subseteq{{}^{co}\textbf{I}}\cup P$ and
$x\in{{}^{co}\mathbf{I}}\to|x^{\prime}|\leq 1$.

In Minlog this lemma has the name CoIClosureInv and its extracted term is
given by

      cCoIClosureInv :: (Sd -> (Str -> Str))
      cCoIClosureInv s0 u1 = strCoRec (s0 , u1)
                                      (\ su2 -> (
                                        (case su2 of
                                        { (,) s u -> s }) ,
                                        (Left (case su2 of
                                          { (,) s0 u0 -> u0 })))),

which is an elaborate way to write the constructor $\mathrm{C}$, namely if f
is the costep-function above then f (s0,u1) = (s0,Left u1) and by unfolding
strCoRec

      cCoIClosureInv s0 u1 = C s0 u1.

###  2.5 Cauchy reals and signed digit streams

We now formalize the relation between reals represented by Cauchy-sequences of
rationals and signed digit streams. [Cauchy representation] We denote
$as:\mathbb{N}\to\mathbb{Q}$ and $M:\mathbb{Z}^{+}\to\mathbb{N}$ and define

$\mathbf{Mon}(M):=M\in\mathbf{T}\wedge\forall_{p\leq q}\left(Mp\leq
Mq\right).$

For a real $x$ we write $x\in\mathbf{R}$, if there exist $M\in\mathbf{Mon}$
and $as\in\mathbf{T}$ with

$\forall_{p\in\textbf{T}}\forall_{n\geq M(p)}\left(|x-(as\
n)|<2^{-(p+1)}\right),$

i.e. there is a sequence of rationals converging to $x$. In Haskell this
representation is given by the datatype

      data Rea = RealConstr (Nat -> Rational) (Pos -> Nat),

with the pair-projections

      realSeq :: (Rea -> (Nat -> Rational))
      realSeq (RealConstr as m) = as
    Ψ
      realMod :: (Rea -> (Pos -> Nat))
      realMod (RealConstr as m) = m.

In the following we will prove that for some $x\in{{}^{co}\mathbf{I}}$ and
$n\in\mathbf{T}$ there exists a rational approximation to $x$ with precision
$\frac{1}{2^{n}}$. To get a sequence of rationals representing $x$ we need
dependent choice. Moreover later we will use countable choice. [Choice
Principles] We denote $f:\mathbb{N}\to\alpha$, then the axiom of dependent
choice $\mathbf{DC}$ is given by

$\exists_{\alpha}P(0,\alpha)\to\forall_{n\in\mathbf{T},\alpha}\left(P(n,\alpha)\to\exists_{\alpha}P(n+1,\alpha)\right)\to\exists_{f}\forall_{n\in\mathbf{T}}P(n,fn).$

It has the type

$\tau(P)\to\left(\mathbb{N}\to\tau(P)\to\tau(P)\right)\to\mathbb{N}\to\tau(P)$

and the realizer is given by the recursion operator for $\mathbb{N}$, i.e.

    Ψ  natRec :: Nat -> a -> (Nat -> a -> a) -> a
    Ψ  natRec 0 g h = g
    Ψ  natRec n g h | n > 0 = h (n - 1) (natRec (n - 1) g h).
    Ψ

The axiom of countable choice CC is given by

$\forall_{n\in\mathbf{T}}\exists_{\alpha\in\mathbf{T}}P(n,\alpha)\to\exists_{f\in\mathbf{T}}\forall_{n\in\mathbf{T}}P(n,fn)$

Its type is
$(\mathbb{N}\to\alpha\times\tau(P))\to(\mathbb{N}\to\alpha)\times(\mathbb{N}\to\tau(P))$
and the realizer is basically given by the identity, namely

$\lambda_{F}\langle\lambda_{n}(F\,n)_{0},\lambda_{n}(F\,n)_{1}\rangle.$

######  Theorem 3 (StrToCs).

Any real $x$ represented by a signed digit code can be represented by a
Cauchy-sequence, i.e.

$\forall_{x\in{{}^{co}\mathbf{I}}}(x\in\mathbf{R}\wedge|x|\leq 1).$

######  Proof 2.3.

Assume $x\in{{}^{co}\mathbf{I}}$, then $|x|\leq 1$ holds by
${{}^{co}\mathbf{I}}^{-}$. Now let

$P(n,a):=a\in\mathbf{T}\wedge\exists_{y\in{{}^{co}\mathbf{I}}}\left(x=2^{-(n+1)}y+a\right)$

We want to apply $\mathbf{DC}$, hence we first prove $\exists_{a}P(0,a)$. By
${{}^{co}\mathbf{I}}^{-}$ there is $y\in{{}^{co}\mathbf{I}},d\in\mathbf{Sd}$
with $x=\frac{y+d}{2}$, so let $a:=\frac{d}{2}$. For the second premise of
$\mathbf{DC}$ assume $n\in\mathbf{T},a\in\mathbf{T}$ and $P(n,a)$ i.e. there
exists $y\in{{}^{co}\mathbf{I}}$ with $x=\frac{1}{2^{n+1}}y+a$. We need to
prove

$\exists_{b}\left(b\in\mathbf{T}\wedge\exists_{z\in{{}^{co}\mathbf{I}}}\left(x=2^{-(n+2)}z+b\right)\right)$

Since $y\in{{}^{co}\mathbf{I}}$ we get
$d\in\mathbf{Sd},y^{\prime}\in{{}^{co}\mathbf{I}}$ with
$y=\frac{y^{\prime}+d}{2}$. Now we choose $b:=a+\frac{d}{2^{n+2}}$ and
$z=y^{\prime}$, then

$x=\frac{1}{2^{n+1}}y+a=\frac{1}{2^{n+2}}y^{\prime}+b$

Hence by $\mathbf{DC}$ there exists $as\in\mathbf{T}$ with

$\forall_{n\in\mathbf{T}}\exists_{y\in{{}^{co}\mathbf{I}}}\left(x=2^{-(n+1)}y+(as\
n)\right).$

Hence with $Mp:=p$ and $|y|\leq 1$ we get $x\in\mathbf{R}$.

The extracted term of the proof is given by

      cStrToCsInit :: (Str -> (Rational, Str))
      cStrToCsInit u0 = (sdtoint(hd u0) % 2 , tl u0)
    Ψ
      cStrToCsStep :: (Nat -> ((Rational, Str) -> (Rational, Str)))
      cStrToCsStep n0 (a,u0)= (a + sdtoint(hd u0) % (((2 ^ n0) * 2) * 2) ,
                               tl u0)

      cStrToCs :: (Str -> Rea)
      cStrToCs u0 = (\ n1 -> (fst (natRec n1 (cStrToCsInit u0) cStrToCsStep)) ,
                     id).

Here cStrToCsInit corresponds to the first premise and cStrToCsStep to the
second premise of $\mathbf{DC}$ in the proof. $\mathbf{DC}$ itself only
appears as the natRec term in cStrToCs. Informally we can represent the
computational content by

$d_{0}d_{1}d_{2}\dots\mapsto\left(\left(\sum_{i=1}^{n}d_{i}2^{-i}\right)_{n},\iota\right),$

where $\iota:\mathbb{Z}^{+}\to\mathbb{N}$ is the canonical inclusion.

For the converse of Theorem 3 we first prove the following two lemmas.

######  Lemma 4 (Special case of ApproxSplit).

Let $a,b:\mathbb{Q}$ then

$\forall_{a,b\in\mathbf{T},x\in\mathbf{R}}\left(a<b\to a\leq x\vee x\leq
b\right).$

######  Proof 2.4.

Given $(as,M)$ a Cauchy-sequence converging to $x$. Find $p$ be such that
$\frac{1}{2^{p}}<b-a$ (which is possible since $a,b\in\mathbf{T}$). Then for
$n\geq M\ p$

$|x-(as\ n)|\leq 2^{-(p+1)},$

i.e. $x\in\left[(as\ n)-\frac{1}{2^{p+1}},(as\ n)+\frac{1}{2^{p+1}}\right]$.
Case $(as\ n)\leq\frac{a+b}{2}$. In that case $x\leq(as\
n)+\frac{1}{2^{p+1}}<b$. Otherwise $a\leq x$.

Note that it can be proven more generally for $y,z\in\mathbf{R}$ and $y<z$
instead of $a,b$, but we will actually only need it for for the special cases
$0<\frac{1}{2}$ and $-\frac{1}{2}<0$. The extracted term for the former case
is:

       cApproxSplitZeroPtFive :: (Rea -> Bool)
       cApproxSplitZeropPtFive (RealConstr as m) = (as (m 3)) <= (1/4)

where cRatLeAbsBound is the extracted term of a proof of
$\forall_{a\in\mathbf{T}}\exists_{n\in\mathbf{T}}|a|\leq 2^{n}$.
For the converse of Theorem 3 we first prove the following lemma.

######  Lemma 5 (CsToStrAux).

For all $x\in\mathbf{R}$ with $|x|\leq 1$

$\exists_{d\in\mathbf{SD},y\in\mathbf{R}}\left(|y|\leq 1\wedge
x=\frac{y+d}{2}\right).$

######  Proof 2.5.

Let $(as,M)$ a Cauchy-sequence converging to $x$. We use Theorem 4 with
$0<\frac{1}{2}$ respectively $-\frac{1}{2}<0$. We define

$d:=\begin{cases}\overline{1}&\text{if\quad}x<-\frac{1}{2},\\\
0&\text{if\quad}-\frac{1}{2}<x<\frac{1}{2},\\\
1&\text{if\quad}\frac{1}{2}<x,\end{cases}$

$bs\ n:=2(as\ n)-d$, $Np:=M(p+1)$ and $y=2x-d$. Then $(bs,N)$ is a Cauchy-
sequence converging to $y$. Furthermore $x=\frac{1}{2}(y+d)$ and $|y|\leq 1$
by definition.

The extracted term is given by

      cCsToStrAux :: (Rea -> (Sd, Rea))
      cCsToStrAux (RealConstr as m) =
        (if ((as (m 3)<=-1/4) then
            (SdL , (RealConstr (\ n3 -> (((2) * (as n3)) + (1)))
                               (\ p3 -> (m (p3 + 1)))))
         else
           (if ((as (m 3)<=1/4) then
              (SdM , (RealConstr (\ n3 -> ((2) * (as n3)))
                                 (\ p3 -> (m (p3 + 1)))))
            else
              (SdR , (RealConstr (\ n3 -> (((2) * (as n3)) + (-1)))
                                 (\ p3 -> (m (p3 + 1))))))))).

Again we can represent the computational content informally, namely

$(as,M)\mapsto(\mathtt{g}(as,M),(\mathtt{h}(as,M),N)),$

where $N\ p:=M(p+1)$ and $\mathtt{g},\mathtt{h}$ are the functions

$\displaystyle\mathtt{g}(as,M)$
$\displaystyle:=\begin{cases}\bar{1}&\text{if\quad}as(M\
3)\leq-\frac{1}{4},\\\ 0&\text{if\quad}|as(M\ 3)|\leq\frac{1}{4},\\\
1&\text{otherwise}.\end{cases}$ $\displaystyle\mathtt{h}(as,M)$
$\displaystyle:=2as-g(as,M)$

Using this lemma the proof of the translation from Cauchy-sequences to stream
is very short:

######  Theorem 6 (CsToStr).

$\forall_{x}\left(x\in\mathbf{R}\to|x|\leq 1\rightarrow
x\in{{}^{co}\mathbf{I}}\right)$

######  Proof 2.6.

Assume $x\in\mathbf{R}$ and $|x|\leq 1$. We use (2.3) with

$Px:=\exists_{d\in\mathbf{Sd},y\in\mathbf{R}}\left(|y|\leq 1\wedge
x=\frac{y+d}{2}\right).$

By the previous lemma it suffices to prove the second premise, namely

$\forall_{x}\left(Px\to\exists_{d\in\mathbf{Sd},x^{\prime}}\left(x^{\prime}\in\left({{}^{co}\textbf{I}}\cup
P\right)\wedge|x^{\prime}|\leq 1\wedge
x=\dfrac{d+x^{\prime}}{2}\right)\right).$

But this follows immediately by another application of the lemma, namely let
$d\in\mathbf{Sd},y\in\mathbf{R}$ with $|y|\leq 1$ and $x=\frac{y+d}{2}$. Then
by the lemma there are $e\in\mathbf{Sd},z\in\mathbf{R}$ with $|z|\leq 1$ and
$y=\frac{z+e}{2}$ and hence $y\in P\subseteq{{}^{co}\mathbf{I}}\cup P$.

The extracted term is

      cCsToStr :: (Rea -> Str)
      cCsToStr x0 = strCoRec
                     (cCsToStrAux x0)
                     (\ sx1 -> (case sx1 of { (,) s0 x0 ->
                     Ψ          (case (cStrToCsAux x0) of { (,) s1 x1 ->
                     Ψ          Ψ(s0 , (Right (s1 , x1))) }) })),

and informally

$x\mapsto\pi_{0}(\texttt{cCsToStrAux}\
x)::\texttt{cCsToStr}(\pi_{1}(\mathtt{cCsToStrAux}\ x)).$

##  3 Convergence theorem

The convergence theorem states that the signed digit representation, is closed
under limits. In this section we consider a direct proof of this theorem,
which only relies on the signed digit representation of real numbers, and an
indirect proof, which works with Cauchy reals and uses the translation between
the signed digit code and Cauchy reals. After proving the convergence theorem
in these two ways, we compare the extracted terms of both proofs.
[Convergence] Let $xs:\mathbb{N}\to\mathbb{R}$ and $M\in\mathbf{Mon}$ then
$xs$ is a Cauchy-sequence with modulus $M$ iff

$\forall_{p\in\mathbf{T}}\forall_{n,m\geq M(p)}|(xs\ n)-(xs\ m)|\leq 2^{-p},$

we also write $\mathbf{Cauchy}(xs,M)$. The sequence $xs$ converges to $x$ with
Modulus $M$ iff

$\forall_{p\in\mathbf{T}}\forall_{n\geq M(p)}|x-(xs\ n)|\leq 2^{-p},$

we write $\mathbf{Conv}(xs,x,M)$. The convergence theorem can now be stated in
the following way.

######  Theorem 7 (SdLim).

Let $xs:\mathbb{N}\rightarrow\mathbb{R}$ be a sequence of reals in
${{}^{co}\mathbf{I}}$ which converges to some real $x$ with modulus $M$. Then
$x\in{{}^{co}\mathbf{I}}$, i.e.

$\forall_{x,xs;M\in\mathbf{Mon}}\left(\forall_{n\in\mathbf{T}}(xs\
n)\in{{}^{co}\mathbf{I}}\to\mathbf{Conv}(xs,x,M)\to
x\in{{}^{co}\mathbf{I}}\right).$

###  3.1 Direct approach

This and the next lemma were already considered in [SW20, Wie17].

######  Lemma 8 (CoINegToCoIPlusOne, CoIPosToCoIMinusOne).

$\displaystyle\forall_{x\in{{}^{co}\mathbf{I}}}(x\leq
0\rightarrow{{}^{co}\textbf{I}}(x+1))$
$\displaystyle\forall_{x\in{{}^{co}\mathbf{I}}}(0\leq
x\rightarrow{{}^{co}\textbf{I}}(x-1))$

######  Proof 3.1.

Since the proofs are very similar, we only prove the first formula. We use
(2.3) with $Px:=\exists_{y\in{{}^{co}\mathbf{I}}}\left(y\leq 0\wedge
y+1=x\right)$. We need to prove the second premise, namely

$\forall_{x}\left(Px\rightarrow\exists_{d\in\mathbf{Sd},x^{\prime}}\left(x^{\prime}\in\left({{}^{co}\textbf{I}}\cup
P\right)\wedge|x^{\prime}|\leq 1\wedge
x=\dfrac{d+x^{\prime}}{2}\right)\right)$

Let $x\in P$, $y\in{{}^{co}\textbf{I}}$ with $y\leq 0$ and $y+1=x$ be given.
Our goal is

$\exists_{d\in\mathbf{Sd},x^{\prime}}\left(x^{\prime}\in\left({{}^{co}\textbf{I}}\cup
P\right)\wedge|x^{\prime}|\leq 1\wedge x=\dfrac{d+x^{\prime}}{2}\right).$

From $y\in{{}^{co}\textbf{I}}$ we get $e$ and $y^{\prime}$ with
$e\in\textbf{Sd}$, $y^{\prime}\in{{}^{co}\mathbf{I}}$, $|y^{\prime}|\leq 1$
and $y=\frac{e+y^{\prime}}{2}$. We make a case distinction on $\textbf{Sd}\
e$:
If $e=-1$, we define $d:=1\in\mathbf{Sd}$ and $x^{\prime}:=y^{\prime}$. Then
$|x^{\prime}|\leq 1$ and $x^{\prime}\in{{}^{co}\mathbf{I}}$ by definition.
Furthermore we have

$x=y+1=\frac{-1+y^{\prime}}{2}+1=\frac{1+y^{\prime}}{2}=\frac{d+x^{\prime}}{2}.$

If $e=0$, we define $d:=1$ and $x^{\prime}:=y^{\prime}+1$. In this case we
prove $Px^{\prime}$, namely we show $y^{\prime}\in{{}^{co}\mathbf{I}}$,
$y^{\prime}\leq 0$ and $x^{\prime}=y^{\prime}+1$. We only need to prove
$y^{\prime}\leq 0$ which follows directly from $y\leq 0$ and
$y=\frac{0+y^{\prime}}{2}$.
The last case is $e=1$. Because of $y\leq 0$, $y=\frac{-1+y^{\prime}}{2}$ and
$|y^{\prime}|\leq 1$, this is only possible if $y$ is equal to $0$, and
therefore $x=1$. Hence we define $d:=1$ and $x^{\prime}:=1$. Then
$x=\frac{d+x^{\prime}}{2}$ and $x^{\prime}=1\in{{}^{co}\mathbf{I}}$ is easily
proven by coinduction. (For details we refer to the Minlog implementation of
the theorem CoIOne in examples/analysis/sddiv.scm.)

A realizer of the first formula is a function f, which takes a signed digit
stream of a real number $x$ and returns a signed digit stream of $x+1$ if
$x\leq 0$. The extracted term of the proof of the first statement translated
to Haskell is

      cCoINegToCoIPlusOne :: (Str -> Str)
      cCoINegToCoIPlusOne u0 = aiCoRec u0
                                 (\ u1 -> (case (hd u1) of
    ΨΨ                                { SdR -> (SdR , (Left cCoIOne)) ;
    ΨΨΨ                                  SdM -> (SdR , (Right (tl u1))) ;
    ΨΨΨ                                  SdL -> (SdR , (Left (tl u1))) })),

where

      cCoIOne :: Str
      cCoIOne = (aiCoRec () (\ g -> (SdR , (Right ()))))

is the stream representing $1$. Unfolding strCoRec once yields cCoIOne = C SdR
cCCoIOne, i.e. it is a constant stream of SdR.

Another way to characterise this function f is to give its computation rules:

$\displaystyle\texttt{f}(\mathrm{C}\overline{1}v)$
$\displaystyle:=\mathrm{C}1v$ $\displaystyle\texttt{f}(\mathrm{C}0v)$
$\displaystyle:=\mathrm{C}1(\texttt{f}v)$
$\displaystyle\texttt{f}(\mathrm{C}1v)$ $\displaystyle:=[1,1,\dots]$

Analogously as extracted term of the second statement of this lemma, we get a
function $\texttt{g}:\texttt{Str}\rightarrow\texttt{Str}$ which is
characterised by the rules

$\displaystyle\texttt{g}(\mathrm{C}\overline{1}v)$
$\displaystyle:=[\overline{1},\overline{1},\dots]$
$\displaystyle\texttt{g}(\mathrm{C}0v)$
$\displaystyle:=\mathrm{C}\overline{1}(\texttt{g}v)$
$\displaystyle\texttt{g}(\mathrm{C}1v)$
$\displaystyle:=\mathrm{C}\overline{1}v.$

It takes a signed digit stream of a real $x$ and returns a signed digit stream
of $x-1$ if $0\leq x$.
Using this lemma, we are now able to prove the following lemma:

######  Lemma 9 (CoIToCoIDouble).

$\displaystyle\forall_{x\in{{}^{co}\mathbf{I}}}\left(|x|\leq\frac{1}{2}\rightarrow
2x\in{{}^{co}\mathbf{I}}\right)$

######  Proof 3.2.

We apply ${{}^{co}\mathbf{I}}^{-}$ and get $d\in\mathbf{Sd}$,
$x^{\prime}\in{{}^{co}\mathbf{I}}$ with $|x^{\prime}|\leq 1$ and
$x=\frac{d+x^{\prime}}{2}$. We distinguish cases on $d\in\mathbf{Sd}$:
$d=1$: Then $2x-1=x^{\prime}$ and $|x|\leq\frac{1}{2}$ which imply
$x^{\prime}\leq 0$. By the first part of Lemma 8
$1+x^{\prime}=2x\in{{}^{co}\mathbf{I}}$.
$d=-1$: As the first case but with the second part of Lemma 8.
$d=0$: In this case $2x=x^{\prime}$ and $x^{\prime}\in{{}^{co}\mathbf{I}}$ by
assumption.

In Haskell notation the extracted term is given by

      cCoIToCoIDouble :: (Str -> Str)
      cCoIToCoIDouble u0 = case (hd u0) of
          { SdR -> (cCoINegToCoIPlusOne (tl u0)) ;
            SdM -> (tl u0) ;
            SdL -> (cCoIPosToCoIMinusOne (tl u0)) }
    Ψ

Again we give a more readable characterisation of the extracted term D by the
computation rules

$\displaystyle\texttt{D}(\mathrm{C}\overline{1}u)$
$\displaystyle:=\texttt{g}u$ $\displaystyle\texttt{D}(\mathrm{C}0u)$
$\displaystyle:=u$ $\displaystyle\texttt{D}(\mathrm{C}1u)$
$\displaystyle:=\texttt{f}u,$

where f, g are the computational content of the previous lemma. The following
lemma is a special case of

$\forall_{x\in{{}^{co}\mathbf{I}},y\in{{}^{co}\mathbf{I}}}\frac{x+y}{2}\in{{}^{co}\mathbf{I}}.$

This theorem is implemented as the theorem Average in
examples/analysis/average.scm of Minlog and was considered in [BS12, MS15].
But here we give a direct proof of a special case because it is instructive
and elementary.

######  Lemma 10 (Special case of CoIAverage).

$\displaystyle\forall_{x\in{{}^{co}\mathbf{I}}}\left(\frac{x}{2}\pm\frac{1}{4}\right)\in{{}^{co}\mathbf{I}}$

######  Proof 3.3.

Applying ${{}^{co}\mathbf{I}}^{-}$ yields $x^{\prime}\in{{}^{co}\mathbf{I}}$
and $d\in\textbf{Sd}$ with $x=\frac{d+x^{\prime}}{2}$. We show only
${{}^{co}\textbf{I}}\left(\frac{x}{2}+\frac{1}{4}\right)$, the other case is
proven analogously. We distinguish cases on $d\in\mathbf{Sd}$:
$d=1$: Then
$\frac{x}{2}+\frac{1}{4}=\frac{2+x^{\prime}}{4}=\frac{1}{2}(1+\frac{x^{\prime}}{2})$.
$d=0$: Then
$\frac{x}{2}+\frac{1}{4}=\frac{1+x^{\prime}}{4}=\frac{1}{2}\frac{1+x^{\prime}}{2}$.
$d=-1$: Then
$\frac{x}{2}+\frac{1}{4}=\frac{x^{\prime}}{4}=\frac{1}{2}\frac{x^{\prime}}{2}$.
In each case we apply Lemma 2 twice to get
$\left(\frac{x}{2}+\frac{1}{4}\right)\in{{}^{co}\mathbf{I}}$

We denote the extracted term of the proven statement by $q^{+}$. From the
proof and the fact that the extracted term of Lemma 2 is given by
$\mathrm{C}$, one easily sees that $q^{+}$ has the following computation
rules:

$\displaystyle q^{+}(\overline{1}u)$ $\displaystyle:=00u$ $\displaystyle
q^{+}(0u)$ $\displaystyle:=01u$ $\displaystyle q^{+}(1u)$ $\displaystyle:=10u$

Analogously, the extracted term $q^{-}$ of the statement
$\forall_{x}.{{}^{co}\textbf{I}}x\rightarrow{{}^{co}\textbf{I}}\left(\frac{x}{2}-\frac{1}{4}\right)$
is characterised by

$\displaystyle q^{-}(\overline{1}u)$ $\displaystyle:=\overline{1}0u$
$\displaystyle q^{-}(0u)$ $\displaystyle:=0\overline{1}u$ $\displaystyle
q^{-}(1u)$ $\displaystyle:=00u.$

In the direct proof of sdlim below we will make use of the following case-
distinction. To shorten the extracted term we outsource this case-distinction
into a separate lemma.

######  Lemma 11 (TripleCases).

For $x\in{{}^{co}\mathbf{I}}$

$x\in\left[\dfrac{1}{8},1\right]\vee x\in\left[-1,-\frac{1}{8}\right]\vee
x\in\left[-\frac{1}{4},\frac{1}{4}\right]$

######  Proof 3.4.

Triple application of ${{}^{co}\textbf{I}}^{-}$ to $x\in{{}^{co}\mathbf{I}}$
gives $d_{1},d_{2},d_{3}\in\textbf{Sd}$ and $y^{\prime}\in{{}^{co}\textbf{I}}$
such that $x=\frac{4d_{1}+2d_{2}+d_{3}+y^{\prime}}{8}$. The claim follows by
case-distinction on $d_{1},d_{2}$ and $d_{3}$. Namely writing
$x=d_{1}d_{2}d_{3}y^{\prime}$ we have

$\begin{drcases}11d_{3}y^{\prime}\\\ 10d_{3}y^{\prime}\\\
1\overline{1}1y^{\prime}\\\ 1\overline{1}0y^{\prime}\\\ 011y^{\prime}\\\
010y^{\prime}\end{drcases}\to\frac{1}{8}\leq
x\qquad\begin{drcases}\overline{11}d_{3}y^{\prime}\\\
\overline{1}0d_{3}y^{\prime}\\\ \overline{1}1\overline{1}y^{\prime}\\\
\overline{1}10y^{\prime}\\\ 0\overline{11}y^{\prime}\\\
0\overline{1}0y^{\prime}\end{drcases}\to
x\leq-\frac{1}{8}\qquad\begin{drcases}00d_{3}y^{\prime}\\\
\overline{1}11y^{\prime}\\\ 1\overline{11}y^{\prime}\\\
01\overline{1}y^{\prime}\\\
0\overline{1}1y^{\prime}\end{drcases}\to-\frac{1}{4}\leq x\leq\frac{1}{4}.$

We omit the extracted term in Haskell here since it is quite long and
unreadable due to the $17$ case-distinctions. The computational content is
basically the diagram in the proof above.

With these preparations we are now able to give the direct proof of Theorem 7.

######  Proof 3.5 (Proof.( $\mathtt{SdLim}$, direct)).

We show that

$\displaystyle\forall_{x}\left(\exists_{xs;M\in\textbf{Mon}}\left(\forall_{n\in\mathbf{T}}(xs\
n)\in{{}^{co}\mathbf{I}}\wedge\forall_{p\in\mathbf{T}}\forall_{n\geq
Mp}|x-(xs\ n)|\leq 2^{-p}\right)\rightarrow{{}^{co}\textbf{I}}x\right),$

which is equivalent. We use (2.3) with $P$ the premise of the formula above:

$Px:=\exists_{xs;M\in\textbf{Mon}}\left(\forall_{n\in\mathbf{T}}(xs\
n)\in{{}^{co}\mathbf{I}}\wedge\forall_{n\geq M(p)}|x-(xs\ n)|\leq
2^{-p}\right)$

Again, we need to prove the second premise, namely

$\forall_{x}\left(Px\to\exists_{d\in\mathbf{Sd},x^{\prime}}\left(x^{\prime}\in\left({{}^{co}\textbf{I}}\cup
P\right)\wedge|x^{\prime}|\leq 1\wedge
x=\dfrac{d+x^{\prime}}{2}\right)\right)$

So let $x$, $xs$ and $M\in\mathbf{Mon}$ be given and assume
$\forall_{n\in\textbf{T}}(xs\ n)\in{{}^{co}\mathbf{I}}$ and
$\forall_{p\in\mathbf{T}}\forall_{n\geq M(p)}|(xs\ n)-x|\leq 2^{-p}$. We use
the lemma above with $(xs(M4))\in{{}^{co}\mathbf{I}}$ and get three cases:

(i) $\frac{1}{8}\leq xs(M(4))$. In this case we choose

$d:=1\ \text{and}\ x^{\prime}:=2x-1.$

Then $|x^{\prime}|\leq 1$ and $x=\frac{d+x^{\prime}}{2}$ follow directly. We
show that $Px^{\prime}$, so we define

$ys\ n:=2(xs((M(4))\sqcup n))-1,$

where $m\sqcup l:=\max\\{m,l\\}$ and $N(p):=M(p+1)\in\mathbf{Mon}$. The
statement $\forall_{n\geq Np}|ys(n)-x^{\prime}|\leq 2^{-p}$ is a direct
consequence of $\forall_{n\geq M(p)}|xs(n)-x|\leq 2^{-p}$ and it remains to
show $\forall_{n\in\mathbf{T}}(ys\ n)\in{{}^{co}\mathbf{I}}$. We calculate

$ys\ n=4\left(\frac{xs(M(4)\sqcup n)}{2}-\frac{1}{4}\right),$

and conclude $\frac{1}{4}(ys\ n)\in{{}^{co}\mathbf{I}}$ by Lemma 10.
Furthermore, we have $xs(M(4))\geq\frac{1}{8}$ and $\forall_{n\geq
M(4)}|xs(n)-x|\leq\frac{1}{16}$ and therefore

$\displaystyle xs(M(4)\sqcup n)$ $\displaystyle=(xs(M(4)\sqcup
n)-x)+(x-xs(M(4)))+xs(M(4))$
$\displaystyle\geq-\frac{1}{16}-\frac{1}{16}+\frac{1}{8}=0.$

Hence $0\leq xs(M(4)\sqcup n)\leq 1$, which implies $\left|\frac{xs(M(4)\sqcup
n)}{2}-\frac{1}{4}\right|\leq\frac{1}{4}$ and by double application of Lemma 9
we finally get $ys\ n\in{{}^{co}\textbf{I}}$.

(ii) $xs(M(4))\leq-\frac{1}{8}$. In this case we define

$d:=-1,\quad x^{\prime}:=2x+1,\quad ys\ n:=(2xs(M(4)\sqcup n)+1),\quad
Np:=M(p+1).$

The proof in this case is analogous to the proof of the first case.

(iii) $-\frac{1}{4}\leq f(M(4))\leq\frac{1}{4}$. We define

$d:=0\quad\text{and}\quad x^{\prime}:=2x.$

Again we show $Px^{\prime}$, namely

$\exists_{ys;N\in\textbf{Mon}}\left(\forall_{n\in\mathbf{T}}(ys\
n)\in{{}^{co}\mathbf{I}}\wedge\forall_{n\geq Np}|x^{\prime}-(ys\ n)|\leq
2^{-p}\right).$

To this end we define

$ys\ n:=2xs(M(4)\sqcup n)\quad\text{and}\quad Np:=M(p+1).$

Again, the right side of the conjunction follows from the assumptions. For the
left side consider

$|2(ys\ n)|=|xs(M(4)\sqcup n)|\leq|xs(M(4)\sqcup
n)-x|+|x-xs(M(4))|+|xs(M(4))|\leq\frac{1}{2},$

which implies $(ys\ n)\in{{}^{co}\mathbf{I}}$ by Lemma 9.

The extracted term is

      coilim :: (((Pos -> Nat), (Nat -> Str)) -> Str)
      coilim (m,us0) = aiCoRec (m,us0)
        (\ mus1 -> (case mus1 of
          { (,) m us -> (case (cTripleCases (us (m 4))) of
            { Left() -> (cSdLimCaseR m us) ;
            Ψ Right(Left ()) ->Ψ(cSdLimCaseL m us) ;
            Ψ Right(Right()) -> (cSdLimCaseM m us)}}.
     Ψ

The terms cSdLimCaseR,cSdLimCaseL and cSdLimCaseM are given by

      cSdLimCaseR :: ((Pos -> Nat) -> ((Nat -> Str) ->
                       (Sd, (Either Str ((Pos -> Nat), (Nat -> Str))))))
      cSdLimCaseR m0 us1 = (SdR ,
        (Right ((\ p2 -> (m0 (p2 + 1))) ,
                (\ n2 -> (cCoIToCoIDoublePlusOne (us1 ((m0 3) + n2)))))))
    Ψ
      cSdLimCaseM :: ((Pos -> Nat) -> ((Nat -> Str) ->
                       (Sd, (Either Str ((Pos -> Nat), (Nat -> Str))))))
      cSdLimCaseM m0 us1 = (SdM ,
        (Right ((\ p2 -> (m0 (p2 + 1))) ,
                (\ n2 -> (cCoIToCoIDouble (us1 ((m0 3) + n2)))))))
    Ψ
      cSdLimCaseL :: ((Pos -> Nat) -> ((Nat -> Str) ->
                       (Sd, (Either Str ((Pos -> Nat), (Nat -> Ai))))))
      cSdLimCaseL m0 us1 = (SdL ,
        (Right ((\ p2 -> (m0 (p2 + 1))) ,
                (\ n2 -> (cCoIToCoIDoubleMinusOne (us1 ((m0 3) + n2)))))))

In the following we will discuss the computational content, we will denote it
by Lim, in more detail. It has the type

$\displaystyle\texttt{Lim}:(\mathbb{Z}^{+}\rightarrow\mathbb{N})\rightarrow(\mathbb{N}\rightarrow\texttt{Str})\rightarrow\texttt{Str}.$

It takes as inputs the modulus of convergence and the sequence of streams and
returns the stream representing the limit. In order to give a more readable
characterisation of Lim, we define the following sets

R $\displaystyle:=\\{11v,10v,1\overline{1}1v,1\overline{1}0v,011v,010v\mid
v:\texttt{Str}\\}$ M
$\displaystyle:=\\{00v,\overline{1}11v,1\overline{11}v,01\overline{1}v,0\overline{1}1v\mid
v:\texttt{Str}\\}$ L
$\displaystyle:=\\{\overline{11}v,\overline{1}0v,\overline{1}1\overline{1}v,\overline{1}10v,0\overline{11}v,0\overline{1}0v\mid
v:\texttt{Str}\\}.$

which correspond to the intervals from Lemma 11. According to the proof we
then have the following rule for Lim:

$\displaystyle\texttt{Lim}\ M\ F:=\begin{cases}\mathrm{C}\ 1\ (\texttt{Lim}\
\lambda_{p}M(p+1)\ \lambda_{n}(\texttt{DD}q^{-}F(M(4)\sqcup n)))&\text{if
}F(M(4))\in\textbf{R}\\\ \mathrm{C}\ 0\ (\texttt{Lim}\ \lambda_{p}M(p+1)\
\lambda_{n}(\texttt{D}F(M(4)\sqcup n)))&\text{if }F(M(4))\in\textbf{M}\\\
\mathrm{C}\ \overline{1}\ (\texttt{Lim}\ \lambda_{p}M(p+1)\
\lambda_{n}(\texttt{DD}q^{+}F(M(4)\sqcup n)))&\text{if
}F(M(4))\in\textbf{L}\end{cases}$

The functions D, $q^{+}$ and $q^{-}$ are the computational content of the
lemmas above. Note that the definition of the new sequence is not unique. For
reasons of efficiency one should be flexible with the choice of the new
sequence, which is called $ys$ in the proof above. For example by choosing
$ys$ one can replace $M(4)\sqcup n$ by $M(4)+n$. The efficiency depends on the
concrete sequence. In the Minlog file we have chosen $M(4)+n$ because the
proofs are simpler with the addition instead of the maximum.

###  3.2 Indirect approach

Now we redo the proof using translations between the Cauchy and sd-
representation. First we state the completeness of Cauchy-reals, which will be
used.

######  Theorem 12 (RealComplete).

Assume $xs$ and $M\in\mathbf{Mon}$ such that $\forall_{n\in\mathbf{T}}(xs\
n)\in\mathbf{R}$ and $\mathbf{Cauchy}(xs,M)$ then there exists
$x\in\mathbf{R}$ such that $\mathbf{Conv}(xs,x,M)$.

######  Proof 3.6.

We refer to Theorem 2.3 in [Sch03].

The extracted term is:

      cRealComplete :: ((Nat -> Rea) -> ((Pos -> Nat) -> Rea))
      cRealComplete xs0 m1 = RealConstr
                                (\ n -> (realSeq (xs0 n)
                                           (realMod (xs0 n) (cNatPos n))))
                                (\ p -> ((m1 (p + 1)) ‘max‘ ((p + 1) + 1)))

Note the following: Given witnesses $(as_{n},M_{n})_{n}$ to
$\forall_{n\in\mathbf{T}}(xs\ n)\in\mathbf{R}$, the rational sequence
witnessing the limit is given by $as\ n:=as_{n}(M_{n}\ n)$ and the Cauchy-
modulus of the limit-real is given by $Np:=\mathtt{max}(M(p+1),p+2)$ where $M$
is the modulus of convergence.

As preparation for the indirect proof we state some elementary properties of
limits and sequences that we will need but do not have any computational
content.

######  Lemma 13.

Assume $xs$ is a sequence of reals, and $M\in\mathbf{Mon}$, $x:\mathbb{R}$
such that $\mathbf{Conv}(xs,x,M)$. We have
(i) $\mathbf{Cauchy}(xs,N)$, where $Np:=M(p+1)$,
(ii) $\forall_{n\in\mathbf{T}}|(xs\ n)|\leq 1\to|x|\leq 1$ and
(iii) $\forall_{y,N\in\mathbf{Mon}}(\mathbf{Conv}(xs,y,N)\to x=y)$.

######  Proof 3.7.

(i) Follows directly by using the triangle inequality and the definitions.
(ii) For arbitrary $p\in\mathbf{T}$ let $n:=M(p)$. Then
$|x|\leq|x-xs(n)|+|xs(n)|\leq 2^{-p}+1$. As $p\in\mathbf{T}$ is arbitrary it
follows $|x|\leq 1.$
(iii) We have $xs(n)-x$ converges to $0$ with modulus $M$ and $xs(n)-y$
converges to $0$ with modulus $N$. Therefore, $x-y$ converges to zero with
modulus $p\mapsto\max\\{M(p+1),N(p+1)\\}$. I.e. $|x-y|\leq 2^{p}$ for all $p$
and therefore $x-y=0$.

Using the lemmas above, the indirect proof of the convergence theorem become
quite short:

######  Proof 3.8 (Proof.( $\mathtt{SdLim}$, indirect)).

Assume $x$, $xs$, $M\in\mathbf{Mon}$, $\forall_{n\in\textbf{T}}(xs\
n)\in{{}^{co}\mathbf{I}}$ and $\forall_{n\geq M(p)}|(xs\ n)-x|\leq 2^{-p}$. We
apply Theorem 3 to $\forall_{n\in\mathbf{T}}(xs\ n)$ and get

$\forall_{n\in\mathbf{T}}xs\in\mathbf{R}\wedge|xs\ n|\leq 1.$

By the lemma above $xs$ is a Cauchy-sequence. So we apply Theorem 12 to get
$y\in\mathbf{R}$ with $\mathbf{Conv}(xs,y,N)$. By the above lemma
$x=y\in\mathbf{R}$ and $|y|\leq 1$, so $x\in{{}^{co}\mathbf{I}}$ by Theorem 6
and 1.

The extracted term for this proof is given by

      cCoILim :: ((Pos -> Nat) -> ((Nat -> Str) -> Str))
      cCoILim m g =  cCsToStr (cRealComplete
                                 (\ n -> (cStrToCs (g n)))
                                 (\ p -> (m (p + 1))))),

i.e. given a sequence $u_{0}u_{1}\dots$ of $\mathbf{Sd}$-streams we apply
$\mathtt{cRealComplete}$ to the sequence of translated stream
$\mathtt{cStrToCs}(u_{0})\mathtt{cStrToCs}(u_{1})\dots$ and then translate the
result back.

###  3.3 Comparison

We now compare the two algorithms obtained by the direct and indirect method.
To understand the results of the runtime-experiments we analyze the lookahead
of the algorithms first. If we unfold the $\mathtt{cRealComplete}$ in
definition of the indirect case we obtain

$\mathtt{cCoILim}(M,us)=\mathtt{cCsToStr}\left(\left(\sum_{i=1}^{n}\frac{(us_{n})_{i}}{2^{i}}\right)_{n},\lambda_{p}M(p+2)\right)$

and $\mathtt{cCsToStr}(as,M)$ compares $as(M\;3)$ with $\pm 0.25$. So to
compute the $n$-th digit of $\mathtt{cCoILim}(M,us)$ we need to examine the
first $M(4+n)$ digits of $us_{M(4+n)}$. The algorithm in the direct case was
given by

$\displaystyle\texttt{Lim}\ M\ F:=\begin{cases}\mathrm{C}\ 1\ (\texttt{Lim}\
\lambda_{p}M(p+1)\ \lambda_{n}(\texttt{DD}q^{-}F(M(4)+n)))&\text{if
}F(M(4))\in\textbf{R}\\\ \mathrm{C}\ 0\ (\texttt{Lim}\ \lambda_{p}M(p+1)\
\lambda_{n}(\texttt{D}F(M(4)+n)))&\text{if }F(M(4))\in\textbf{M}\\\
\mathrm{C}\ \overline{1}\ (\texttt{Lim}\ \lambda_{p}M(p+1)\
\lambda_{n}(\texttt{DD}q^{+}F(M(4)+n)))&\text{if
}F(M(4))\in\textbf{L}\end{cases}$

By examining the defining equations of $\mathtt{D},q^{\pm}$ on easily sees
that all these functions have a look-ahead of $n+1$. For the first digit we
need to decide whether $F(M(4))$ is in $\textbf{R},\textbf{M}$ or L which
requires the first three digits, since we apply $\mathtt{cCoITripleClosure}$.
Then the worst cases are $\textbf{R},\textbf{L}$ which add $3$ to the next
lookahead. All in all, to compute the $n$-th digit of $\texttt{Lim}\ M\ F$ we
need to examine the first $3n$ digits of $F(M4+n)$. As we can see the look-
ahead of the indirect algorithm depends on the modulus of convergence, whereas
in the direct case it is independent. Hence in case the modulus of convergence
is lower than $\lambda_{n}3n$ the indirect algorithm should outperform the
direct one.
As a first test we run both algorithms in Haskell on the constant sequence
$us:=\lambda_{n}[0,0,...]$ which converges with the constant modulus
$\lambda_{p}0$. To test the dependence of the two algorithms on the modulus of
convergence we artificially set different moduli and compute the first $50$
respectively $100$ digits. All measurements are in seconds.

Modulus | indirect(50) | direct(50) | indirect(100) | direct(100)
---|---|---|---|---
$\lambda_{p}p$ | 0.05 | 0.01 | 0.06 | 0.02
$\lambda_{p}p^{2}$ | 0.75 | 0.01 | 3.18 | 0.02
$\lambda_{p}p^{3}$ | 36.03 | 0.01 | 495.91 | 0.02

Figure 3: First test - Constant sequence with different moduli

As a second experiment we take the geometric series $(x^{n})_{n}$ for some
$|x|\leq 0.5$. This is a Cauchy-sequence converging to $0$ with modulus
$\lambda_{p}p$, since for $n\leq m$ and $|x|\leq 0.5$ we have

$|x^{n}-x^{m}|\leq|x^{n}||1-x^{n-m}|\leq\frac{1}{2^{n}}.$

For this test we use the Haskell $\mathtt{System.Random}$ package to generate
a pseudo-random stream $u$ of $\mathbf{Sd}$. Then we put a $0$ in front to
ensure that the absolute value is bounded by $0.5$. Then we run both
algorithms for the sequence $us$ given by

$us\ 0:=0::u\qquad us(n+1)=\mathtt{cCoIMult}(0::u)(us\,n),$

where $\mathtt{cCoIMult}$ is the algorithm from [Sch21b]. The results below
are the average over $n=15$ runs. The direct algorithm did not terminate in a
reasonable amount of time ($\leq 30$ minutes) for $n\geq 30$ digits. As
expected the indirect algorithm is better here, since the modulus of
convergence is the identity here.

digits | indirect | direct
---|---|---
5 | 0.74 | 0.69
10 | 3.3 | 23.4
20 | 26 | 1227
30 | 87 | -
40 | 239 | -
50 | 502 | -
Figure 4: Second test - Geometric sequence

##  4 Applications

###  4.1 Heron’s method

To show an application of the two algorithms extracted in the last section, we
define the Heron sequence and show that it converges to the square root.
[Heron] We define
$\text{H}:\mathbb{R}\rightarrow\mathbb{N}\rightarrow\mathbb{R}$ by the
computation rules

$\text{H}(x,0):=1,\qquad\text{H}(x,n+1):=\frac{1}{2}\left(\text{H}(x,n)+\frac{x}{\text{H}(x,n)}\right).$

For every non-negative $x$ the sequence
$H(x,\cdot)=:H(x):\mathbb{N}\rightarrow\mathbb{R}$ is the sequence, we get
from Heron’s method with initial value 1. Note that $H$ is well-defined for
non-negative $x$ since $H(x,n)\geq 2^{-n}$.

######  Lemma 14.

For every $x\in[0,1]$ $H(x)$ converges to $\sqrt{x}$ with modulus
$\iota:\mathbb{Z}^{+}\to\mathbb{N}$. Furthermore we have that

$\forall_{n\in\textbf{T}}\sqrt{x}\leq H(x,n).$

######  Proof 4.1.

Let $x\in[0,1]$ be given. We define $\Delta(x,n):=H(x,n)-\sqrt{x}$. We
calculate

$\displaystyle\Delta(x,n+1)$
$\displaystyle=\frac{1}{2}\left(\text{H}(x,n)+\frac{x}{\text{H}(x,n)}\right)-\sqrt{x}=\frac{(H(n,x))^{2}-2H(x,n)\sqrt{x}+x}{2H(x,n)}$
$\displaystyle=\frac{(\Delta(x,n))^{2}}{2H(x,n)}.$

By induction on $n$ we immediately get $0\leq H(x,n)$ and therefore
$0\leq\Delta(x,n+1)$. Since $\Delta(x,0)=1-\sqrt{x}\geq 0$ we have
$\forall_{n\in\textbf{T}}\sqrt{x}\leq H(x,n)$.
Furthermore, we calculate:

$\displaystyle\Delta(x,n+1)$
$\displaystyle=\frac{(\Delta(x,n))^{2}}{2H(x,n)}=\frac{1}{2}\Delta(x,n)\frac{\Delta(x,n)}{H(x,n)}=\frac{1}{2}\Delta(x,n)\left(1-\frac{\sqrt{x}}{H(x,n)}\right)$
$\displaystyle\leq\frac{1}{2}\Delta(x,n)$

Therefore, by induction we have $|H(x,n)-\sqrt{x}|=\Delta(x,n)\leq 2^{-n}$ and
this implies

$\forall_{p\in\textbf{T}}\forall_{n\geq p}|H(x,n)-\sqrt{x}|\leq 2^{-p},$

i.e. $H(x)$ converges to $\sqrt{x}$ with modulus $\iota$.

This lemma by itself does not have any computational content, but it states
that $\iota$ is a modulus of convergence of $Hx$ to $\sqrt{x}$. In some
special cases we can improve on the modulus. [Poslog] For a positive integer
$p$ we define $\texttt{poslog}(p)$ as the least natural number $n$ with $p\leq
2^{n}$. Equivalently it is the number of digits in the binary representation.
One possibility to implement the function poslog is to define an auxiliary
function
$\texttt{auxlog}:\mathbb{Z}^{+}\rightarrow\mathbb{N}\rightarrow\mathbb{N}$
with the computation rules

$\displaystyle\texttt{auxlog}\ p\ n:=\begin{cases}n,&\text{if }p\leq 2^{n}\\\
\texttt{auxlog}\ p\ (n+1),&\text{otherwise,}\end{cases}$

and then set $\texttt{poslog}(p):=\texttt{auxlog}\ p\ 0$.

######  Proposition 15.

If $x\in[\frac{1}{4},1]$ then
$\mathtt{poslog}:\mathbb{Z}^{+}\rightarrow\mathbb{N}$ is a modulus of
convergence of $H(x)$ to $\sqrt{x}$.

######  Proof 4.2.

Let $x\in[\frac{1}{4},1]$. From Lemma 14 we know
$\forall_{n\in\mathbf{T}}\sqrt{x}\leq H(x,n)$ and therefore
$\forall_{n\in\mathbf{T}}\frac{1}{2}\leq H(x,n)$. In the proof of Lemma 14 the
formula

$\Delta(x,n+1)=\frac{(\Delta(x,n))^{2}}{2H(x,n)}$

is proven. This implies $\Delta(x,n+1)\leq(\Delta(x,n))^{2}$. Since
$\frac{1}{2}\leq\sqrt{x}$, by induction we get

$\Delta(x,n)\leq 2^{-2^{n}}$

for all $n\in\mathbf{T}$. Hence for given $p$ and $n\geq\texttt{poslog}(p)$ we
get $p\leq 2^{n}$ and

$\left|H(x,n)-\sqrt{x}\right|=\Delta(x,n)\leq 2^{-2^{n}}\leq 2^{-p}.$

######  Lemma 16.

For all $x\in{{}^{co}\mathbf{I}}$ with $\frac{1}{16}\leq x$ we have
$\forall_{n\in\textbf{T}}H(x,n)\in{{}^{co}\mathbf{I}}$. Expressed as a formula

$\displaystyle\forall_{x\in{{}^{co}\mathbf{I}}}\left(\frac{1}{16}\leq
x\rightarrow\forall_{n\in\mathbf{T}}H(x,n)\in{{}^{co}\mathbf{I}}\right).$

######  Proof 4.3.

We use the results of [MS15], [SW20] and of Section 3.3 from [Wie17]. Namely
we have

$\displaystyle\forall_{x\in{{}^{co}\mathbf{I}},y\in{{}^{co}\mathbf{I}}}\frac{x+y}{2}\in{{}^{co}\mathbf{I}}.$
(1)

In Minlog this theorem is implemented in average.scm in the folder
examples/analysis and has the name CoIAverage. Furthermore

$\displaystyle\forall_{x\in{{}^{co}\mathbf{I}},y\in{{}^{co}\mathbf{I}}}\left(|x|\leq
y\rightarrow\frac{1}{4}\leq
y\rightarrow\frac{x}{y}\in{{}^{co}\mathbf{I}}\right)$ (2)

is proven there. In Minlog this theorem is implemented in sddiv.scm in the
folder examples/analysis and has the name CoIDiv. Using these, the proof of
this lemma is done by induction on $n$: For $n=0$ it is easy since $H(x,0)=1$
and $1\in{{}^{co}\mathbf{I}}$. For any total $n$ we have

$H(x,n+1)=\frac{1}{2}\left(H(x,n)+\frac{x}{H(x,n)}\right).$

By Lemma 14 we get $\sqrt{x}\leq H(n,x)$ and therefore

$\sqrt{\frac{1}{16}}=\frac{1}{4}\leq H(x,n)\quad\text{and}\quad
x\leq\sqrt{x}\leq H(x,n).$

Additionally, by the induction hypothesis, $H(x,n)\in{{}^{co}\mathbf{I}}$. By
(2) we have $\frac{x}{H(x,n)}\in{{}^{co}\mathbf{I}}$, so with (1) we get
$H(x,n+1)\in{{}^{co}\mathbf{I}}$.

By cCoIAverage and cCoIDiv we denote the computational content of (1) and (2).
Each of these terms takes two streams of reals and returns a stream of their
average and their quotient, respectively. Then the extracted term is

      cCoIHeron :: (Str -> (Nat -> Str))
      cCoIHeron u0 n1 = natRec n1
                          cCoIOne
                          (\ n2 -> (\ u3 -> (cCoIAverage u3 (cCoIDiv u0 u3))))

Informally the computational content Heron is defined by recursion:

$\displaystyle\texttt{Heron}\ v\ 0:=[1,1,\dots]$ $\displaystyle\texttt{Heron}\
v\ (n+1):=\texttt{cCoIAverage}(\texttt{Heron}\ v\ n)(\texttt{cCoIDiv}\ v\
(\texttt{Heron}\ v\ n))$

Which is Definition 4.1 in the notation of streams.

######  Theorem 17.

$\displaystyle\forall_{x\in{{}^{co}\mathbf{I}}}\left(0\leq
x\to\sqrt{x}\in{{}^{co}\mathbf{I}}\right)$

######  Proof 4.4.

We apply (2.3) with

$Px:=\exists_{y\in{{}^{co}\mathbf{I}}}\left(0\leq y\wedge\sqrt{y}=x\right).$

To show the goal formula, we need to show the second premise, namely for all
$x$

$\exists_{y\in{{}^{co}\mathbf{I}}}\left(0\leq
y\wedge\sqrt{y}=x\right)\rightarrow\exists_{d\in\mathbf{Sd},x^{\prime}}\left(x^{\prime}\in\left({{}^{co}\textbf{I}}\cup
P\right)\wedge|x^{\prime}|\leq 1\wedge x=\dfrac{d+x^{\prime}}{2}\right).$

Let $y\in{{}^{co}\mathbf{I}}$ with $0\leq x$ and $\sqrt{y}=x$ be given. Triple
application of ${{}^{co}\textbf{I}}^{-}$ to $y\in{{}^{co}\mathbf{I}}$ yields
$d_{1},d_{2},d_{3}\in\textbf{Sd}$ and $y^{\prime}\in{{}^{co}\mathbf{I}}$ with
$y=d_{1}d_{2}d_{3}y^{\prime}$. We distinguish three different cases:

If $y$ has one of the forms $\overline{1}d_{2}d_{3}y^{\prime}$,
$0\overline{1}d_{3}y^{\prime}$ or $00\overline{1}y^{\prime}$ we have $y\leq 0$
and therefore $x=\sqrt{y}=0$. Hence we define $d:=0$ and $x^{\prime}:=0$ and
the claim follows immediately.

If $y$ has one of the forms $000y^{\prime}$, $001y^{\prime}$,
$01\overline{1}y^{\prime}$ or $1\overline{11}y^{\prime}$ we can rewrite
$y=00ey^{\prime}$ for some $e\in\\{0,1\\}$. Here we define $d:=0$ and
$x^{\prime}:=\sqrt{\frac{e+y^{\prime}}{2}}$. Then

$x=\sqrt{y}=\sqrt{\frac{e+y^{\prime}}{8}}=\frac{\sqrt{\frac{e+y}{2}}}{2}=\frac{d+x^{\prime}}{2}.$

Furthermore $\frac{e+y^{\prime}}{2}\in{{}^{co}\mathbf{I}}$ by Lemma 2 and
$0\leq\frac{e+y^{\prime}}{2}$ since $0\leq y=\frac{e+y^{\prime}}{8}$.
Altogether we get $Px^{\prime}$.

The remaining case is that $y$ has one of the forms $010y^{\prime}$,
$011y^{\prime}$, $1\overline{1}1y^{\prime}$, $1\overline{1}0y^{\prime}$,
$10d_{3}y^{\prime}$ or $11d_{3}y^{\prime}$. In that case we have
$\frac{1}{8}\leq y$. Hence by Lemma 16
$\forall_{n\in\textbf{T}}{{}^{co}\textbf{I}}(H(y,n))$ and we know that $H(y)$
converges to $\sqrt{y}$ with modulus
$\iota:\mathbb{Z}^{+}\rightarrow\mathbb{N}$ by Lemma 14 . Thus we use Theorem
7 to get $x\in{{}^{co}\textbf{I}}$ and by one application of
${{}^{co}\mathbf{I}}^{-}$

$\exists_{d\in\mathbf{Sd},x^{\prime}\in{{}^{co}\mathbf{I}}}\left(|x^{\prime}|\leq
1\wedge x=\dfrac{d+x^{\prime}}{2}\right),$

which proves the goal formula.

We omit the description of the extracted term as Haskell code as it is quite
long due to the case distinctions. But we give an informal description of the
extracted term:

By the definitions of cSdLim as the computational content of Theorem 7 and
Heron as the computational content of Lemma 16 we have the following rules for
the computational content $\texttt{sqrt}:\texttt{Str}\rightarrow\texttt{Str}$
of this theorem:

$\displaystyle\texttt{sqrt}(\overline{1}u)$ $\displaystyle:=[0,0,\dots]$
$\displaystyle\texttt{sqrt}(0\overline{1}u)$ $\displaystyle:=[0,0,\dots]$
$\displaystyle\texttt{sqrt}(00u)$ $\displaystyle:=0\ \texttt{sqrt}\ u$
$\displaystyle\texttt{sqrt}(01\overline{1}u)$ $\displaystyle:=0\
\texttt{sqrt}\ 1u$ $\displaystyle\texttt{sqrt}(1\overline{11}u)$
$\displaystyle:=0\ \texttt{sqrt}\ 1u$ $\displaystyle\texttt{sqrt}\ u$
$\displaystyle:=\texttt{cSdLim}\ \iota\ (\texttt{Heron}\ u)$

The last rule shall only be applied if the other rules do not fit.

###  4.2 Multiplication

Our last application is motivated by Helmut Schwichtenberg and the Minlog file
sdmult.scm in examples/analysis. There it is proven that for any
$x,y\in{{}^{co}\mathbf{I}}$ the product $xy$ is also in ${{}^{co}\mathbf{I}}$.
In the following we use the limit-theorem to formulate another proof of this
theorem. Our approach is based on repeated applications of
${{}^{co}\mathbf{I}}^{-}$ to $y\in{{}^{co}\mathbf{I}}$, namely

$xy=\frac{xd_{1}+xy_{1}}{2}=\frac{x(d_{1}+\frac{d_{1}}{2})+x\frac{y_{2}}{2}}{2}=\dots=x\sum_{i=1}^{n}\frac{d_{i}}{2^{i}}+x\frac{y_{n}}{2^{n}},$

and the sequence $xs\ n:=\sum_{i=1}^{n}\frac{d_{i}}{2^{i}}$ converges to $y$.
In order to realize this idea we first we define a constant
$\mathtt{Sum}:\mathbb{L}(\mathbf{Sd})\to\mathbb{Q}$ by

$\mathtt{Sum}\,[]=0\qquad\mathtt{Sum}\,l:=\sum_{i=1}^{\mathtt{lth}(l)}\frac{(l)_{i}}{2^{i}},$

where $\mathtt{lth}:\mathbb{L}\to\mathbb{N}$ is the length-function for lists
and $(l)_{i}$ is the $i$-th element of the list $l$. We prove the following.

######  Lemma 18 (CoIMultSum).

Let $x\in{{}^{co}\mathbf{I}}$ then for all $l:\mathbb{L}(\mathbf{Sd})$ in
$\mathbf{T}$ we have

$x\cdot\mathtt{Sum}\,l\in{{}^{co}\mathbf{I}}.$

######  Proof 4.5.

We use the theorem CoIAverage (which was already mention in the proof of Lemma
16 and CoISdTimes (i.e.
$\forall_{x\in{{{}^{co}\mathbf{I}}},d\in\mathbf{Sd}}dx\in{{}^{co}\mathbf{I}}$).

The proof is done by induction on $l\in\mathbf{T}$. Namely if $l=[]$ then
$x\cdot 0=0\in{{}^{co}\mathbf{I}}$ (see CoIZero in Minlog). Now assume that
$x\cdot\mathtt{Sum}\,l\in{{}^{co}\mathbf{I}}$ and $d\in\mathbf{Sd}$. We
calculate

$x\cdot\mathtt{Sum}(d::l)=x\sum_{i=1}^{n+1}\frac{(l)_{i}}{2^{i}}=\frac{1}{2}\left(x\sum_{i=1}^{n}\frac{(l)_{i+1}}{2^{i}}+x\cdot(l)_{1}\right).$

Now we can apply CoIAverage, namely $x\cdot l_{1}\in{{}^{co}\mathbf{I}}$ by
CoISdTimes and the first summand is in ${{}^{co}\mathbf{I}}$ by the induction
hypothesis.

Note that the induction hypothesis is applied to the list
$(l)_{2}::\dots::(l)_{n+1}$, so the stream computed in the previous step is
not used. Therefore, the runtime of the algorithm must be at least quadratic
in the length of the list in the output. We will later see that the runtime of
the algorithm that is obtained is worse that the one extracted in [Sch21b].
The Haskell-translation of the extracted term is

      cCoIMultSum :: Str -> [Sd] -> Str
      cCoIMultSum u0 l1 = listRec
        l1
        cCoIZero
        (\ s2 -> (\ l3 -> (\ u4 -> (cCoIAverage (cCoISdTimes s2 u0) u4))))

And the computational content of the lemma, here denoted
$\mathtt{f}:\texttt{Str}\to\mathbb{L}(\mathbf{Sd})\to\texttt{Str}$, can also
be be represented in the more readable form by

$\displaystyle\mathtt{f}(u,[])=\mathtt{cCoIZero}$
$\displaystyle\mathtt{f}(u,d::l)=\mathtt{cCoIAverage}(\mathtt{f}(u,l),\mathtt{cCoISdTimes}(d,u)),$

where cCoIZero is analogous to cCoIOne:

      cCoIZero :: Str
      cCoIZero = (aiCoRec () (\ g -> (SdM , (Right ()))))Ψ

The next lemma is basically repeated application of ${{}^{co}\mathbf{I}}^{-}$.
The proof is very similar to the proof of Theorem 3 and so are the extracted
terms.

######  Lemma 19 (CoIToConvSeq).

Let $x\in{{}^{co}\mathbf{I}}$ then there exists
$G:\mathbb{N}\to\mathbb{L}(\mathbf{Sd})$ in $\mathbf{T}$ such that

$\mathbf{Conv}(\lambda_{n}\mathtt{Sum}\,G(n),x,\iota).$

######  Proof 4.6.

For $x\in{{}^{co}\mathbf{I}}$ we first show that

$\exists_{G\in\mathbf{T}}\forall_{n\in\mathbf{T}}\exists_{y\in{{}^{co}\mathbf{I}}}\left(\mathtt{lth}(G\,n)=n\wedge
x=\mathtt{Sum}\,(G\,n)+\frac{y}{2^{n}}\right).$

By application of $\mathbf{CC}$ it suffices to show

$\forall_{n\in\mathbf{T}}\exists_{l\in\mathbf{T}}\exists_{y\in{{}^{co}\mathbf{I}}}\left(\mathtt{lth}(l)=n\wedge
x=\mathtt{Sum}\,l+\frac{y}{2^{n}}\right),$

which is done by induction on $n\in\mathbf{T}$. If $n=0$ then choose $y:=x$
and $l=[]$.
Now assume we have $l^{\prime}\in\mathbf{T}$ with $\mathtt{lth}(l^{\prime})=n$
and $z\in{{}^{co}\mathbf{I}}$ with

$x=\mathtt{Sum}\,l^{\prime}+\frac{z}{2^{n}}.$

We apply ${{}^{co}\mathbf{I}}^{-}$ to $z$ and get
$d\in\mathbf{Sd},y\in{{}^{co}\mathbf{I}}$ with $z=\frac{y+d}{2}$, then
$l:=l^{\prime}\star d$ (Note that $\star$ denotes concatenation of lists) will
do the trick.
So assume we have $G$ with the properties above and $n\in\mathbf{T}$. Then
there exists some $y_{n}\in{{}^{co}\mathbf{I}}$ with
$x=\mathtt{Sum}\,(G\,n)+\frac{y}{2^{n}}$ and

$\left|x-\mathtt{Sum}\,(G\,n)\right|\leq\frac{|y_{n}|}{2^{n}}\leq 2^{-n}.$

Hence $\mathtt{Sum}\,(G\,\cdot)$ converges to $x$ with modulus
$\mathtt{PosToNat}$.

The extracted term is

      cCoIToConvSeq :: Str -> Nat -> [Sd]
      cCoIToConvSeq u0 n1 = fst
        (natRec n1 ([] , u0)
        (\ n2 -> (\ g -> (case g of
          { (,) l u1 -> ((l ++ ((head u1) : [])) , (tail u1)) }))))

Let $\mathtt{g}:\texttt{Str}\to\mathbb{N}\to\mathbb{L}(\mathbf{Sd})$ denote a
simplified iterative version of the computational content of the last lemma.
It can be given by the computation rules

$\mathtt{g}(u,0)=([],u)\qquad\mathtt{g}(\mathrm{C}\,s\,v,n+1)=g(v,n)\star s,$

so this is the function that returns the first $n$ elements of the stream. The
last lemma we need states that limits are closed under multiplication, namely:

######  Lemma 20.

Assume $\mathbf{Conv}(ys,y,M)$ and $|x|\leq 1$ then
$\mathbf{Conv}(\lambda_{n}(x\cdot(ys\,n)),xy,M)$.

The proof is elementary. Now we can apply the limit theorem.

######  Theorem 21.

For all $x,y\in{{}^{co}\mathbf{I}}$ we have $x\cdot y\in{{}^{co}\mathbf{I}}$.

######  Proof 4.7.

We apply Lemma 19 to $y\in{{}^{co}\mathbf{I}}$ in order to obtain
$G\in\mathbf{T}$ with

$\mathbf{Conv}(\mathtt{Sum}(G,\cdot),y,\mathtt{PosToNat}).$

By Lemma 20 $x\cdot(\mathtt{Sum}(G\,n))\in{{}^{co}\mathbf{I}}$ for all $n$ and
it converges to $x\cdot y$ by Lemma 20. Hence, we apply Theorem 7.

The extracted term from Haskell is given by

      cCoIMultLim :: Str -> Str -> Str
      cCoIMultLim u0 u1 = cCoILim
        id
        (\ n2 -> (cCoIMultSum u0 (cCoIToConvSeq u1 n2))).

Now let $\mathtt{Mult}:\texttt{Str}\to\texttt{Str}\to\texttt{Str}$ denote the
computational content in human-readable. Then

$\mathtt{Mult}(u,v):=\mathtt{coilim}(\mathtt{PosToNat},\lambda_{n}\mathtt{f}(u,\mathtt{g}(v,n))).$

We compare the algorithms obtained in this way using the indirect and direct
limit theorem with the algorithm from [Sch21b] that was obtained from a direct
proof. To this end we apply all three algorithms to two randomly generated
sequences and measure the runtime in Haskell. The result is the average over
$n=10$ tests.

number of digits | mult(schwicht) | mult(lim,indirect) | mult(lim,direct)
---|---|---|---
5 | 0.056 | 0.51 | 0.1
10 | 0.061 | 15 | 0.71
15 | 0.063 | 432 | 11.6
30 | 0.095 | - | 60.8
100 | 0.43 | - | -
Figure 5: Third test - Runtime of different multiplication algorithms

Although the algorithm using the direct limit is better here, the algorithm
from [Sch21b] still performs best. It seems that in order to obtain efficient
algorithms, completeness results should only be used if they are really
needed.

##  5 Conclusion and further work

We presented a formal method for extracting verified algorithms for exact real
number arithmetic using different representations. All the proofs up to
Section 4 have been carried out in the proof assistant Minlog. Furthermore
automatic generation of correctness proofs and translation to Haskell was
carried out. Even though the proofs from 4 have only been partially carried
out in a proof assistant, the program extraction by hand was still a reliable
method to get certified algorithms.

We assume that the direct approach yields a more efficient algorithm. Although
algorithms extracted via the indirect method by translations tend to have a
low look-ahead, they do rely on rational arithmetic. Our aim was to obtain
verified algorithms and we do not claim that our programs are the most
efficient. Some inefficiency stems from overestimation of bounds in formal
proofs. These can usually be removed by careful analysis of the proofs
involved.

Since we have proven that the signed digit representation is closed under
multiplication, average, division and limits we can now easily prove that a
lot of functions are represented by stream-transformers, e.g. trigonometric
functions, using their Taylor-expansion directly as was done for Herons
algorithm. Another viable approach to limits should be to use the completeness
of metric spaces, i.e. prove that signed-digits-reals satisfy the axioms of a
metric space and then use a completeness theorem for abstract metric spaces.

## Acknowledgment

The first author would like to thank the Istituto Nazionale di Alta Matematica
“Francesco Severi” for their scholarship of his PhD study.
Both authors would like to thank Helmut Schwichtenberg for proof reading this
paper and for his support during the creation of this paper.

## References

  * [BH08] Ulrich Berger and Tie Hou.  Coinduction for Exact Real Number Computation.  Theory of Computing Systems, 43(3):394–409, 2008.
  * [BS12] Ulrich Berger and Monika Seisenberger.  Proofs, programs, processes.  Theory of Computing Systems, 51(3):313–329, 2012.
  * [CG06] Alberto Ciaffaglione and Pietro Di Gianantonio.  A certified, corecursive implementation of exact real numbers.  Theoretical Computer Science, 351:39–51, 2006.
  * [K1̈8] Nils Köpp.  Automatically verified program extraction from proofs with applications to constructive analysis.  MSc Thesis, Ludwig Maximilians University Munich, 2018.
  * [Miy17] Kenji Miyamoto.  The Minlog System.  http://www.mathematik.uni-muenchen.de/~logik/minlog/index.php, 2017\.  [Online; accessed 29-January-2017].
  * [MS15] Kenji Miyamoto and Helmut Schwichtenberg.  Program extraction in exact real arithmetic.  Mathematical Structures in Computer Science, 25(Special issue 8):1692–1704, 2015.
  * [Sch03] Helmut Schwichtenberg.  Constructive analysis with witnesses.  In Proc. NATO Advanced Study Institute, Marktoberdorf, 2003, pages 323–353, 2003.
  * [Sch21a] Helmut Schwichtenberg.  Computational aspects of Bishop’s constructive mathematics.  In D. Bridges, H. Ishihara, H. Schwichtenberg, and M. Rathjen, editors, Handbook of constructive mathematics. Cambridge University Press, 2021.  Submitted.
  * [Sch21b] Helmut Schwichtenberg.  Logic for exact real arithmetic: Multiplication.  preprint, 2021.
  * [SW12] Helmut Schwichtenberg and Stanley S. Wainer.  Proofs and Computations.  Perspectives in Logic. Association for Symbolic Logic and Cambridge University Press, 2012.
  * [SW20] Helmut Schwichtenberg and Franziskus Wiesnet.  Logic for exact real arithmetic.  submitted, 2020.
  * [Wie80] Edwin Wiedmer.  Computing with infinite objects.  Theoretical Computer Science, 10:133–155, 1980.
  * [Wie17] Franziskus Wiesnet.  Konstruktive Analysis mit exakten reellen Zahlen.  MSc Thesis, Ludwig Maximilians University Munich, 2017.
  * [Wie18] Franziskus Wiesnet.  Introduction to Minlog.  In Klaus Mainzer, Peter Schuster, and Helmut Schwichtenberg, editors, Proof and Computation, pages 233–288. World Scientific, 2018.