Logic for exact real arithmetic

TL;DR

This paper presents a method to extract a division algorithm for real numbers represented as digit streams from formal proofs using coinductive predicates, with implementation in Minlog and translation to Haskell.

Contribution

It introduces a formal proof framework for real arithmetic with coinductive definitions and demonstrates extraction of executable algorithms from these proofs.

Findings

Successfully extracted a division algorithm from formal proofs.

Implemented the algorithm in Haskell for practical use.

Validated the approach with experimental results.

Abstract

Continuing earlier work of the first author with U. Berger, K. Miyamoto and H. Tsuiki, it is shown how a division algorithm for real numbers given as a stream of signed digits can be extracted from an appropriate formal proof. The property of being a real number represented as a stream is formulated by means of coinductively defined predicates, and formal proofs involve coinduction. The proof assistant Minlog is used to generate the formal proofs and extract their computational content as terms of the underlying theory, a form of type theory for finite or infinite data. Some experiments with running the extracted term are described, after its translation to Haskell.

Equations

$$\vec{\alpha }\to (\xi {)}_{i<n}\to \xi$$

$$\iota :={\mu }_{\xi }\vec{\kappa }(\vec{\kappa }not\; empty)$$

$$\mathbb{U}$$

$$\mathbb{B}$$

$$\mathbb{D}$$

$$\mathbb{N}$$

$$\mathbb{P}$$

$$\mathbb{Z}$$

$$\mathbb{Y}$$

$$\mathbb{I}(\alpha )$$

$$\mathbb{L}(\alpha )$$

$$\mathbb{S}(\alpha )$$

$$\alpha \times \beta$$

$$\alpha +\beta$$

$$\rho ,\sigma ,\tau ::=\alpha \mid \iota (\vec{\rho })\mid \tau \to \sigma ,$$

$$\mathrm{lev}(\alpha )$$

$$\mathrm{lev}(\iota (\vec{\rho }))$$

$$\mathrm{lev}(\tau \to \sigma )$$

$$\mathrm{Branch}(-,\mathrm{Branch}(-,-))\mathrm{Branch}(-,\mathrm{Branch}(\ast ,-))$$

$$\begin{picture}(48.0,36.0)\put(0.0,18.0){\makebox(0.0,0.0)[]{$-$}} \put(48.0,18.0){\makebox(0.0,0.0)[]{$-$}} \par\put(0.0,12.0){\line(2,-1){24.0}} \put(24.0,0.0){\line(2,1){24.0}} \end{picture}\quad\not\uparrow\quad\begin{picture}(60.0,36.0)\put(0.0,18.0){\makebox(0.0,0.0)[]{$-$}} \put(36.0,30.0){\makebox(0.0,0.0)[]{$\ast$}} \put(60.0,30.0){\makebox(0.0,0.0)[]{$\ast$}} \par\put(0.0,12.0){\line(2,-1){24.0}} \put(24.0,0.0){\line(2,1){24.0}} \put(48.0,12.0){\line(-1,1){12.0}} \put(48.0,12.0){\line(1,1){12.0}} \end{picture}\quad\hbox{but}\quad\begin{picture}(48.0,36.0)\put(0.0,18.0){\makebox(0.0,0.0)[]{$-$}} \put(48.0,18.0){\makebox(0.0,0.0)[]{$\ast$}} \par\put(0.0,12.0){\line(2,-1){24.0}} \put(24.0,0.0){\line(2,1){24.0}} \end{picture}\quad\uparrow\quad\begin{picture}(60.0,36.0)\put(0.0,18.0){\makebox(0.0,0.0)[]{$-$}} \put(36.0,30.0){\makebox(0.0,0.0)[]{$\ast$}} \put(60.0,30.0){\makebox(0.0,0.0)[]{$\ast$}} \par\put(0.0,12.0){\line(2,-1){24.0}} \put(24.0,0.0){\line(2,1){24.0}} \put(48.0,12.0){\line(-1,1){12.0}} \put(48.0,12.0){\line(1,1){12.0}} \end{picture}$$

$$\{\quad\begin{picture}(48.0,36.0)\put(0.0,18.0){\makebox(0.0,0.0)[]{$-$}} \put(48.0,18.0){\makebox(0.0,0.0)[]{$\ast$}} \par\put(0.0,12.0){\line(2,-1){24.0}} \put(24.0,0.0){\line(2,1){24.0}} \end{picture}\quad,\quad\begin{picture}(48.0,36.0)\put(0.0,18.0){\makebox(0.0,0.0)[]{$\ast$}} \put(48.0,18.0){\makebox(0.0,0.0)[]{$-$}} \par\put(0.0,12.0){\line(2,-1){24.0}} \put(24.0,0.0){\line(2,1){24.0}} \end{picture}\quad\}\qquad\vdash_{\mathbb{Y}}\qquad\begin{picture}(48.0,36.0)\put(0.0,18.0){\makebox(0.0,0.0)[]{$-$}} \put(48.0,18.0){\makebox(0.0,0.0)[]{$-$}} \par\put(0.0,12.0){\line(2,-1){24.0}} \put(24.0,0.0){\line(2,1){24.0}} \end{picture}$$

$$\begin{picture}(60.0,36.0)\put(0.0,18.0){\makebox(0.0,0.0)[]{$\ast$}} \put(36.0,30.0){\makebox(0.0,0.0)[]{$\ast$}} \put(60.0,30.0){\makebox(0.0,0.0)[]{$-$}} \par\put(0.0,12.0){\line(2,-1){24.0}} \put(24.0,0.0){\line(2,1){24.0}} \put(48.0,12.0){\line(-1,1){12.0}} \put(48.0,12.0){\line(1,1){12.0}} \end{picture}\qquad\vdash_{\mathbb{Y}}\qquad\begin{picture}(60.0,36.0)\put(0.0,18.0){\makebox(0.0,0.0)[]{$\ast$}} \put(36.0,30.0){\makebox(0.0,0.0)[]{$\ast$}} \put(60.0,30.0){\makebox(0.0,0.0)[]{$\ast$}} \par\put(0.0,12.0){\line(2,-1){24.0}} \put(24.0,0.0){\line(2,1){24.0}} \put(48.0,12.0){\line(-1,1){12.0}} \put(48.0,12.0){\line(1,1){12.0}} \end{picture}\quad\hbox{and}\quad\begin{picture}(48.0,36.0)\put(0.0,18.0){\makebox(0.0,0.0)[]{$\ast$}} \put(48.0,18.0){\makebox(0.0,0.0)[]{$\ast$}} \par\put(0.0,12.0){\line(2,-1){24.0}} \put(24.0,0.0){\line(2,1){24.0}} \end{picture}$$

$$-$$

$$(1)-(4)$$

$$(5)$$

$$(6)$$

$$\{\mathsf{f}\mathsf{f}\}::\{\mathsf{f}\mathsf{f}\}::\{\mathsf{t}\mathsf{t}\}::\mathrm{Nil}abbreviatedRRL[]$$

$$RL[]/\uparrow RRL\ast ,RR\ast \uparrow RRL\ast$$

$$RRL\ast ⊢RR\ast ,R\ast (and\; also\; e.g.RR\varnothing \ast ),$$

$$RRL[]⊢RRL\ast ,RR\ast ,R\ast$$

$$RLRR[]$$

$$RLRR\dots R\ast$$

$$RLRR\ast$$

$${\mathcal{R}}_{\mathbb{L}}^{\tau }$$

$${\mathcal{D}}_{\mathbb{L}}$$

$${}^{\mathrm{co}}{\mathcal{R}}_{\mathbb{L}}^{\tau }$$

$${\mathcal{R}}_{\mathbb{L}}^{\tau }([],z,f)=z,{\mathcal{R}}_{\mathbb{L}}^{\tau }(s::\ell ,z,f)=f(s,\ell ,{\mathcal{R}}_{\mathbb{L}}^{\tau }(\ell ,z,f)).$$

$${\mathcal{D}}_{\mathbb{L}}([])=\mathrm{InL}(\mathrm{Dummy}),{\mathcal{D}}_{\mathbb{L}}(s::\ell )=\mathrm{InR}⟨s,\ell ⟩.$$

$${}^{\mathrm{co}}{\mathcal{R}}_{\mathbb{L}}^{\tau }zf=\{\begin{array}{ll}[]& iffz\equiv \mathrm{InL}(\mathrm{Dummy}),\\ s::u& iffz\equiv \mathrm{InR}⟨s,\mathrm{InL}(u)⟩,\\ s::{}^{\mathrm{co}}{\mathcal{R}}_{\mathbb{L}}^{\tau }{z}^{\prime }f& iffz\equiv \mathrm{InR}⟨s,\mathrm{InR}(z^{\prime })⟩.\end{array}$$

Full text

This project has received funding from the European Union’s 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 731143. The second author is a Marie Skłodowska-Curie fellow of the Istituto Nazionale di Alta Matematica

Real numbers in the exact (as opposed to floating-point) sense can be defined as Cauchy sequences (of rationals, with modulus). However, for computational purposes it is better to see them as coded by “streams” of signed digits $\{1,0,-1\}$. A variant stream representation is the so-called “binary reflected” or Gray-code [Gia99, Tsu02] explained below. Apart from being practically more useful, the stream view turns real numbers into “infinite data” and hence objects of type level [math]. As a consequence the type level of other concepts in constructive analysis [Bis67] is lowered by one, which simplifies matters considerably.

Our overall goal is to obtain formally verified algorithms (given by terms in our language) operating on stream represented real numbers. Given an informal idea of how the algorithm should work, there are two methods how this can be achieved.

1. (I)

Formulate (using corecursion) the algorithm in the term language of a suitable theory, and then formally prove that this term satifies the specification; 2. (II)

Find a formal existence proof $M$ (using coinduction) for the object the algorithm is supposed to return. Then apply a proof theoretic method (“realizability”) to extract $M$’s computational content as a term (involving corecursion) in the term language of the underlying theory. The verification is done by a formal soundness proof of the realizability interpretation. The extraction of the computational content and the verification are automatic.

A general advantage of (II) over (I) is that one does not need to begin with a detailed formulation of the algorithm, but instead can stay on a more abstract level when proving the (existential) specification. In mathematics we know how to organize proofs, for instance by splitting them into lemmas or on occasion make use of more abstract concepts. In short, mathematical experience can help to find a well-structured algorithmic solution.

Method (I) was employed in [CG06] using Coq, and method (II) in [Ber09, MS15, BMST16] using Minlog. The present paper continues previous work [MS15, BMST16] by a case study on division. It is shown how a division algorithm for real numbers represented as either streams of signed digits or else in binary reflected form (Gray code) can be extracted from an appropriate formal proof dealing with concrete real numbers (Cauchy sequences of rationals, with moduli); in [MS15, BMST16] real numbers were treated axiomatically. The reason for switching to concrete real numbers is the desire to have reliable programs, which are less studied for real number computation. The method described in this paper achieves reliability by providing an (automatically generated) formal proof that the extracted program meets its specification. These proofs are in a formal theory whose consistency is guaranteed by a concrete model [Sco70, Ers77]. There is no need to rely on an axiom system for real numbers as in [MS15, BMST16].

We will work with constructive existence proofs in the style of [Bis67], but in such a way that we can switch on and off the availability of input data for the constructions implicit in the proof [Ber93]. In the present context this will be applied to real numbers as input data: we do not want to make use of the Cauchy sequence for the constructions to be done, but only the computational content of an appropriate coinductive predicate to which the real number is supposed to belong. We consider division of real numbers as a non-trivial case study; it has been dealt with in [CG06] using method (I). Based on the algorithmic idea in [CG06], we employ method (II) to extract signed digit and Gray code based stream algorithms for division from proofs that the reals are closed under division (under some obvious restrictions). As a benefit from the necessary organization into a sequence of lemmas we obtain a relatively easy analysis of the “look-ahead”, i.e., how far we have to look into the argument streams to obtain the $n$-th digit of the result stream.

The paper is organized as follows. Section 1 collects some background material. Section 1.1 describes (mainly by examples) the base type objects of the Scott-Ershov [Sco70, Ers77] model of partial continuous functionals, which is the intended model of the theory $\mathrm{TCF}$ we are going to use. It is a form of type theory suitable for reasoning with finite and infinite data. This theory is described in Section 1.2. The notion of computational content of proofs is introduced in Section 1.3. Section 1.4 recalls the constructive theory of real numbers of Bishop [Bis67, Ch.2]. In Section 2 division for stream-represented real numbers is studied, both for signed and binary reflected digit streams. Formalizations of the relevant proofs are described, including the terms (programs) extracted from them. Numerical experiments after translating these terms into Scheme or Haskell programs are discussed. Section 3 recalls the notion of realizability in Section 3.1, sketches a proof of the general soundness theorem in Section 3.2, and its formalization for real division algorithms in Section 3.3. Section 4 concludes.

1. Preliminaries

We informally describe a formal theory $\mathrm{TCF}$ [SW12, Section 7.1] which will be used to carry out proofs on real numbers and also functions and predicates on real numbers. In contrast to [MS15, BMST16] where an axiomatic approach was used we now work with concrete real numbers: Cauchy sequences of rationals, with moduli. The reason for this switch is that we aim at full reliability of the soundness proofs we will (automatically) generate (see Section 3). The axioms the formal theory is based upon, and hence all propositions proved, are valid in a model and therefore correct.

The base type data of the theory are free algebras given by their constructors, for instance lists of signed digits. Functions (“program constants”) are defined by defining equations (“computation rules”) whose left hand sides are non-overlapping constructor patterns. Termination is not required, which makes it possible the have the corecursion operator (see below) as an ordinary constant in the language. Predicates are least and greatest fixed points of clauses.. Examples are totality and cototality of lists of signed digits. The only axioms are the defining equations of the functions and the introduction and elimination axioms for the (co)inductively defined constants, which state their fixed point properties.

An important predicate is equality. Clearly we have the inductively defined Leibniz equality and the decidable equality for finitary algebras like the natural numbers. Equality on the (concrete) reals is more delicate. It is defined from an inductive $\leq$-predicate which refers to the underlying Cauchy sequences and their moduli. For all functions and predicates on the reals that we consider it is necessary to prove compatibility with real equality. The reason for this extension of the axiomatic treatment is to obtain formal proofs which rest only on the fixed point axioms and in this sense are correct: the propositions proved are valid in the concrete model of $\mathrm{TCF}$.

1.1. Objects

Base type objects of our theory are determined by the constructors of (free) algebras. More precisely, let $\alpha,\beta,\xi$ be type variables.

Definition**.**

Constructor types $\kappa$ have the form

[TABLE]

with all type variables $\alpha_{i}$ distinct from each other and from $\xi$. Iterated arrows are understood as associated to the right. An argument type of a constructor type is called a parameter argument type if it is different from $\xi$, and a recursive argument type otherwise. A constructor type $\kappa$ is nullary if it has no recursive argument types. We call

[TABLE]

an algebra form (“form” since type parameters may occur). An algebra form is non-recursive (or explicit) if it does not have recursive argument types.

Examples**.**

We list some algebra forms without parameters, with standard names for the constructors added to each constructor type.

[TABLE]

Algebra forms with type parameters are

[TABLE]

The default name for the $i$-th constructor of an algebra form is $\mathrm{C}_{i}$.

Definition** (Type).**

[TABLE]

where $\iota$ is an algebra form with $\vec{\alpha}$ its parameter type variables, and $\iota(\vec{\rho}\,)$ the result of substituting the (already generated) types $\vec{\rho}$ for $\vec{\alpha}$. Types of the form $\iota(\vec{\rho}\,)$ are called algebras. An algebra is closed if it has no type variables. The level of a type is defined by

[TABLE]

Base types are types of level [math], and a higher type has level at least $1$.

Examples**.**

1. $\mathbb{L}(\alpha)$, $\mathbb{L}(\mathbb{L}(\alpha))$, $\alpha\times\beta$ are algebras.

2. $\mathbb{L}(\mathbb{L}(\mathbb{N}))$, $\mathbb{N}+\mathbb{B}$, $\mathbb{Q}:=\mathbb{Z}\times\mathbb{P}$ are closed base types.

3. $(\mathbb{N}\to\mathbb{Q})\times(\mathbb{P}\to\mathbb{N})$ is a closed algebra of level $1$.

There can be many equivalent ways to define a particular type. For instance, we could take $\mathbb{U}+\mathbb{U}$ to be the type of booleans, $\mathbb{L}(\mathbb{U})$ to be the type of natural numbers, and $\mathbb{L}(\mathbb{B})$ to be the type of positive binary numbers.

We introduce the base type objects by example only, for $\mathbb{N}$, $\mathbb{Y}$, $\mathbb{L}(\mathbb{B})$; cf. [SW12, Section 6.1.4] for the general case. These objects are built from tokens, which are type correct constructor expressions possibly containing the special symbol $\ast$ which carries no information. Examples in the algebra $\mathbb{Y}$ of binary trees are

[TABLE]

or pictorially

[TABLE]

For tokens we have obvious concepts called consistency ($\uparrow$) and entailment ($\vdash$). For instance

[TABLE]

Examples for entailment in $\mathbb{Y}$ are

[TABLE]

and also

[TABLE]

Definition**.**

Objects of a base type are finite or infinite sets of tokens with are consistent and closed under entailment. An object $x$ is cototal if for each of its tokens $P(\ast)$ with a distinguished occurrence of $\ast$ there is another token in $x$ where this occurrence of $\ast$ is replaced by a constructor expression with only $\ast$’s as arguments. We call $x$ total if it is cototal and finite.

The tokens of $\mathbb{N}$ are shown in Figure 1. For tokens $a,b$ we have $\{a\}\vdash b$ if and only if there is a path from $a$ (up) to $b$ (down). There is exactly one cototal object, consisting of $S\ast$, $SS\ast$, $SSS\ast$ …. Note that $\ast$ is not a token; the “bottom” object is the empty set.

Examples of more interesting objects in $\mathbb{Y}$ are

1. (1)

$R:=$ closure (under entailment) of all tokens of the form

[TABLE] 2. (2)

$L$ is defined similarly 3. (3)

$L\cup R$ 4. (4)

$\frac{1}{2}:=$ closure of all tokens of the form

[TABLE] 5. (5)

Closure of

[TABLE] 6. (6)

Closure of

[TABLE]

Among these are

[TABLE]

Finally we consider the algebra $\mathbb{L}(\mathbb{B})$ of lists of booleans, to represent finite or infinite paths. Tokens in $\mathbb{L}(\mathbb{B})$ are for instance (writing $::$ for $\mathrm{Cons}$)

[TABLE]

Consistency in $\mathbb{L}(\mathbb{B})$:

[TABLE]

Entailment in $\mathbb{L}(\mathbb{B})$:

[TABLE]

Objects in $\mathbb{L}(\mathbb{B})$:

[TABLE]

Objects of higher type are canonically defined in the Scott-Ershov model [Sco70, Ers77]. A detailed exposition is in [SW12, Chapter 6].

1.2. Type theory for finite and infinite data

Terms are built from (typed) variables, constructors and (equationally) defined constants by $\lambda$-abstraction and application, where termination of the defining equations is not required. Defined constants are given by their type and computation rules. Examples for the type $\mathbb{L}:=\mathbb{L}(\mathbb{D})$ of lists of signed digits are

Terms are built from (typed) variables, constructors and (equationally) defined constants by $\lambda$-abstraction and application, where termination of the defining equations is not required. Defined constants are given by their type and computation rules. Examples for the type $\mathbb{L}:=\mathbb{L}(\mathbb{D})$ of lists of signed digits are

[TABLE]

$\mathcal{R}_{\mathbb{L}}^{\tau}$ takes a recursion argument $\ell\colon\mathbb{L}$, an initial value $z\colon\tau$ and a “step” argument $f\colon(\mathbb{D}\to\mathbb{L}\to\tau\to\tau)$ operating according to the structure of the given list. The meaning of $\mathcal{R}_{\mathbb{L}}^{\tau}$ is determined by the computation rules

[TABLE]

$\mathcal{D}_{\mathbb{L}}$ operates by disassembling the given list $\ell\colon\mathbb{L}$ into its head and tail. The computation rules are

[TABLE]

For ${}^{\mathrm{co}}\mathcal{R}_{\mathbb{L}}^{\tau}$ the “step” $f\colon(\tau\to\mathbb{U}+(\mathbb{D}\times(\mathbb{L}+\tau)))$ operates by inspection (or observation) of its argument $z\colon\tau$. More precisely, the meaning of ${}^{\mathrm{co}}\mathcal{R}_{\mathbb{L}}^{\tau}$ is given by the (non-terminating) computation rule

[TABLE]

We use $\equiv$ for Leibniz equality (inductively defined by the clause $\forall_{z}(z\equiv z)$).

Predicates are either (co)inductively defined or of the form $\{\,\vec{x}\mid A\,\}$ where $A$ is a formula. We identify $\{\,\vec{x}\mid A(\vec{x}\,)\,\}\vec{t}$ with $A(\vec{t\,}\,)$. Formulas are given as atomic formulas $P\vec{t}$ where $P$ is a predicate and $\vec{t}$ are terms, or else as $A\to B$ or $\forall_{x}A$ where $A$ and $B$ are already formulas. The formulas $\exists_{x}A$, $A\land B$ and $A\lor B$ technically are inductively defined (nullary) predicates.

An inductively defined predicate $I$ is given by clauses of the form

[TABLE]

for $i\in\{0,\dots,k-1\}$, $k>0$ and $n_{i}\geq 0$, where $I$ only occurs strictly positive in each $A_{ij}(I)$ and $\vec{x_{i}}$ contains all free variables of $A_{ij}(I)$ and $\vec{t}_{i}$. The clauses are called introduction axioms of $I$.

An example is the totality predicate $T_{\mathbb{L}}$. Its clauses are

[TABLE]

where $T_{\mathbb{D}}$ is the totality predicate for the three-element algebra $\mathbb{D}$ of signed digits, defined by the three clauses $T_{\mathbb{D}}s$ for $s$ a signed digit.

Intuitively, an inductively defined predicate is the smallest (w.r.t. $\subseteq$) predicate fulfilling its clauses. This is expressed by its elimination axiom:

[TABLE]

where $X$ can be any predicate with the same arity as $I$. The axiom $I^{-}$ is also called induction axiom. For example,

[TABLE]

Let $I$ be an inductively defined predicate given by its clauses $(I^{+}_{i})_{i<k}$, and assume that there are recursive calls in some clauses. To every such $I$ we associate a “companion” ${}^{\mathrm{co}}\!I$ and call it a coinductively defined predicate. The elimination (or closure) axiom ${}^{\mathrm{co}}\!I^{-}$ of the coinductively defined predicate says that if ${}^{\mathrm{co}}\!I\vec{x}$ holds, then it comes from one of the clauses:

[TABLE]

In words: if ${}^{\mathrm{co}}\!I\vec{x}$ holds, then there is at least one clause $I^{+}_{i}$ whose premises $(A_{ij}({}^{\mathrm{co}}\!I))_{j<n_{i}}$ (with ${}^{\mathrm{co}}\!I$ instead of $I$) are fulfilled and whose conclusion is ${}^{\mathrm{co}}\!I\vec{x}$ up to Leibniz equality. For example, the co-predicate associated with $T_{\mathbb{L}}$ is cototality ${}^{\mathrm{co}}T_{\mathbb{L}}$. Its elimination axiom is

[TABLE]

The introduction (or coinduction or greatest-fixed-point) axiom ${}^{\mathrm{co}}\!I^{+}$ of ${}^{\mathrm{co}}\!I$ says that ${}^{\mathrm{co}}\!I$ is the greatest predicate such that

[TABLE]

This means that any other “competitor” predicate $X$ satisfying the same closure property is below ${}^{\mathrm{co}}\!I$. For example,

[TABLE]

1.3. Computational content

We are interested in the computational content of proofs, which in the present setting arises from inductively and coinductively defined predicates only: they can be declared to be computationally relevant (c.r.) or non-computational (n.c.). This also applies to predicate variables $X$. The (finitely many) clauses of a c.r. inductive predicate $I$ determine an algebra $\iota_{I}$. A “witness” that $I\vec{t}$ or ${}^{\mathrm{co}}\!I\vec{t}$ holds has type $\iota_{I}$. It will be a total object in the first and a cototal object in the second case. For instance, the type of the c.r. version of $T_{\mathbb{L}}$ or ${}^{\mathrm{co}}T_{\mathbb{L}}$ is $\mathbb{L}$. A formula $A$ built from atomic formulas by $\to$, $\forall$ is c.r. if its final conclusion is. The type $\tau(A)$ is defined by

[TABLE]

Recall that $\exists_{x}A$, $A\land B$ and $A\lor B$ technically are inductively defined (nullary) predicates. If they are c.r., their types are $\tau(\exists_{x}A):=\tau(A)$; $\tau(A\land B):=\tau(A)\times\tau(B),\tau(A),\tau(B)$ depending on the c.r./n.c. status of $A,B$; $\tau(A\lor B):=\tau(A)+\tau(B),\tau(A)+\mathbb{U},\mathbb{U}+\tau(B),\mathbb{B}$ depending on the c.r./n.c. status of $A,B$.

Let $M$ be a proof in $\mathrm{TCF}$ of a c.r. formula $A$. We define its extracted term $\mathrm{et}(M)$, of type $\tau(A)$, with the aim to express $M$’s computational content. It will be a term built up from variables, constructors, recursion operators, destructors and corecursion operators by $\lambda$-abstraction and application:

[TABLE]

It remains to define extracted terms for the axioms. Consider a (c.r.) inductively defined predicate $I$. For its introduction and elimination axioms define $\mathrm{et}(I^{+}_{i}):=\mathrm{C}_{i}$ and $\mathrm{et}(I^{-}):=\mathcal{R}$, where both the constructor $\mathrm{C}_{i}$ and the recursion operator $\mathcal{R}$ refer to the algebra $\iota_{I}$ associated with $I$. For the closure and greatest-fixed-point axioms of ${}^{\mathrm{co}}\!I$ define $\mathrm{et}({}^{\mathrm{co}}\!I^{-}):=\mathcal{D}$ and $\mathrm{et}({}^{\mathrm{co}}\!I^{+}):={}^{\mathrm{co}}\mathcal{R}$, where both the destructor $\mathcal{D}$ and the corecursion operator ${}^{\mathrm{co}}\mathcal{R}$ again refer to the algebra $\iota_{I}$ associated with $I$.

1.4. Real numbers

Rational numbers $\mathbb{Q}$ are defined by $\mathbb{Q}:=\mathbb{Z}\times\mathbb{P}$, where the pair of $k\colon\mathbb{Z}$ and $p\colon\mathbb{P}$ is denoted by $\frac{k}{p}$. We also have the expected notion of equality between rational numbers. In contrast to the positive, natural, rational numbers or the integers, the real numbers are not an algebra. The property to be a real number is a predicate on $(\mathbb{N}\to\mathbb{Q})\times(\mathbb{P}\to\mathbb{N})$. Totality on this type means that both components map total arguments into total values. By a real number $x$ we mean a pair of this type whose first component is a Cauchy sequence $(a_{n})_{n\in\mathbb{N}}$ of rationals with the second component $M$ as modulus, i.e.,

[TABLE]

We write $\mathbb{R}$ for this predicate. For real numbers we can define the arithmetic functions $+$, $-$, $\cdot$ and the inverse and also the absolute value $|\cdot|$. Note that the inverse needs a witness that the real number is positive. We will not go into details here. An exact definition of these functions and also of positivity can be found in [Wie17, Wie18] and in the library of Minlog111http://minlog-system.de..

An important predicate on the real numbers is real equality: we define $x\leq y$ by

[TABLE]

and real equality $x=y$ by $x\leq y\land y\leq x$. Most of the predicates and functions on real numbers will be compatible with real equality; however, this must be proved in each case.

The rational numbers can be embedded into the real numbers by identifying a rational number $a$ with the pair consisting of the constant Cauchy sequence $(a)_{n\in\mathbb{N}}$ and the constant modulus $(0)_{p\in\mathbb{P}}$.

We use variable names

[TABLE]

Let $T_{\mathbb{Z}}^{\mathrm{nc}}$ be the n.c. version of the totality predicate for $\mathbb{Z}$, and similarly for other types. Let $\mathrm{Sd}$ be the (formally inductive) predicate consisting of the integers $1,0,-1$, i.e., $\mathrm{Sd}$ is given by the three clauses $1\in\mathrm{Sd}$, $0\in\mathrm{Sd}$ and $-1\in\mathrm{Sd}$. We require that $\mathrm{Sd}$ has computational content (in the three-element algebra $\mathbb{D}$), and write

[TABLE]

and similarly for $\exists$. In this case the premise $\hat{d}\in T_{\mathbb{Z}}^{\mathrm{nc}}$ is not necessary because it follows from $\hat{d}\in\mathrm{Sd}$. The predicate $\mathbb{R}$ and also $\leq,=$ on real numbers are assumed to be n.c. We write (with $x$ ranging over $[-1,1]$)

[TABLE]

and again similarly for $\exists$. The totality of $\hat{x}$ is part of $\hat{x}\in\mathbb{R}$.

We inductively define a predicate $I_{0}$ on reals $s$ such that the generating sequence $d_{0},\dots,d_{m-1}$ for $x\in I_{0}$ means that $x$ is between $\sum_{n<m}\frac{d_{n}}{2^{n+1}}-\frac{1}{2^{m}}$ and $\sum_{n<m}\frac{d_{n}}{2^{n+1}}+\frac{1}{2^{m}}$. Let $I_{0}$ be defined by the two clauses

[TABLE]

Then the induction axiom is

[TABLE]

The clauses of $I_{0}$ also determine the dual predicate ${}^{\mathrm{co}}\!I_{0}$, which is coinductively given by the closure axiom

[TABLE]

and the coinduction axiom

[TABLE]

We require that both predicates $I_{0}$ and ${}^{\mathrm{co}}\!I_{0}$ have computational content. The data type associated to these clauses is the algebra $\mathbb{L}$ of lists of signed digits. This association is quite canonical: the first constructor $[]\colon\mathbb{L}$ is a witness for the first clause, which does not need any further information. The second constructor $::$ of type $\mathbb{D}\to\mathbb{L}\to\mathbb{L}$ is a witness for the second clause consisting of a signed digit and a witness that $x^{\prime}\in I_{0}$. We refer to [SW12, Section 7.2] for a formal definition of the type of a (co)inductively defined predicate.

The computational content of the clauses are the constructors, of the induction axiom the recursion operator $\mathcal{R}_{\mathbb{L}}^{\tau}$, of the closure axiom the destructor $\mathcal{D}_{\mathbb{L}}$ and of the coinduction axiom the corecursion operator ${}^{\mathrm{co}}\mathcal{R}_{\mathbb{L}}^{\tau}$. All these have been explained in Section 1.2.

2. Division for stream-represented real numbers

2.1. Division for signed digit streams

From a computational point of view, a real number $x$ is best seen as a device producing for a given accuracy $\frac{1}{2^{n}}$ a rational number $a_{n}$ being $\frac{1}{2^{n}}$-close to $x$, i.e., $|a_{n}-x|\leq\frac{1}{2^{n}}$. For simplicity we again restrict ourselves to real numbers in the interval $[-1,1]$ (rather than $[-2^{n},2^{n}]$), and to dyadic rationals $\sum_{n<m}\frac{d_{n}}{2^{n+1}}$ ($d_{n}\in\{1,\bar{1}\}$).

Clearly we can represent real numbers (in $[-1,1]$) as streams of $1,\bar{1}$. Now when doing arithmetic operations on such streams the problem of “productivity” arises: suppose we want to add the two streams $\bar{1}111\dots$ and $1\bar{1}\bar{1}\bar{1}\dots$. Then the first digit of the output stream will only be known after we have checked the two input streams long enough, but there is no bound how far we have to look. The well-known cure for this problem is to add a delay digit [math] and work with signed digits $\sum_{n<m}\frac{d_{n}}{2^{n+1}}$, now with $d_{n}\in\{1,0,\bar{1}\}$. We have a lot of redundancy here (for instance $\bar{1}1$ and $0\bar{1}$ both denote $-\frac{1}{4}$), but this is not a serious problem.

Since [math] as real number is represented by the stream consisting of the digit [math] only, we can simplify our example by removing the nullary clause from the inductive definition of $I_{0}$, and define $I$ and ${}^{\mathrm{co}}\!I$ accordingly. We only need ${}^{\mathrm{co}}\!I$, coinductively defined by the closure axiom

[TABLE]

Therefore, the coinduction axiom is

[TABLE]

The canonically associated data type then becomes the algebra $\mathbb{S}$ given by a single binary constructor of type $\mathbb{D}\to\mathbb{S}\to\mathbb{S}$, again denoted by $::$ (infix). Note that we do not require that $T_{\mathbb{S}}u$ holds for any $u$. Objects $u\in{}^{\mathrm{co}}T_{\mathbb{S}}$ are called streams of signed digits.

The computational content of the closure axiom (1) now is the destructor $\mathcal{D}_{\mathbb{S}}$ of type $\mathbb{S}\to\mathbb{D}\times\mathbb{S}$, defined by

[TABLE]

For the coinduction axiom (2) we have the corecursion operator ${}^{\mathrm{co}}\mathcal{R}_{\mathbb{S}}^{\tau}$ of type $\tau\to(\tau\to\mathbb{D}\times(\mathbb{S}+\tau))\to\mathbb{S}$. Note that $\mathbb{D}\times(\mathbb{S}+\tau)$ appears since $\mathbb{S}$ has the a single constructor of type $\mathbb{D}\to\mathbb{S}\to\mathbb{S}$. The meaning of ${}^{\mathrm{co}}\mathcal{R}_{\mathbb{S}}^{\tau}$ is determined by a (non-terminating) computation rule similar to the one for ${}^{\mathrm{co}}\mathcal{R}_{\mathbb{L}}^{\tau}$ (see Section 1.2), with the first case left out.

Our goal in this section is to prove that $[-1,1]$ is closed under division under some conditions, w.r.t. the representation of reals as signed digit streams. For division $\frac{x}{y}$ we clearly need a restriction on the denominator $y$ to stay in the interval $[-1,1]$, and must assume that $|y|$ is strictly positive. For simplicity we assume $\frac{1}{4}\leq y$; this can easily be extended to the case $2^{-p}\leq y$ (using induction on $p$ and Lemma 3 below). The main idea of the algorithm and also of the proof, which is inspired by [CG06], consists in three representations of $\frac{x}{y}$:

[TABLE]

where

[TABLE]

Depending on what we know about $x$ we choose one of these representations of $\frac{x}{y}$ to obtain its first digit. This will give us a corecursive definition of $\frac{x}{y}$.

As we see in the representation of $\frac{x}{y}$, we will use that ${}^{\mathrm{co}}\!I$ is closed under the average:

Theorem 1**.**

The average of two real numbers $x,y$ in ${}^{\mathrm{co}}\!I$ is in ${}^{\mathrm{co}}\!I$:

[TABLE]

Proof 2.1**.**

The proof in [Ber09, BMST16] can be adapted to the present setting with concrete rather than abstract reals.

The term extracted from this proof corresponds to an algorithm transforming stream representations of $x$ and $y$ into a stream representation of their average $\frac{x+y}{2}$. For the first $n$ digits in the representation of $\frac{x+y}{2}$ one needs the first $n+1$ digits in the representations of $x$ and $y$.

Lemma 2**.**

${}^{\mathrm{co}}\!I$ is closed under shifting a real $x\leq 0$ ($x\geq 0$) by $+1$ ($-1$):

[TABLE]

Proof 2.2**.**

We only consider the first claim; the second one is proved similarly. Since we want to prove that something is in ${}^{\mathrm{co}}\!I$, the proof must use its introduction axiom given in (2):

[TABLE]

The crucial point is how to choose the competitor predicate $P$. Looking at the formula we want to prove, we take $P:=\{\,x\mid\exists_{y\in{}^{\mathrm{co}}\!I}(y\leq 0\land x=y+1)\,\}$ as competitor predicate. Then we have

[TABLE]

and since ${}^{\mathrm{co}}\!I$ is compatible with the real equality, this implies

[TABLE]

Therefore it suffices to prove the premise of the formula above. Let $x\in P$ be given. Then by definition of $P$ there is $y$ with $y\in{}^{\mathrm{co}}\!I$, $y\leq 0$ and $x=y+1$. From $y\in{}^{\mathrm{co}}\!I$ we know $|y|\leq 1$ and with $y\leq 0$ also $|x|\leq 1$. We need $d\in\mathrm{Sd}$ and $x^{\prime}$ such that

[TABLE]

Again from $y\in{}^{\mathrm{co}}\!I$ we obtain $e\in\mathrm{Sd}$ and $z\in{}^{\mathrm{co}}\!I$ with $y=\frac{e+z}{2}$. We now distinguish cases on $e\in\mathrm{Sd}$.

Case $e=1$. Then $0\geq y=\frac{1+z}{2}\geq\frac{1}{2}-\frac{1}{2}=0$ and hence $x=y+1=1$. Picking $d=1$ and $x^{\prime}=1$ gives the claim. Here we need a lemma CoIOne stating that $1$ is in ${}^{\mathrm{co}}\!I$. The proof of this lemma (by coinduction) is omitted.

Case $e=0$. Pick $d=1$ and $x^{\prime}=z+1$. Then $z=2y\leq 0$ and hence the r.h.s. of the disjunction above holds with $z$ for $y$. Also $x=2y=\frac{1+2y+1}{2}$.

Case $e=-1$. Pick $d=1$ and $x^{\prime}=z$. Then the l.h.s. of the disjunction above holds, and $\frac{d+x^{\prime}}{2}=\frac{1+z}{2}=\frac{-1+z}{2}+1=y+1=x$.

We have formalized this proof in the Minlog222The development described here resides in minlog/examples/analysis, file sddiv.scm proof assistant. Minlog has a tool to extract from the proof a term representing its computational content; it is a term in the theory $\mathrm{TCF}$ described in Section 1.2. The extracted term is displayed as

[u](CoRec ai=>ai)u ([u0][case (DesYprod u0) (s pair u1 -> [case s (SdR -> SdR pair InL cCoIOne) (SdM -> SdR pair InR u1) (SdL -> SdR pair InL u1)])])

Here [u] means lambda abstraction $\lambda_{u}$, and (CoRec ai=>ai) is the corecursion operator ${}^{\mathrm{co}}\mathcal{R}_{\mathbb{S}}^{\tau}$ defined above, where $\tau$ is $\mathbb{S}$ again. The type of ${}^{\mathrm{co}}\mathcal{R}_{\mathbb{S}}^{\mathbb{S}}$ is $\mathbb{S}\to(\mathbb{S}\to\mathbb{D}\times(\mathbb{S}+\mathbb{S}))\to\mathbb{S}$. The first argument of the corecursion operator is the abstracted variable u of type $\mathbb{S}$, and the second ([u0][case …]) is the “step” function, which first destructs its argument u0 into a pair of a signed digit s and another stream u1, and then distinguishes cases on s. In the SdR case the returned pair of type $\mathbb{D}\times(\mathbb{S}+\mathbb{S})$ has SdR again as its left component, and as right component the $\mathrm{InL}$ (left embedding into a sum type) of a certain stream denoted cCoIOne. This is the computational content (hence the “c”) of CoIOne, essentially an infinite sequence of the digit $\mathrm{SdR}$ (written $\vec{1}$ ).

The algorithm represented by the extracted term can be understood as follows. If $s=\mathrm{SdR}$, then $y$ must be non-negative. Hence $y=0$, and a stream-representation of $y+1$ is $\vec{1}$. Here we do not need a corecursive call, and hence the result is $\langle\mathrm{SdR},\mathrm{InL}(\vec{1}\;)\rangle$. The same happens in case $s=\mathrm{SdL}$. Here $y+1$ can be determined easily by changing the first digit from $\mathrm{SdL}$ to $\mathrm{SdR}$ and leaving the tail as it is. Hence the result is $\langle\mathrm{SdR},\mathrm{InL}(u^{\prime})\rangle$. Only in case $s=\mathrm{SdM}$ we have a corecursive call. Here we change the first digit from $\mathrm{SdM}$ to $\mathrm{SdR}$, which however amounts to adding $\frac{1}{2}$ only. Therefore the procedure continues with the tail. Hence the result is $\langle\mathrm{SdR},\mathrm{InR}(u^{\prime})\rangle$. Using the computation rule for ${}^{\mathrm{co}}\mathcal{R}_{\mathbb{S}}^{\mathbb{S}}$ we can now describe the computational content as a function $\texttt{add1}\colon\mathbb{S}\to\mathbb{S}$ defined by

[TABLE]

A similar argument for the second part of the lemma gives $\mathrm{sub1}\colon\mathbb{S}\to\mathbb{S}$ with

[TABLE]

Lemma 3**.**

For $x$ in ${}^{\mathrm{co}}\!I$ with $|x|\leq\frac{1}{2}$ we have $2x$ in ${}^{\mathrm{co}}\!I$:

[TABLE]

Proof 2.3**.**

Let $x\in{}^{\mathrm{co}}\!I$ be given. From the closure axiom (1) for ${}^{\mathrm{co}}\!I$ we obtain $d\in\mathrm{Sd}$ and $x^{\prime}\in{}^{\mathrm{co}}\!I$ such that $x=\frac{d+x^{\prime}}{2}$. We distinguish cases on $d\in\mathrm{Sd}$.

Case $d=1$. Then $x=\frac{1+x^{\prime}}{2}$ and hence $2x=1+x^{\prime}$. Since $|x|\leq\frac{1}{2}$ we have $x^{\prime}\leq 0$. Now the first part of Lemma 2 gives the claim.

Case $d=0$. Then $x=\frac{0+x^{\prime}}{2}$ and hence $2x=x^{\prime}\in{}^{\mathrm{co}}\!I$.

Case $d=-1$. Then $x=\frac{-1+x^{\prime}}{2}$ and hence $2x=-1+x^{\prime}$. Since $|x|\leq\frac{1}{2}$ we have $0\leq x^{\prime}$. Now the second part of Lemma 2 gives the claim.

Using arguments similar to those in the remark after Lemma 2 we can see that the corresponding algorithm can be written as a function $\mathrm{Double}\colon\mathbb{S}\to\mathbb{S}$ with

[TABLE]

where $\mathrm{add1}$ and $\mathrm{sub1}$ are the functions from this remark.

Lemma 4**.**

For $x,y$ in ${}^{\mathrm{co}}\!I$ with $\frac{1}{4}\leq y$, $|x|\leq y$ and $0\leq x$ ($x\leq 0$) we have $2x-y$ ( $2x+y$) in ${}^{\mathrm{co}}\!I$:

[TABLE]

Proof 2.4**.**

In the formulas above instead of $2x\pm y$ we have written $4\frac{x+(\pm y/2)}{2}$ to make Theorem 1 applicable. We also use two lemmas stating that ${}^{\mathrm{co}}\!I$ is closed under $x\mapsto\frac{x}{2}$ and $x\mapsto-x$. To prove the first claim, let $x,y$ in ${}^{\mathrm{co}}\!I$ with $\frac{1}{4}\leq y$, $|x|\leq y$ and $0\leq x$. Then clearly $\frac{-y}{2}\in{}^{\mathrm{co}}\!I$, and $\frac{x+\frac{-y}{2}}{2}\in{}^{\mathrm{co}}\!I$ by Theorem 1. We have

[TABLE]

Hence we can apply Lemma 3 twice and obtain $4\frac{x+\frac{-y}{2}}{2}\in{}^{\mathrm{co}}\!I$. The proof of the second claim is similar.

The computational content of the proofs is $\mathrm{AuxL},\mathrm{AuxR}\colon\mathbb{S}\to\mathbb{S}\to\mathbb{S}$:

[TABLE]

Here $h,-\colon\mathbb{S}\to\mathbb{S}$ represent the computational content of the two lemmas used in the proof; both are proved by coinduction. The function $h$ prepends $\mathrm{SdM}$ to the stream, and $-$ negates all digits:

[TABLE]

Theorem 5**.**

For $x,y$ in ${}^{\mathrm{co}}\!I$ with $\frac{1}{4}\leq y$ and $|x|\leq y$ we have $\frac{x}{y}$ in ${}^{\mathrm{co}}\!I$:

[TABLE]

Proof 2.5**.**

The proof uses coinduction (2) on ${}^{\mathrm{co}}\!I$ with $P:=\{\,z\mid\exists_{x,y\in{}^{\mathrm{co}}\!I}(|x|\leq y\land\frac{1}{4}\leq y\land z=\frac{x}{y})\,\}$. It suffices to prove (2)’s premise for this $P$. Let $x,y,z$ be given with $x,y\in{}^{\mathrm{co}}\!I$, $|x|\leq y$, $\frac{1}{4}\leq y$ and $z=\frac{x}{y}$. From $|x|\leq y$ we have $z\leq 1$. By a trifold application of the closure axiom (1) to $x$ we obtain $d_{1},d_{2},d_{3}\in\mathrm{Sd}$ and $\tilde{x}\in{}^{\mathrm{co}}\!I$ such that $x=\frac{4d_{1}+2d_{2}+d_{3}+\tilde{x}}{8}$ or $x=d_{1}d_{2}d_{3}\tilde{x}$ for short. We now distinguish three cases.

If $x=1d_{2}d_{3}\tilde{x}$, $x=01d_{3}\tilde{x}$ or $x=001\tilde{x}$, then $0\leq x$. Pick $d=1$ and $z^{\prime}=\frac{x^{\prime}}{y}$ with $x^{\prime}=4\frac{x+\frac{-y}{2}}{2}$. Then $x^{\prime}\in{}^{\mathrm{co}}\!I$ by Lemma 4. From (3) we also obtain $|x^{\prime}|\leq y$ and hence $z^{\prime}\in P$. One can easily check that $z=\frac{1+z^{\prime}}{2}$.

If $x=\bar{1}d_{2}d_{3}\tilde{x}$, $x=0\bar{1}d_{3}\tilde{x}$ or $x=00\bar{1}\tilde{x}$, then $x\leq 0$. Pick $d=-1$ and $z^{\prime}=\frac{x^{\prime}}{y}$ with $x^{\prime}=4\frac{x+\frac{y}{2}}{2}$. We can then proceed as in the first case.

The final case is $x=000\tilde{x}$. Then $|x|\leq\frac{1}{8}$; pick $d=0$ and $z^{\prime}=\frac{x^{\prime}}{y}$ with $x^{\prime}=2x$. We obtain $|x^{\prime}|\leq\frac{1}{4}\leq y$ and with Lemma 3 also $x^{\prime}\in{}^{\mathrm{co}}\!I$. Therefore $z^{\prime}\in P$, and $z=\frac{z^{\prime}}{2}$ is easily checked.

The term Minlog extracts is displayed in Figure 3.

The three occurrences of cCoIClosure correspond to the trifold application of the closure axioms (1) to $x$. The seven cases $x=1d_{2}d_{3}\tilde{x}$, $x=01d_{3}\tilde{x}$, $x=001\tilde{x}$, $x=000\tilde{x}$, $x=\bar{1}d_{2}d_{3}\tilde{x}$, $x=0\bar{1}d_{3}\tilde{x}$ and $x=00\bar{1}\tilde{x}$ are clearly visible. In the first three cases SdR corresponds to picking $d=1$ and usage of the $\mathrm{AuxR}$ function from Lemma 4, and similarly in the last three cases SdL corresponds to picking $d=-1$ and usage of $\mathrm{AuxL}$. In the middle case SdM corresponds to $d=0$; there we use the computational content of Lemma 3. We can describe the extracted term by a function $\mathrm{Div}\colon\mathbb{S}\to\mathbb{S}\to\mathbb{S}$ corecursively defined by

[TABLE]

As abbreviation in the case distinction, we have denoted $\mathrm{SdL},\mathrm{SdM}$ and $\mathrm{SdR}$ by $\overline{1},0$ and $1$ and we have omitted the constructor $::$.

We use this description of the extracted term to see how far we have to look into $u$ and $v$ to determine the first $n$ entries of $\mathrm{Div}(u,v)$. To this end we write the above equation as

[TABLE]

where $d(u)$ depends on the first three digits of $u$, and $G(u,v)$ is one of $\mathrm{AuxR}(u,v)$, $\mathrm{Double}(u)$ or $\mathrm{AuxL}(u,v)$, according to the present case. Recall

[TABLE]

By the equations for $-$, $h$, $\mathrm{Av}$ and $\mathrm{Double}$ we see that the first $n$ entries of

[TABLE]

Hence $\mathrm{AuxR}(u,v)$, $\mathrm{AuxL}(u,v)$ and $G(u,v)$ all need at most the first $n+3$ entries of $u$ and $n+2$ entries of $v$. Iterating the above equation for $G$ gives for $\mathrm{Div}(u,v)$ the representation

[TABLE]

Therefore the first $n$ entries of $\mathrm{Div}(u,v)$ depend on at most the first $3n$ entries of $u$ and the first $3n-1$ entries of $v$.

2.2. Division for binary reflected digit streams

In the stream representation of real numbers described in Section 2.1 adjacent dyadics of the same length can differ in many digits:

[TABLE]

A possible cure is to flip after an occurrence of $1$; see Figure 4. The result is called binary reflected (or Gray-) code.

Then two dyadics of the same length are adjacent if and only if they differ in exactly one digit. For instance we now have

[TABLE]

This is a desirable property of stream-coded real numbers.

Again when doing arithmetical operations on Gray code the problem of productivity arises, which is dealt with in a somewhat different way. The idea is to introduce two “modes” when generating the code, and flip from one mode to the other whenever we encounter the digit $1$. More precisely, instead of the predicate $I$ we now use two predicates $G,H$ ($G$ for Gray, $H$ next character) and flip from one to the other after reading $1$. They are defined by simultaneous induction, with clauses

[TABLE]

Here $\mathrm{Psd}$ (for proper signed digit) is the (inductive) predicate consisting of the integers $1,-1$. We require that $\mathrm{Psd}$ has computational content, in the booleans $\mathbb{B}=\{\mathsf{t\kern-1.4ptt},\mathsf{f\kern-1.4ptf}\}$. Note that there are no nullary clauses (as for $I$), since they are not needed. We are only interested in the duals ${}^{\mathrm{co}}\!G,{}^{\mathrm{co}}\!H$, coinductively defined by the simultaneous closure axioms

[TABLE]

and the simultaneous coinduction axioms

[TABLE]

We require that the predicates $G,H$ and therefore ${}^{\mathrm{co}}\!G,{}^{\mathrm{co}}\!H$ as well have computational content, in simultaneously defined algebras $\mathbb{G}$ and $\mathbb{H}$ given by the constructors

[TABLE]

We write $\mathrm{Lr}_{\mathsf{t\kern-0.98ptt}}(u)$ for $\mathrm{Lr}(\mathsf{t\kern-1.4ptt},u)$ and $\mathrm{Lr}_{\mathsf{f\kern-0.98ptf}}(u)$ for $\mathrm{Lr}(\mathsf{f\kern-1.4ptf},u)$, and similarly for $\mathrm{Fin}$. Then $\mathrm{Lr}_{\mathsf{t\kern-0.98ptt}/\mathsf{f\kern-0.98ptf}}$ means left/right, $\mathrm{Fin}_{\mathsf{t\kern-0.98ptt}/\mathsf{f\kern-0.98ptf}}$ means finally left/right. The delay constructors are $\mathrm{U}$ (“undefined”) for $\mathbb{G}$ and $\mathrm{D}$ (“delay”) for $\mathbb{H}$. Figure 5 indicates how these constructors generate Gray code.

Totality $T_{\mathbb{G}}$, $T_{\mathbb{H}}$ and cototality ${}^{\mathrm{co}}T_{\mathbb{G}}$, ${}^{\mathrm{co}}T_{\mathbb{H}}$ can be defined as for $\mathbb{S}$ above. Objects $u\in{}^{\mathrm{co}}T_{\mathbb{G}}$ are called streams in Gray code.

The computational content of the closure axioms (4) are the destructors $\mathcal{D}_{\mathbb{G}}\colon\mathbb{G}\to(\mathbb{B}\times\mathbb{G})+\mathbb{H}$ and $\mathcal{D}_{\mathbb{H}}\colon\mathbb{H}\to(\mathbb{B}\times\mathbb{G})+\mathbb{H}$ defined by

[TABLE]

The computational content of the coinduction axioms (5) are instances of the simultaneous corecursion operators

[TABLE]

with step types

[TABLE]

The type $\mathbb{B}\times(\mathbb{G}+\sigma)+(\mathbb{H}+\tau)$ appears since $\mathbb{G}$ has the two constructors $\mathrm{Lr}\colon\mathbb{B}\to\mathbb{G}\to\mathbb{G}$ and $\mathrm{U}\colon\mathbb{H}\to\mathbb{G}$, and $\mathbb{H}$ has the two constructors $\mathrm{Fin}\colon\mathbb{B}\to\mathbb{G}\to\mathbb{H}$ and $\mathrm{D}\colon\mathbb{H}\to\mathbb{H}$. Omitting the upper indices of ${}^{\mathrm{co}}\mathcal{R}$ the computation rules for the terms ${}^{\mathrm{co}}\mathcal{R}_{\mathbb{G}}sgh$ and ${}^{\mathrm{co}}\mathcal{R}_{\mathbb{H}}tgh$ are

[TABLE]

with $s$ of type $\sigma$ and $t$ of type $\tau$.

Our goal in this section is to prove that $[-1,1]$ is closed under division $\frac{x}{y}$ (for $|x|\leq|y|>0$), w.r.t. the representation of reals in Gray code. We proceed essentially as for the signed digit case. The main difference is that the simultaneous definition of ${}^{\mathrm{co}}\!G$ and ${}^{\mathrm{co}}\!H$ makes it necessary to use simultaneous coinduction.

Theorem 6**.**

The average of two real numbers $x,y$ in ${}^{\mathrm{co}}\!G$ is in ${}^{\mathrm{co}}\!G$:

[TABLE]

Proof 2.6**.**

The proof in [BMST16] can be adapted to the present setting with concrete rather than abstract reals.

Lemma 7**.**

${}^{\mathrm{co}}\!G$ and ${}^{\mathrm{co}}\!H$ are closed under minus:

[TABLE]

Proof 2.7**.**

We prove both claims simultaneously, by coinduction:

[TABLE]

We choose $P:=\{\,x\mid-x\in{}^{\mathrm{co}}\!G\,\}$ and $Q:=\{\,x\mid-x\in{}^{\mathrm{co}}\!H\,\}$. Since ${}^{\mathrm{co}}\!G$ and ${}^{\mathrm{co}}\!H$ are invariant under real equality (also proven by coinduction) we have to prove the two premises. We only consider the first one; the second is proved similarly. Let $x\in P$ be given. The goal is

[TABLE]

From $x\in P$ we get $-x\in{}^{\mathrm{co}}\!G$ and therefore

[TABLE]

by the closure axiom. If the right hand side of this disjunction holds, we are done by definition of $Q$. If the left hand side holds, we have $x=d\frac{x^{\prime}-1}{2}$ for some $d\in\mathrm{Psd}$ and $x^{\prime}\in{}^{\mathrm{co}}\!G$. To get the left hand side of the disjunction in the goal formula, we take $d:=-d$ and $x^{\prime}:=x^{\prime}$.

The function we get from the proof takes a Gray code and flips all $\mathsf{t\kern-1.4ptt}$ to $\mathsf{f\kern-1.4ptf}$ and the other way around. We denote this function by $-$. Then the computation rules are:

[TABLE]

Lemma 8**.**

${}^{\mathrm{co}}\!G$ and ${}^{\mathrm{co}}\!H$ are equivalent:

[TABLE]

Proof 2.8**.**

In the coinduction axiom we choose $P:={}^{\mathrm{co}}\!H$ and $Q:={}^{\mathrm{co}}\!G$ and the conclusion in the coinduction axiom is our goal. Therefore we have to prove the premises of the coinduction axiom. We only consider the first one; the secound one is proved similarly. Let $x\in{}^{\mathrm{co}}\!H$ be given. By the closure axiom of ${}^{\mathrm{co}}\!H$ we have

[TABLE]

If the second part of this disjunction holds, we get directly the second part of the first premise. If the first part of the disjunction holds, we have $x=d\frac{x^{\prime}+1}{2}$ for some $d\in\mathrm{Psd}$ and $x^{\prime}\in{}^{\mathrm{co}}\!G$. Then $x=-d\frac{(-x^{\prime})-1}{2}$ and using Lemma 7 we get the first part of disjunction in the premise.

As computational content we have two functions $\mathrm{ToCoH}\colon\mathbb{G}\to\mathbb{H}$ and $\mathrm{ToCoG}\colon\mathbb{H}\to\mathbb{G}$, with computation rules

[TABLE]

Note that no corecursive call is involved. We denote $\mathrm{ToCoG}(v)$, $\mathrm{ToCoH}(u)$ by $\tilde{v}$, $\tilde{u}$, respectively.

We show that ${}^{\mathrm{co}}\!G$ is closed under shifting a real $x\leq 0$ ($x\geq 0$) by $+1$ ($-1$):

[TABLE]

The proof is by coinduction, simultaneously with the same proposition for ${}^{\mathrm{co}}\!H$. For the coinduction proof it is helpful to reformulate the claim in such a way that the conclusion has the form $x\in{}^{\mathrm{co}}\!G$:

Lemma 9**.**

[TABLE]

Proof 2.9**.**

We use the introduction axiom for ${}^{\mathrm{co}}\!G$ and ${}^{\mathrm{co}}\!H$, and simultaneously prove

[TABLE]

The competitor predicates are

[TABLE]

It suffices to prove the premises of the coinduction axiom for these $P$, $Q$. We only consider the first part; the second is proved similarly. Let $x\in P$ be given. Then we have $y$ with $y\in{}^{\mathrm{co}}\!G$, $y\leq 0$ and $x=y+1\lor x=-(y+1)$. From $y\in{}^{\mathrm{co}}\!G$ we know $|y|\leq 1$ and with $y\leq 0$ also $|x|\leq 1$. We need to prove the disjunction

[TABLE]

From $y\in{}^{\mathrm{co}}\!G$ we obtain either (i) $e\in\mathrm{Psd}$, $z\in{}^{\mathrm{co}}\!G$ with $y=-e\frac{z-1}{2}$ or else (ii) $z\in{}^{\mathrm{co}}\!H$ with $y=\frac{z}{2}$. In case (i) we have $|z|\leq 1$ since $z\in{}^{\mathrm{co}}\!G$. We distinguish cases on $e\in\mathrm{Psd}$, and use Lemma 7.

Case $e=1$. Then $0\geq y=-\frac{z-1}{2}\geq-\frac{1}{2}+\frac{1}{2}=0$, hence $y=0$. If $x=y+1$, take $x=1$ and go for the l.h.s. of the disjunction $D$. Picking $d=1$ and $x^{\prime}=-1$ gives the claim (since $-1\in{}^{\mathrm{co}}\!G$). If $x=-(y+1)$, take $x=-1$ and go for the l.h.s. of the disjunction $D$. Picking $d=-1$ and $x^{\prime}=-1$ gives the claim (since $-1\in{}^{\mathrm{co}}\!G$).

Case $e=-1$. If $x=y+1$, go for the l.h.s. of the disjunction $D$, picking $d=1$ and $x^{\prime}=-z$. Then $x=y+1=\frac{z-1}{2}+1=\frac{z+1}{2}=-\frac{-z-1}{2}$. If $x=-(y+1)$, go for the l.h.s. of the disjunction $D$, picking $d=-1$ and $x^{\prime}=-z$. Then $x=-(y+1)=-\frac{z-1}{2}-1=\frac{-z+1}{2}-1=\frac{-z-1}{2}$.

In case (ii) we have $|z|\leq 1$ (since $z\in{}^{\mathrm{co}}\!H$) and $z\leq 0$ (since $y=\frac{z}{2}$ and $y\leq 0$). Hence $|z+1|\leq 1$. If $x=y+1$, go for the l.h.s. of the disjunction $D$, picking $d=1$ and $x^{\prime}=-(z+1)$. Then $-(z+1)\in P$ (since also $z\in{}^{\mathrm{co}}\!G$ and $z\leq 0$), and $x=y+1=\frac{z}{2}+1=\frac{z+2}{2}=-\frac{-(z+1)-1}{2}$. If $x=-(y+1)$, go for the l.h.s. of the disjunction $D$, with $d=-1$ and $x^{\prime}=-(z+1)$. Then again $-(z+1)\in P$ and $x=-(y+1)=\frac{-(z+1)-1}{2}$.

As computational content of a formalization of this proof Minlog returns a term involving simultaneous corecursion. The corresponding algorithm can be described as a pair of two functions $\mathrm{shG}\colon\mathbb{G}\to\mathbb{B}\to\mathbb{G}$ and $\mathrm{shH}\colon\mathbb{H}\to\mathbb{B}\to\mathbb{H}$ defined by

[TABLE]

Recall that $v\mapsto\tilde{v}$ is the function extracted from the proof of Lemma 8 stating that ${}^{\mathrm{co}}\!G$ and ${}^{\mathrm{co}}\!H$ are equivalent. If $b=\mathsf{t\kern-1.4ptt}$, we have computational content of the first part of the lemma. If $b=\mathsf{f\kern-1.4ptf}$, we have the second part.

Lemma 10**.**

For $x$ in ${}^{\mathrm{co}}\!G$ with $|x|\leq\frac{1}{2}$ we have $2x$ in ${}^{\mathrm{co}}\!G$:

[TABLE]

Proof 2.10**.**

Let $x\in{}^{\mathrm{co}}\!G$ be given. From the closure axiom for ${}^{\mathrm{co}}\!G$ we obtain either (i) $d\in\mathrm{Psd}$, $x^{\prime}\in{}^{\mathrm{co}}\!G$ with $x=-d\frac{x^{\prime}-1}{2}$, or else (ii) $x^{\prime}\in{}^{\mathrm{co}}\!H$ with $x=\frac{x^{\prime}}{2}$. In case (i) we distinguish cases on $d\in\mathrm{Psd}$. In case $d=1$ we obtain $x=\frac{-x^{\prime}+1}{2}$ and hence $2x=-x^{\prime}+1$. Since $|x|\leq\frac{1}{2}$ we have $x^{\prime}\leq 0$. Now the first part of Lemma 9 gives the claim. The case $d=-1$ is similar, using the second part of Lemma 9. In case (ii) we have $2x=x^{\prime}$, hence the goal $2x\in{}^{\mathrm{co}}\!G$ follows from the equivalence of ${}^{\mathrm{co}}\!G$ and ${}^{\mathrm{co}}\!H$.

Using arguments similar to those in the remark after Lemma 9 we can see that the corresponding algorithm can be written as a function $\mathrm{Double}\colon\mathbb{G}\to\mathbb{G}$ with

[TABLE]

where $\mathrm{shG}$ and $v\mapsto\tilde{v}$ are the functions from this remark.

Parallel to Lemma 4 we can now prove

Lemma 11**.**

For $x,y$ in ${}^{\mathrm{co}}\!G$ with $\frac{1}{4}\leq y$, $|x|\leq y$ and $0\leq x$ ($x\leq 0$) we have $2x-y$ ( $2x+y$) in ${}^{\mathrm{co}}\!G$:

[TABLE]

Proof 2.11**.**

We only consider the first claim, and again use Theorem 6 on the average. In the formulas above instead of $2x\pm y$ we have written $4\frac{x+(\pm y/2)}{2}$ to make Theorem 6 applicable. One can see easily that ${}^{\mathrm{co}}\!G$ is closed under $x\mapsto\frac{x}{2}$. Formally, this is proved by coinduction, and the corresponding algorithm is given by a function $h\colon\mathbb{G}\to\mathbb{G}$. To prove the first claim, let $x,y$ in ${}^{\mathrm{co}}\!G$ with $\frac{1}{4}\leq y$, $|x|\leq y$ and $0\leq x$. Then clearly $\frac{-y}{2}\in{}^{\mathrm{co}}\!G$, and $\frac{x+\frac{-y}{2}}{2}\in{}^{\mathrm{co}}\!G$ by Theorem 6. We have the same estimate (3) as in the proof of Lemma 4; hence we can apply Lemma 10 twice and obtain $4\frac{x+\frac{-y}{2}}{2}\in{}^{\mathrm{co}}\!G$. The proof of the second claim is similar.

The computational content are functions $\mathrm{AuxL},\mathrm{AuxR}\colon\mathbb{G}\to\mathbb{G}\to\mathbb{G}$ with

[TABLE]

Parallel to the essential part of Theorem 5 we can now prove that division by $y$ satisfies to closure axiom for ${}^{\mathrm{co}}\!I$:

Theorem 12**.**

For $x,y$ in ${}^{\mathrm{co}}\!G$ with $\frac{1}{4}\leq y$ and $|x|\leq y$ we find a signed digit $d$ such that $2x=x^{\prime}+yd$ for some $x^{\prime}\in{}^{\mathrm{co}}\!G$ with $|x^{\prime}|\leq y$:

[TABLE]

Proof 2.12**.**

We proceed as for Theorem 5, now using Lemma 11. The proof uses a trifold application of the coinduction axioms for ${}^{\mathrm{co}}\!G$ and ${}^{\mathrm{co}}\!H$ to obtain the first three digits.

The computational content is a function $f\colon\mathbb{G}\to\mathbb{G}\to\mathbb{D}\times\mathbb{G}$ defined by

[TABLE]

Corollary 13**.**

For $x,y$ in ${}^{\mathrm{co}}\!G$ with $\frac{1}{4}\leq y$ and $|x|\leq y$ we have $\frac{x}{y}$ in ${}^{\mathrm{co}}\!G$:

[TABLE]

Proof 2.13**.**

By coinduction, simultaneously with the same formula where ${}^{\mathrm{co}}\!G$ is replaced by ${}^{\mathrm{co}}\!H$. Theorem 12 is used in both cases of the simultaneous coinduction. The extracted term could be analyzed in a similar way as in the remark after Theorem 5.

2.3. Translation to Haskell

The terms extracted from Theorem 5 and Corollary 13 can be translated into Scheme or Haskell programs. Because of the presence of corecursion operators in the extracted terms the lazy evaluation of Haskell is more appropriate. As tests we have run (in ghci with time measuring by :set +s) the signed digit division files333sddiv.scm and graydiv.scm residing in minlog/examples/analysis on approximations of $\frac{1}{3}$ and $\frac{1}{2}$. To return the first 19 digits of the result of dividing $\frac{1001}{3001}$ by $\frac{10001}{20001}$ took about 0.04 seconds in the signed digit case and about 0.06 seconds in the Gray case.

In the following table we see how the runtime increases if we increase the number of signed digits in the output. Of course, this depends on the used computer, but instead of the concrete numbers we are interested in the scale of the runtime.

In the remark after Theorem 5 we have shown that the look-ahead of the input is linear in the digits of the output, i.e., we need at most the first $3n$ entries of $u$ and $v$ to compute the first $n$ entries of $\text{Div}(u,v)$. But here we see that the runtime is clearly not linear. This is not surprising because in this remark we had the representation

[TABLE]

of $\text{Div}(u,v)$. Therefore, for the first $n$ digits, we have to compute

[TABLE]

and we have to read the first $3n$ digits of $u$ and $v$ and operate on them $n-1$ times. We see that $n$ occurs twice in the calculation and hence the runtime has to be at least quadratic in the numbers of digits of the output. We also see this in the table above:

If we compare, for example, the runtimes for 100, 1000 and 10000 digits, we see that a multiplication of the numbers of digits by 10 causes a multiplication of the runtime by approximately 100. Therefore the runtime seems to be approximately quadratic in the number of computed digits.

3. Soundness

We have extracted terms from the two proofs of Theorem 5 and Corollary 13 and tested them on numerical examples. Now we want to prove that these terms are correct, in the sense that they “satisfy their specification”. We interpret this statement in the sense of Kolmogorov [Kol32]: a (c.r.) formula should be viewed as a problem asking for a solution. But what is a solution of a formula/problem $A$? We use Kreisel’s notion of (modified) realizability and understand “the term $t$ is a solution of $A$” as $t\mathrel{\mathbf{r}}A$ ($t$ realizes $A$). This definition is reviewed in Section 3.1. Then we go on and prove in Section 3.2 that for every proof $M$ of a c.r. formula $A$ its extracted term $\mathrm{et}(M)$ realizes $A$, i.e., $\mathrm{et}(M)\mathrel{\mathbf{r}}A$. In this proof we make use of “invariance axioms”444They are called (A-r) “to assert is to realize” in [Fef79]. stating that every c.r. formula is invariant under realizability, formally $A\leftrightarrow\exists_{z}(z\mathrel{\mathbf{r}}A)$. Finally in Section 3.3 we report on a Minlog tool automatically generating such soundness proofs.

3.1. Realizers

Recall that computational content arises from (co)inductive predicates only. Therefore we begin with a definition of what it means to be a realizer of such a predicate. We restrict ourselves to define realizers for special instances only; a general treatment can be found in [SW12, p.334].

Consider the definition of the inductive predicate $I_{0}$ in Section 1.4. By another (n.c.) inductive predicate $I_{0}^{\textbf{r}}$ of arity $(\mathbb{R},\mathbb{L})$ we can express that a list $u$ witnesses (“realizes”) that the real $x$ is in $I_{0}$. We write $u\mathrel{\mathbf{r}}I_{0}x$ ($u$ is a realizer of $x\in I_{0}$) for $(x,u)\in I_{0}^{\textbf{r}}$. The predicate $I_{0}^{\textbf{r}}$ is required to be non-computational, since in $(x,u)\in I_{0}^{\textbf{r}}$ we already have a realizer $u$. $I_{0}^{\textbf{r}}$ is inductively defined by the two clauses

[TABLE]

and the induction axiom

[TABLE]

where $s_{d}$ is the signed digit corresponding to $d\in\mathrm{Sd}$ [SW12, p.334]). We write $u\mathrel{\mathbf{r}}I_{0}x$ ($u$ is a realizer of $x\in I_{0}$) for $(x,u)\in I_{0}^{\textbf{r}}$. The predicate $I_{0}^{\textbf{r}}$ is required to be non-computational, since in $(x,u)\in I_{0}^{\textbf{r}}$ we already have a realizer $u$. $I_{0}^{\textbf{r}}$ is inductively defined by the two clauses

[TABLE]

and the induction axiom

[TABLE]

where $s_{d}$ is the signed digit corresponding to $d\in\mathrm{Sd}$. Similarly we coinductively define the n.c. predicate $({}^{\mathrm{co}}\!I_{0})^{\textbf{r}}$ of arity $(\mathbb{R},\mathbb{L})$ to express that a list $u$ witnesses (“realizes”) that the real $x$ is in ${}^{\mathrm{co}}\!I_{0}$. We write $u\mathrel{\mathbf{r}}{}^{\mathrm{co}}\!I_{0}x$ ($u$ is a realizer of $x\in{}^{\mathrm{co}}\!I_{0}$) for $(x,u)\in{}^{\mathrm{co}}\!I_{0}^{\textbf{r}}$. The closure axiom is

[TABLE]

and the coinduction axiom

[TABLE]

3.2. Soundness theorem

A formula or predicate is called $\mathrel{\mathbf{r}}$-free if it does not contain any of the $I^{\textbf{r}}$- or ${}^{\mathrm{co}}\!I^{\textbf{r}}$-predicates. A proof $M$ is called $\mathrel{\mathbf{r}}$-free if it contains $\mathrel{\mathbf{r}}$-free formulas only.

Theorem 14** (Soundness).**

Let $M$ be an $\mathrel{\mathbf{r}}$-free proof of a formula $A$ from assumptions $u_{i}\colon C_{i}$ ( $i<n$). Then we can derive

[TABLE]

from assumptions

[TABLE]

Proof 3.1**.**

By induction on $M$. In the base case we have to prove that the extracted terms of $I^{\pm}$, ${}^{\mathrm{co}}\!I^{\pm}$ realize the respective axioms. The proofs in [SW12, Sections 7.2.8 and 7.2.10] can be adapted to the present situation. The step cases are easier; we only consider the ones where invariance axioms are used.

Case $(\lambda_{u^{A}}M^{B})^{A\to B}$ with $A$ c.r. and $B$ n.c. We need a derivation of $A\to B$. By induction hypothesis we have a derivation of $B$ from $z\mathrel{\mathbf{r}}A$. Using the invariance axiom $A\to\exists_{z}(z\mathrel{\mathbf{r}}A)$ we obtain the required derivation of $B$ from $A$ as follows.

[TABLE]

Case $(M^{A\to B}N^{A})^{B}$ with $A$ c.r. and $B$ n.c. The goal is to find a derivation of $B$. By induction hypothesis we have derivations of $A\to B$ and of $\mathrm{et}(N)\mathrel{\mathbf{r}}A$. Now using the invariance axiom $\forall_{z}(z\mathrel{\mathbf{r}}A\to A)$ we obtain the required derivation of $B$ by $\to^{-}$ from the derivation of $A\to B$ and

[TABLE]

3.3. Formal soundness proofs for real division algorithms

In the files sddiv.scm, graydiv.scm the Minlog command add-sound has been applied repeatedly to c.r. theorems to automatically generate the corresponding soundness proofs.

4. Conclusion

Recall that our goal was the extraction of computational content from proofs in constructive analysis. Although these proofs work with some standard representation of real numbers, the technique used here makes it possible to extract from such proofs terms describing algorithms which operate on different representations of real numbers, for instance streams of signed digits or Gray code. Moreover, formal proofs of their correctness can be generated automatically.

As future work it is planned to extend the present approach to problems involving e.g. the exponential function and more generally power series. A promising application area would be Euler’s existence proof of solutions for ordinary differential equations satisfying a Lipschitz condition.

Acknowledgment

We thank Tatsuji Kawai, Nils Köpp, Kenji Miyamoto, Hideki Tsuiki and three anonymous referees for helpful comments.