Plaintext
Logical Methods in Computer Science
Volume 17, Issue 2, 2021, pp. 7:1–7:27 Submitted May 01, 2019
https://lmcs.episciences.org/ Published Apr. 20, 2021
LOGIC FOR EXACT REAL ARITHMETIC
HELMUT SCHWICHTENBERG a AND FRANZISKUS WIESNET b
a
Mathematisches Institut, LMU, München
e-mail address: schwicht@math.lmu.de
b
Mathematisches Institut, LMU, München and Dipartimento di Matematica, Università degli Studi
di Trento
e-mail address: franziskus.wiesnet@unitn.it
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.
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 0. 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.
(I) Formulate (using corecursion) the algorithm in the term language of a suitable theory,
and then formally prove that this term satifies the specification;
(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
Key words and phrases: signed digit code, real number computation, inductive and coinductive definitions,
corecursion, program extraction, realizability.
This project has received funding from the European Union’s 2020 research and innovation programme
under the Marie Sklodowska-Curie grant agreement No 731143. The second author is a Marie Sklodowska-
Curie fellow of the Istituto Nazionale di Alta Matematica.
l LOGICAL METHODS
IN COMPUTER SCIENCE DOI:10.23638/LMCS-17(2:7)2021
©
CC
H. Schwichtenberg and F.Wiesnet
Creative Commons
7:2 H. Schwichtenberg and F.Wiesnet Vol. 17:2
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 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.
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:3
1. Preliminaries
We informally describe a formal theory 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 ≤-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 TCF.
1.1. Objects. Base type objects of our theory are determined by the constructors of (free)
algebras. More precisely, let α, β, ξ be type variables.
Definition. Constructor types κ have the form
~ → (ξ)i<n → ξ
α
with all type variables αi distinct from each other and from ξ. 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 ξ, and a recursive argument type otherwise. A constructor
type κ is nullary if it has no recursive argument types. We call
ι := µξ ~κ (~κ not empty)
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.
7:4 H. Schwichtenberg and F.Wiesnet Vol. 17:2
Examples. We list some algebra forms without parameters, with standard names for the
constructors added to each constructor type.
U := µξ (Dummy : ξ) (unit),
B := µξ (tt : ξ, ff : ξ) (booleans),
D := µξ (SdR : ξ, SdM : ξ, SdL : ξ) (signed digits, for 1, 0, −1),
N := µξ (0 : ξ, S : ξ → ξ) (natural numbers, unary),
P := µξ (1 : ξ, S0 : ξ → ξ, S1 : ξ → ξ) (positive numbers, binary),
Z := µξ (0Z : ξ, IntP : P → ξ, IntN : P → ξ) (integers),
Y := µξ (− : ξ, Branch : ξ → ξ → ξ) (binary trees).
Algebra forms with type parameters are
I(α) := µξ (Id : α → ξ) (identity),
L(α) := µξ (Nil : ξ, Cons : α → ξ → ξ) (lists),
S(α) := µξ (SCons : α → ξ → ξ) (streams),
α × β := µξ (Pair : α → β → ξ) (product),
α + β := µξ (InL : α → ξ, InR : β → ξ) (sum).
The default name for the i-th constructor of an algebra form is Ci .
Definition (Type).
ρ, σ, τ ::= α | ι(~
ρ ) | τ → σ,
where ι is an algebra form with α ~ its parameter type variables, and ι(~ ρ ) the result of
substituting the (already generated) types ρ
~ for α
~ . Types of the form ι(~
ρ ) are called algebras.
An algebra is closed if it has no type variables. The level of a type is defined by
lev(α) := 0,
lev(ι(~
ρ )) := max(lev(~
ρ )),
lev(τ → σ) := max(lev(σ), 1 + lev(τ )).
Base types are types of level 0, and a higher type has level at least 1.
Examples. 1. L(α), L(L(α)), α × β are algebras.
2. L(L(N)), N + B, Q := Z × P are closed base types.
3. (N → Q) × (P → N) is a closed algebra of level 1.
There can be many equivalent ways to define a particular type. For instance, we could
take U + U to be the type of booleans, L(U) to be the type of natural numbers, and L(B) to
be the type of positive binary numbers.
We introduce the base type objects by example only, for N, Y, L(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 ∗ which carries no information.
Examples in the algebra Y of binary trees are
Branch(−, Branch(−, −)) Branch(−, Branch(∗, −))
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:5
.
• ..
SSS0
@
@
SS0 • @• SSS∗
@
@
S0 • @• SS∗
@
@
0 • @• S∗
Figure 1: Tokens and entailment for N
or pictorially
− − ∗ −
− @
@ − @
@
H H
H
H H
H
For tokens we have obvious concepts called consistency (↑) and entailment (`). For instance
∗ ∗ ∗ ∗
− − − @
@ − ∗ − @
@
HH HH HH HH
H 6↑ H but H ↑ H
Examples for entailment in Y are
− ∗ ∗ − − −
H H H
{ HH , H
H } `Y H
H
and also
∗ − ∗ ∗
∗ @
@ ∗ @
@ ∗ ∗
HH HH HH
H `Y H
and H
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 (∗) with
a distinguished occurrence of ∗ there is another token in x where this occurrence of ∗ is
replaced by a constructor expression with only ∗’s as arguments. We call x total if it is
cototal and finite.
The tokens of N are shown in Figure 1. For tokens a, b we have {a} ` b if and only if
there is a path from a (up) to b (down). There is exactly one cototal object, consisting of
S∗, SS∗, SSS∗ . . . . Note that ∗ is not a token; the “bottom” object is the empty set.
Examples of more interesting objects in Y are
7:6 H. Schwichtenberg and F.Wiesnet Vol. 17:2
(1) R := closure (under entailment) of all tokens of the form
− ∗
−
−
−
(2) L is defined similarly
(3) L ∪ R
(4) 12 := closure of all tokens of the form
−∗
− ∗ −
− −
−
(5) Closure of
− −
− @
@
HH
H
(6) Closure of
∗ −
− @
@
HH
H
Among these are
(1) − (4) cototal objects,
(5) a total object,
(6) a general object.
Finally we consider the algebra L(B) of lists of booleans, to represent finite or infinite
paths. Tokens in L(B) are for instance (writing :: for Cons)
{ff} :: {ff} :: {tt} :: Nil abbreviated RRL[]
Consistency in L(B):
RL[] 6↑ RRL∗, RR∗ ↑ RRL∗
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:7
Entailment in L(B):
RRL∗ ` RR∗, R ∗ (and also e.g. RR∅∗),
RRL[] ` RRL∗, RR∗, R∗
Objects in L(B):
total: Closure of RLRR[]
cototal: Closure of all RLRR . . . R∗ and all RRLL . . . L∗
general: Closure of RLRR∗
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 λ-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 L := L(D) of lists of signed digits are
Terms are built from (typed) variables, constructors and (equationally) defined constants
by λ-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
L := L(D) of lists of signed digits are
RτL : L → τ → (D → L → τ → τ ) → τ (recursion operator),
DL : L → U + (D × L) (destructor),
co
RτL : τ → (τ → U + (D × (L + τ ))) → L (corecursion operator).
RτL takes a recursion argument ` : L, an initial value z : τ and a “step” argument f : (D →
L → τ → τ ) operating according to the structure of the given list. The meaning of RτL is
determined by the computation rules
RτL ([], z, f ) = z, RτL (s :: `, z, f ) = f (s, `, RτL (`, z, f )).
DL operates by disassembling the given list ` : L into its head and tail. The computation
rules are
DL ([]) = InL(Dummy), DL (s :: `) = InRhs, `i.
For co RτL the “step” f : (τ → U + (D × (L + τ ))) operates by inspection (or observation) of
its argument z : τ . More precisely, the meaning of co RτL is given by the (non-terminating)
computation rule
[]
if f z ≡ InL(Dummy),
co τ
RL zf = s :: u if f z ≡ InRhs, InL(u)i,
s :: RL z f if f z ≡ InRhs, InR(z 0 )i.
co τ 0
We use ≡ for Leibniz equality (inductively defined by the clause ∀z (z ≡ z)).
Predicates are either (co)inductively defined or of the form { ~x | A } where A is a formula.
We identify { ~x | A(~x ) }~t with A(~t ). Formulas are given as atomic formulas P ~t where P is a
predicate and ~t are terms, or else as A → B or ∀x A where A and B are already formulas.
The formulas ∃x A, A ∧ B and A ∨ B technically are inductively defined (nullary) predicates.
7:8 H. Schwichtenberg and F.Wiesnet Vol. 17:2
An inductively defined predicate I is given by clauses of the form
Ii+ : ∀~xi ((Aij (I))j<ni → I~ti ),
for i ∈ {0, . . . , k − 1}, k > 0 and ni ≥ 0, where I only occurs strictly positive in each Aij (I)
and x~i contains all free variables of Aij (I) and ~ti . The clauses are called introduction axioms
of I.
An example is the totality predicate TL . Its clauses are
(TL )+
0 : TL [], (TL )+
1 : ∀s,` (TD s → TL ` → TL s :: `),
where TD is the totality predicate for the three-element algebra D of signed digits, defined
by the three clauses TD s for s a signed digit.
Intuitively, an inductively defined predicate is the smallest (w.r.t. ⊆) predicate fulfilling
its clauses. This is expressed by its elimination axiom:
I − : (∀~xi ((Aij (I ∩ X))j<ni → X~ti ))i<k → I ⊆ X,
where X can be any predicate with the same arity as I. The axiom I − is also called induction
axiom. For example,
TL− : X[] → ∀s,` (TD s → TL ` → X` → X(s :: `)) → TL ⊆ X.
Let I be an inductively defined predicate given by its clauses (Ii+ )i<k , and assume that
there are recursive calls in some clauses. To every such I we associate a “companion” coI
and call it a coinductively defined predicate. The elimination (or closure) axiom coI − of the
coinductively defined predicate says that if coI~x holds, then it comes from one of the clauses:
co −
I : ∀~x (coI~x → Aij (coI) ∧ ~x ≡ ~ti )).
W
W V
V
∃~xi (
i<k j<ni
In words: if coI~x holds, then there is at least one clause Ii+ whose premises (Aij (coI))j<ni
(with coI instead of I) are fulfilled and whose conclusion is coI~x up to Leibniz equality. For
example, the co-predicate associated with TL is cototality co TL . Its elimination axiom is
co
TL− : co
TL ` → ` ≡ [] ∨ ∃s,`0 (TD s ∧ co TL `0 ∧ ` ≡ s :: `0 ).
The introduction (or coinduction or greatest-fixed-point) axiom coI + of coI says that coI
is the greatest predicate such that
co +
Aij (coI ∪ X) ∧ ~x ≡ ~ti )) → X ⊆ coI.
W
W V
V
I : ∀~x (X~x → ∃~xi (
i<k j<ni
This means that any other “competitor” predicate X satisfying the same closure property is
below coI. For example,
co
TL+ : ∀` (X` → ` ≡ [] ∨ ∃s,`0 (TD s ∧ (co TL `0 ∨ X`0 ) ∧ ` ≡ s :: `0 ) → X ⊆ co TL .
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:9
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 ιI . A “witness” that I~t or coI~t holds has type ι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 TL or co TL is L. A formula A built from atomic formulas by →, ∀ is c.r. if
its final conclusion is. The type τ (A) is defined by
τ (P ~t ) := τ (P ),
(
τ (A) → τ (B) if A is c.r.
τ (A → B) :=
τ (B) if A is n.c.
τ (∀x A) := τ (A).
Recall that ∃x A, A ∧ B and A ∨ B technically are inductively defined (nullary) predicates. If
they are c.r., their types are τ (∃x A) := τ (A); τ (A ∧ B) := τ (A) × τ (B), τ (A), τ (B) depending
on the c.r./n.c. status of A, B; τ (A ∨ B) := τ (A) + τ (B), τ (A) + U, U + τ (B), B depending
on the c.r./n.c. status of A, B.
Let M be a proof in TCF of a c.r. formula A. We define its extracted term et(M ), of
type τ (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
λ-abstraction and application:
τ (A)
et(uA ) := zuτ (A) (zu uniquely associated with uA ),
(
λzu et(M ) if A is c.r.
et((λuA M B )A→B ) :=
et(M ) if A is n.c.
(
et(M )et(N ) if A is c.r.
et((M A→B N A )B ) :=
et(M ) if A is n.c.
et((λx M A )∀x A ) := et(M ),
∀x A(x) A(t)
et((M t) ) := et(M ).
It remains to define extracted terms for the axioms. Consider a (c.r.) inductively defined
predicate I. For its introduction and elimination axioms define et(Ii+ ) := Ci and et(I − ) := R,
where both the constructor Ci and the recursion operator R refer to the algebra ιI associated
with I. For the closure and greatest-fixed-point axioms of coI define et(coI − ) := D and
et(coI + ) := co R, where both the destructor D and the corecursion operator co R again refer
to the algebra ιI associated with I.
1.4. Real numbers. Rational numbers Q are defined by Q := Z × P, where the pair of
k : Z and p : P is denoted by kp . 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
(N → Q) × (P → 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
7:10 H. Schwichtenberg and F.Wiesnet Vol. 17:2
a Cauchy sequence (an )n∈N of rationals with the second component M as modulus, i.e.,
1
|an − am | ≤ p for n, m ≥ M (p).
2
We write R for this predicate. For real numbers we can define the arithmetic functions +,
−, · and the inverse and also the absolute value | · |. 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
Minlog1.
An important predicate on the real numbers is real equality: we define x ≤ y by
1
aM (p+1) ≤ bN (p+1) + p for all p ∈ P
2
and real equality x = y by x ≤ y ∧ y ≤ 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∈N and the constant
modulus (0)p∈P .
We use variable names
x, y for real numbers,
a, b, c for rational numbers,
d, e, k, j, i for integers,
s for signed digits,
u, v for lists (and streams) of signed digits.
Let TZnc
be the n.c. version of the totality predicate for Z, and similarly for other types. Let
Sd be the (formally inductive) predicate consisting of the integers 1, 0, −1, i.e., Sd is given
by the three clauses 1 ∈ Sd, 0 ∈ Sd and −1 ∈ Sd. We require that Sd has computational
content (in the three-element algebra D), and write
∀d∈Sd A(d) for ∀ ˆ(dˆ ∈ T nc → dˆ ∈ Sd → A(d))
d Z
ˆ
and similarly for ∃. In this case the premise dˆ ∈ TZnc is not necessary because it follows from
dˆ ∈ Sd. The predicate R and also ≤, = on real numbers are assumed to be n.c. We write
(with x ranging over [−1, 1])
∀x A(x) for ∀x̂ (x̂ ∈ R → A(x̂))
∀x∈P A(x) for ∀x̂ (x̂ ∈ R → x̂ ∈ P → A(x̂))
and again similarly for ∃. The totality of x̂ is part of x̂ ∈ R.
We inductively define a predicate I0 on realsPs such that the generating sequence
dn dn
d0 , . . . , dm−1 for x ∈ I0 means that x is between n<m 2n+1 − 2m and n<m 2n+1 + 21m .
1 P
Let I0 be defined by the two clauses
x0 + d
∀x (x = 0 → x ∈ I0 ), ∀d∈Sd ∀x ∀x0 ∈I0 x = → x ∈ I0 .
2
Then the induction axiom is
x+d
∀x (x = 0 → x ∈ P ) → ∀d∈Sd ∀x ∀x0 ∈I0 ∩P x = → x ∈ P → I0 ⊆ P.
2
1http://minlog-system.de.
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:11
The clauses of I0 also determine the dual predicate coI0 , which is coinductively given by
the closure axiom
x0 + d
∀x∈coI0 x = 0 ∨ ∃d∈Sd ∃x0 ∈coI0 x =
2
and the coinduction axiom
x0 + d
∀x∈P x = 0 ∨ ∃d∈Sd ∃x0 ∈coI0 ∪P x = → P ⊆ coI0 .
2
We require that both predicates I0 and coI0 have computational content. The data type
associated to these clauses is the algebra L of lists of signed digits. This association is quite
canonical: the first constructor [] : L is a witness for the first clause, which does not need
any further information. The second constructor :: of type D → L → L is a witness for the
second clause consisting of a signed digit and a witness that x0 ∈ I0 . 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 RτL , of the closure axiom the destructor DL and of the coinduction
axiom the corecursion operator co RτL . 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 21n a rational number an
being 21n -close to x, i.e., |an − x| ≤ 21n . For simplicity we again restrict ourselves to real
dn
numbers in the interval [−1, 1] (rather than [−2n , 2n ]), and to dyadic rationals n<m 2n+1
P
(dn ∈ {1, 1̄}).
15 15
− 16 16
1̄ 1 1̄ 1 1̄ 1 1̄ 1 1̄ 1 1̄ 1 1̄ 1 1̄ 1
− 78 7
8
1̄ 1 1̄ 1 1̄ 1 1̄ 1
− 43 3
4
1̄ 1 1̄ 1
− 12 1
2
1̄ 1
0
Figure 2: Dyadic rationals.
Clearly we can represent real numbers (in [−1, 1]) as streams of 1, 1̄. Now when doing
arithmetic operations on such streams the problem of “productivity” arises: suppose we
want to add the two streams 1̄111 . . . and 11̄1̄1̄ . . . . 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 P well-known cure for this problem is to add a delay
dn
digit 0 and work with signed digits n<m 2n+1 , now with dn ∈ {1, 0, 1̄}. We have a lot of
redundancy here (for instance 1̄1 and 01̄ both denote − 14 ), but this is not a serious problem.
7:12 H. Schwichtenberg and F.Wiesnet Vol. 17:2
Since 0 as real number is represented by the stream consisting of the digit 0 only, we can
simplify our example by removing the nullary clause from the inductive definition of I0 , and
define I and coI accordingly. We only need coI, coinductively defined by the closure axiom
x0 + d
∀x∈coI ∃d∈Sd ∃x0 ∈coI x = . (2.1)
2
Therefore, the coinduction axiom is
x0 + d
∀x∈P ∃d∈Sd ∃x0 ∈coI∪P x = → P ⊆ coI. (2.2)
2
The canonically associated data type then becomes the algebra S given by a single binary
constructor of type D → S → S, again denoted by :: (infix). Note that we do not require
that TS u holds for any u. Objects u ∈ co TS are called streams of signed digits.
The computational content of the closure axiom (2.1) now is the destructor DS of type
S → D × S, defined by
DS (s :: u) = hs, ui.
For the coinduction axiom (2.2) we have the corecursion operator co RτS of type τ → (τ →
D × (S + τ )) → S. Note that D × (S + τ ) appears since S has the a single constructor of
type D → S → S. The meaning of co RτS is determined by a (non-terminating) computation
rule similar to the one for co RτL (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 xy 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 14 ≤ y; this can easily be extended to the
case 2−p ≤ y (using induction on p and Lemma 2.3 below). The main idea of the algorithm
and also of the proof, which is inspired by [CG06], consists in three representations of xy :
x−1
x 1 + xy1 0 + xy0 −1 + y
= = =
y 2 2 2
where
x + −y
2 x + y2
x1 = 4 , x0 = 2x, x−1 = 4 .
2 2
Depending on what we know about x we choose one of these representations of xy to obtain
its first digit. This will give us a corecursive definition of xy .
As we see in the representation of xy , we will use that coI is closed under the average:
Theorem 2.1. The average of two real numbers x, y in coI is in coI:
x + y
∀x,y∈coI ∈ coI .
2
Proof. 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 x+y2 . For the first n
x+y
digits in the representation of 2 one needs the first n + 1 digits in the representations of x
and y.
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:13
Lemma 2.2. coI is closed under shifting a real x ≤ 0 (x ≥ 0) by +1 (−1):
∀x∈coI (x ≤ 0 → x + 1 ∈ coI),
∀x∈coI (0 ≤ x → x − 1 ∈ coI).
Proof. We only consider the first claim; the second one is proved similarly. Since we want to
prove that something is in coI, the proof must use its introduction axiom given in (2.2):
x0 + d
∀x∈P ∃d∈Sd ∃x0 ∈coI∪P x = → ∀x (x ∈ P → x ∈ coI).
2
The crucial point is how to choose the competitor predicate P . Looking at the formula we
want to prove, we take P := { x | ∃y∈coI (y ≤ 0 ∧ x = y + 1) } as competitor predicate. Then
we have
x0 + d
∀x∈P ∃d∈Sd ∃x0 ∈coI∪P x = → ∀x (∃y∈coI (y ≤ 0 ∧ x = y + 1) → x ∈ coI)
2
and since coI is compatible with the real equality, this implies
x0 + d
∀x∈P ∃d∈Sd ∃x0 ∈coI∪P x = → ∀x∈coI (x ≤ 0 → x + 1 ∈ coI).
2
Therefore it suffices to prove the premise of the formula above. Let x ∈ P be given. Then by
definition of P there is y with y ∈ coI, y ≤ 0 and x = y + 1. From y ∈ coI we know |y| ≤ 1
and with y ≤ 0 also |x| ≤ 1. We need d ∈ Sd and x0 such that
d + x0
(x0 ∈ coI ∨ ∃y∈coI (y ≤ 0 ∧ x0 = y + 1)) ∧ x = .
2
Again from y ∈ coI we obtain e ∈ Sd and z ∈ coI with y = e+z
2 . We now distinguish cases on
e ∈ Sd.
Case e = 1. Then 0 ≥ y = 1+z 1 1
2 ≥ 2 − 2 = 0 and hence x = y + 1 = 1. Picking d = 1
0
and x = 1 gives the claim. Here we need a lemma CoIOne stating that 1 is in coI. The proof
of this lemma (by coinduction) is omitted.
Case e = 0. Pick d = 1 and x0 = z + 1. Then z = 2y ≤ 0 and hence the r.h.s. of the
disjunction above holds with z for y. Also x = 2y = 1+2y+1
2 .
Case e = −1. Pick d = 1 and x0 = z. Then the l.h.s. of the disjunction above holds,
0 −1+z
and d+x 1+z
2 = 2 = 2 + 1 = y + 1 = x.
We have formalized this proof in the Minlog2 proof assistant. Minlog has a tool to
extract from the proof a term representing its computational content; it is a term in the
theory 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 λu , and (CoRec ai=>ai) is the corecursion operator
co Rτ defined above, where τ is S again. The type of co RS is S → (S → D × (S + S)) → S.
S S
The first argument of the corecursion operator is the abstracted variable u of type S, and
the second ([u0][case ...]) is the “step” function, which first destructs its argument u0
2The development described here resides in minlog/examples/analysis, file sddiv.scm
7:14 H. Schwichtenberg and F.Wiesnet Vol. 17:2
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 D × (S + S) has SdR again as its left component, and
as right component the 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 SdR (written ~1 ).
The algorithm represented by the extracted term can be understood as follows. If
s = SdR, then y must be non-negative. Hence y = 0, and a stream-representation of y + 1
is ~1. Here we do not need a corecursive call, and hence the result is hSdR, InL(~1 )i. The
same happens in case s = SdL. Here y + 1 can be determined easily by changing the first
digit from SdL to SdR and leaving the tail as it is. Hence the result is hSdR, InL(u0 )i. Only
in case s = SdM we have a corecursive call. Here we change the first digit from SdM to
SdR, which however amounts to adding 12 only. Therefore the procedure continues with the
tail. Hence the result is hSdR, InR(u0 )i. Using the computation rule for co RSS we can now
describe the computational content as a function add1 : S → S defined by
add1(SdR :: u) := [SdR, SdR, . . . ],
add1(SdM :: u) := SdR :: add1(u),
add1(SdL :: u) := SdR :: u.
A similar argument for the second part of the lemma gives sub1 : S → S with
sub1(SdR :: u) := SdL :: u,
sub1(SdM :: u) := SdL :: sub1(u),
sub1(SdL :: u) := [SdL, SdL, . . . ].
1
Lemma 2.3. For x in coI with |x| ≤ 2 we have 2x in coI:
1
∀x∈coI |x| ≤ → 2x ∈ coI .
2
Proof. Let x ∈ coI be given. From the closure axiom (2.1) for coI we obtain d ∈ Sd and
0
x0 ∈ coI such that x = d+x
2 . We distinguish cases on d ∈ Sd.
0
Case d = 1. Then x = 1+x 0 1 0
2 and hence 2x = 1 + x . Since |x| ≤ 2 we have x ≤ 0. Now
the first part of Lemma 2.2 gives the claim.
0
Case d = 0. Then x = 0+x 0 co
2 and hence 2x = x ∈ I.
−1+x0
Case d = −1. Then x = 2 and hence 2x = −1 + x0 . Since |x| ≤ 12 we have 0 ≤ x0 .
Now the second part of Lemma 2.2 gives the claim.
Using arguments similar to those in the remark after Lemma 2.2 we can see that the
corresponding algorithm can be written as a function Double : S → S with
Double(SdR :: u) := add1(u),
Double(SdM :: u) := u,
Double(SdL :: u) := sub1(u)
where add1 and sub1 are the functions from this remark.
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:15
Lemma 2.4. For x, y in coI with 14 ≤ y, |x| ≤ y and 0 ≤ x (x ≤ 0) we have 2x − y ( 2x + y)
in coI:
1 x + −y
∀x,y∈coI ≤ y → |x| ≤ y → 0 ≤ x → 4 2
∈ coI ,
4 2
1 x + y2 co
∀x,y∈coI ≤ y → |x| ≤ y → x ≤ 0 → 4 ∈ I .
4 2
Proof. In the formulas above instead of 2x±y we have written 4 x+(±y/2)
2 to make Theorem 2.1
applicable. We also use two lemmas stating that coI is closed under x 7→ x2 and x 7→ −x. To
prove the first claim, let x, y in coI with 14 ≤ y, |x| ≤ y and 0 ≤ x. Then clearly −y co
2 ∈ I,
x+ −y
and 2
2
∈ coI by Theorem 2.1. We have
x + −y
2 2x − y 2y − y y 1
= ≤ = ≤ . (2.3)
2 4 4 4 4
x+ −y
Hence we can apply Lemma 2.3 twice and obtain 4 2
2
∈ coI. The proof of the second
claim is similar.
The computational content of the proofs is AuxL, AuxR : S → S → S:
AuxL(u, v) := Double(Double(Av(u, h(−v)))),
AuxR(u, v) := Double(Double(Av(u, h(v)))).
Here h, − : S → S represent the computational content of the two lemmas used in the proof;
both are proved by coinduction. The function h prepends SdM to the stream, and − negates
all digits:
−(SdR :: u) := SdL :: (−u),
h(u) := SdM :: u, −(SdM :: u) := SdM :: (−u),
−(SdL :: u) := SdR :: (−u).
1 x
Theorem 2.5. For x, y in coI with 4 ≤ y and |x| ≤ y we have y in coI:
1 x co
∀x,y∈coI ≤ y → |x| ≤ y → ∈ I .
4 y
Proof. The proof uses coinduction (2.2) on coI with P := { z | ∃x,y∈coI (|x| ≤ y ∧ 41 ≤ y ∧ z =
x co
y ) }. It suffices to prove (2.2)’s premise for this P . Let x, y, z be given with x, y ∈ I,
|x| ≤ y, 14 ≤ y and z = xy . From |x| ≤ y we have z ≤ 1. By a trifold application of the
closure axiom (2.1) to x we obtain d1 , d2 , d3 ∈ Sd and x̃ ∈ coI such that x = 4d1 +2d82 +d3 +x̃ or
x = d1 d2 d3 x̃ for short. We now distinguish three cases.
0
If x = 1d2 d3 x̃, x = 01d3 x̃ or x = 001x̃, then 0 ≤ x. Pick d = 1 and z 0 = xy with
x+ −y
x0 = 4 2 2 . Then x0 ∈ coI by Lemma 2.4. From (2.3) we also obtain |x0 | ≤ y and hence
0
z 0 ∈ P . One can easily check that z = 1+z 2 .
0
If x = 1̄d2 d3 x̃, x = 01̄d3 x̃ or x = 001̄x̃, then x ≤ 0. Pick d = −1 and z 0 = xy with
x+ y2
x0 = 4 2 . We can then proceed as in the first case.
7:16 H. Schwichtenberg and F.Wiesnet Vol. 17:2
[u,u0](CoRec ai=>ai)u
([u1][case (cCoIClosure u1)
(s pair u2 -> [case s
(SdR -> SdR pair InR(cCoIDivSatCoIClAuxR u1 u0))
(SdM -> [case (cCoIClosure u2)
(s0 pair u3 -> [case s0
(SdR -> SdR pair InR(cCoIDivSatCoIClAuxR u1 u0))
(SdM -> [case (cCoIClosure u3)
(s1 pair u4 -> [case s1
(SdR -> SdR pair InR(cCoIDivSatCoIClAuxR u1 u0))
(SdM -> SdM pair InR(cCoIToCoIDouble u1))
(SdL -> SdL pair InR(cCoIDivSatCoIClAuxL u1 u0))])])
(SdL -> SdL pair InR(cCoIDivSatCoIClAuxL u1 u0))])])
(SdL -> SdL pair InR(cCoIDivSatCoIClAuxL u1 u0))])])
Figure 3: Extracted term for Theorem 2.5.
x0
The final case is x = 000x̃. Then |x| ≤ 18 ; pick d = 0 and z 0 = y with x0 = 2x. We
z0
obtain |x0 | ≤ 1
4 ≤ y and with Lemma 2.3 also x0 ∈ coI. Therefore z 0 ∈ P , and z = 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 (2.1) to x. The seven cases
x = 1d2 d3 x̃, x = 01d3 x̃, x = 001x̃, x = 000x̃, x = 1̄d2 d3 x̃, x = 01̄d3 x̃ and x = 001̄x̃ are
clearly visible. In the first three cases SdR corresponds to picking d = 1 and usage of the
AuxR function from Lemma 2.4, and similarly in the last three cases SdL corresponds to
picking d = −1 and usage of AuxL. In the middle case SdM corresponds to d = 0; there we
use the computational content of Lemma 2.3. We can describe the extracted term by a
function Div : S → S → S corecursively defined by
SdR :: Div(AuxR(u, v), v) if u = 1ũ ∨ u = 01ũ ∨ u = 001ũ,
Div(u, v) := SdM :: Div(Double(u), v) if u = 000ũ,
SdL :: Div(AuxL(u, v), v) if u = 1̄ũ ∨ u = 01̄ũ ∨ u = 001̄ũ.
As abbreviation in the case distinction, we have denoted SdL, SdM and SdR by 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 Div(u, v). To this end we write the above equation as
Div(u, v) = d(u) :: Div(G(u, v), v),
where d(u) depends on the first three digits of u, and G(u, v) is one of AuxR(u, v), Double(u)
or AuxL(u, v), according to the present case. Recall
AuxL(u, v) := Double(Double(Av(u, h(n(v))))),
AuxR(u, v) := Double(Double(Av(u, h(v)))).
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:17
By the equations for −, h, Av and Double we see that the first n entries of
−u need the first n entries of u,
h(u) need the first n − 1 entries of u,
Av(u, v) need the first n + 1 entries of u and v,
Double(u) need the first n + 1 entries of u.
Hence AuxR(u, v), 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 Div(u, v) the representation
d(u) :: d(G(u, v)) :: d(G(G(u, v), v)) :: d(G(G(G(u, v), v), v), v) . . .
Therefore the first n entries of 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:
7 9
∼ 11̄11, ∼ 111̄1̄.
16 16
A possible cure is to flip after an occurrence of 1; see Figure 4. The result is called binary
reflected (or Gray-) code.
15 15
− 16 16
1̄ 1 1 1̄ 1̄ 1 1 1̄ 1̄ 1 1 1̄ 1̄ 1 1 1̄
− 78 7
8
1̄ 1 1 1̄ 1̄ 1 1 1̄
− 43 3
4
1̄ 1 1 1̄
− 12 1
2
1̄ 1
0
Figure 4: 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
7 9
∼ 1111̄, ∼ 11̄11̄.
16 16
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
7:18 H. Schwichtenberg and F.Wiesnet Vol. 17:2
Gray, H next character) and flip from one to the other after reading 1. They are defined by
simultaneous induction, with clauses
x−1 x
∀d∈Psd ∀x∈G −d ∈ G , ∀x∈H ∈G ,
2 2
x+1 x
∀d∈Psd ∀x∈G d ∈H , ∀x∈H ∈H .
2 2
Here Psd (for proper signed digit) is the (inductive) predicate consisting of the integers
1, −1. We require that Psd has computational content, in the booleans B = {tt, ff}. Note
that there are no nullary clauses (as for I), since they are not needed. We are only interested
in the duals coG, coH, coinductively defined by the simultaneous closure axioms
x0 − 1 x0
∀x∈coG ∃d∈Psd ∃x0 ∈coG x = −d ∨ ∃x0 ∈coH x =
2 2 (2.4)
0
x +1 0
x
∀x∈coH ∃d∈Psd ∃x0 ∈coG x = d ∨ ∃x0 ∈coH x =
2 2
and the simultaneous coinduction axioms
x0 − 1 x0
∀x∈P ∃d∈Psd ∃x0 ∈coG∪P x = −d ∨ ∃x0 ∈coH∪Q x = →
2 2
x0 + 1 x0 (2.5)
∀x∈Q ∃d∈Psd ∃x0 ∈coG∪P x = d ∨ ∃x0 ∈coH∪Q x = →
2 2
P ⊆ coG and the same with conclusion Q ⊆ coH.
We require that the predicates G, H and therefore coG, coH as well have computational
content, in simultaneously defined algebras G and H given by the constructors
Lr : B → G → G, U: H → G for G,
Fin : B → G → H, D: H → H for H.
We write Lrtt (u) for Lr(tt, u) and Lrff (u) for Lr(ff, u), and similarly for Fin. Then Lrtt/ff
means left/right, Fintt/ff means finally left/right. The delay constructors are U (“undefined”)
for G and D (“delay”) for H. Figure 5 indicates how these constructors generate Gray code.
− 34 3
4
U Lrtt Finff D Fintt U
Lrff Lrtt Lrff
− 12 1
2
U
Lrff Lrtt
0
Figure 5: Gray code with delay.
Totality TG , TH and cototality co TG , co T
H can be defined as for S above. Objects
u∈ co T
are called streams in Gray code.
G
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:19
The computational content of the closure axioms (2.4) are the destructors DG : G →
(B × G) + H and DH : H → (B × G) + H defined by
DG (Lrb (u)) = InLhb, ui, DG (Uv) = InR(v),
DH (Finb (u)) = InLhb, ui, DH (Dv) = InR(v).
The computational content of the coinduction axioms (2.5) are instances of the simultaneous
corecursion operators
co (G,H),(σ,τ )
RG : σ → δG → δH → G
(2.6)
co (G,H),(σ,τ )
RH : τ → δG → δH → H
with step types
δG := σ → B × (G + σ) + (H + τ ),
δH := τ → B × (G + σ) + (H + τ ).
The type B × (G + σ) + (H + τ ) appears since G has the two constructors Lr : B → G → G
and U : H → G, and H has the two constructors Fin : B → G → H and D : H → H. Omitting
the upper indices of co R the computation rules for the terms co RG sgh and co RH tgh are
Lr(b, u) if g(s) ≡ InLhb, InLG+σ ui
Lr(b, co R s0 gh) if g(s) ≡ InLhb, InR
0
co G G+σ s i
RG sgh =
U(v) if g(s) ≡ InR(InLH+τ v)
co
U( RH tgh) if g(s) ≡ InR(InRH+τ t)
(2.7)
Fin(b, u) if h(t) ≡ InLhb, InLG+σ ui
Fin(b, co R sgh) if h(t) ≡ InLhb, InR
co G G+σ si
RH tgh =
D(v)
if h(t) ≡ InR(InLH+τ v)
co 0
D( RH t gh) if h(t) ≡ InR(InRH+τ t0 )
with s of type σ and t of type τ .
Our goal in this section is to prove that [−1, 1] is closed under division xy (for |x| ≤ |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 coG and coH makes it
necessary to use simultaneous coinduction.
Theorem 2.6. The average of two real numbers x, y in coG is in coG:
x + y
∀x,y∈coG ∈ coG .
2
Proof. The proof in [BMST16] can be adapted to the present setting with concrete rather
than abstract reals.
Lemma 2.7. coG and coH are closed under minus:
∀x∈coG (−x ∈ coG), ∀x∈coH (−x ∈ coH).
7:20 H. Schwichtenberg and F.Wiesnet Vol. 17:2
Proof. We prove both claims simultaneously, by coinduction:
x0 − 1 x0
∀x∈P ∃d∈Psd ∃x0 ∈coG∪P x = −d ∨ ∃x0 ∈coH∪Q x = →
2 2
x0 + 1 x0
∀x∈Q ∃d∈Psd ∃x0 ∈coG∪P x = d ∨ ∃x0 ∈coH∪Q x = →
2 2
∀x (x ∈ P → x ∈ coG) ∧ ∀x (x ∈ Q → x ∈ coH).
We choose P := { x | −x ∈ coG } and Q := { x | −x ∈ coH }. Since coG and coH 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 ∈ P be given. The goal is
x0 − 1 x0
∃d∈Psd ∃x0 ∈coG∪P x = −d ∨ ∃x0 ∈coH∪Q x = .
2 2
From x ∈ P we get −x ∈ coG and therefore
x0 − 1 x0
∃d∈Psd ∃x0 ∈coG −x = −d ∨ ∃x0 ∈coH −x =
2 2
by the closure axiom. If the right hand side of this disjunction holds, we are done by
0
definition of Q. If the left hand side holds, we have x = d x 2−1 for some d ∈ Psd and
x0 ∈ coG. To get the left hand side of the disjunction in the goal formula, we take d := −d
and x0 := x0 .
The function we get from the proof takes a Gray code and flips all tt to ff and the other
way around. We denote this function by −. Then the computation rules are:
−(Lrtt (u)) = Lrff (−u), −(Fintt (u)) = Finff (−u),
−(Lrff (u)) = Lrtt (−u), −(Finff (u)) = Fintt (−u)),
−(U(v)) = U(−v), −(D(v)) = D(−v).
Lemma 2.8. coG and coH are equivalent:
∀x∈coG (x ∈ coH), ∀x∈coH (x ∈ coG).
Proof. In the coinduction axiom we choose P := coH and Q := coG 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 ∈ coH be
given. By the closure axiom of coH we have
x0 + 1 x0
∃d∈Psd ∃x0 ∈coG x = d ∨ ∃x0 ∈coH x =
2 2
If the second part of this disjunction holds, we get directly the second part of the first
0
premise. If the first part of the disjunction holds, we have x = d x 2+1 for some d ∈ Psd and
0
x0 ∈ coG. Then x = −d (−x2)−1 and using Lemma 2.7 we get the first part of disjunction in
the premise.
As computational content we have two functions ToCoH : G → H and ToCoG : H → G,
with computation rules
ToCoH(Lrb (u)) = Finb (−u), ToCoG(Finb (u)) = Lrb (−u),
ToCoH(U(v)) = D(v), ToCoG(D(v)) = U(v).
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:21
Note that no corecursive call is involved. We denote ToCoG(v), ToCoH(u) by ṽ, ũ, respec-
tively.
We show that coG is closed under shifting a real x ≤ 0 (x ≥ 0) by +1 (−1):
∀x∈coG ((x ≤ 0 → x + 1 ∈ coG) ∧ (0 ≤ x → x − 1 ∈ coG)).
The proof is by coinduction, simultaneously with the same proposition for coH. For the
coinduction proof it is helpful to reformulate the claim in such a way that the conclusion
has the form x ∈ coG:
Lemma 2.9.
∀x (∃y∈coG (y ≤ 0 ∧ (x = y + 1 ∨ x = −(y + 1))) → x ∈ coG).
Proof. We use the introduction axiom for coG and coH, and simultaneously prove
∀x (∃y∈coH (y ≤ 0 ∧ (x = y + 1 ∨ x = −(y + 1))) → x ∈ coH).
The competitor predicates are
P := { x | ∃y∈coG (y ≤ 0 ∧ (x = y + 1 ∨ x = −(y + 1))) },
Q := { x | ∃y∈coH (y ≤ 0 ∧ (x = y + 1 ∨ x = −(y + 1))) }.
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 ∈ P be given. Then we have y with
y ∈ coG, y ≤ 0 and x = y + 1 ∨ x = −(y + 1). From y ∈ coG we know |y| ≤ 1 and with y ≤ 0
also |x| ≤ 1. We need to prove the disjunction
x0 − 1 x0
D := ∃d∈Psd ∃x0 ∈coG∪P x = −d ∨ ∃x0 ∈coH∪Q x = .
2 2
From y ∈ coG we obtain either (i) e ∈ Psd, z ∈ coG with y = −e z−1 co
2 or else (ii) z ∈ H with
z
y = 2 . In case (i) we have |z| ≤ 1 since z ∈ coG. We distinguish cases on e ∈ Psd, and use
Lemma 2.7.
Case e = 1. Then 0 ≥ y = − z−1 1 1
2 ≥ − 2 + 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 x0 = −1 gives the claim (since
−1 ∈ coG). If x = −(y + 1), take x = −1 and go for the l.h.s. of the disjunction D. Picking
d = −1 and x0 = −1 gives the claim (since −1 ∈ coG).
Case e = −1. If x = y+1, go for the l.h.s. of the disjunction D, picking d = 1 and x0 = −z.
−z−1
Then x = y + 1 = z−1 z+1
2 + 1 = 2 = − 2 . If x = −(y + 1), go for the l.h.s. of the disjunction
−z+1
D, picking d = −1 and x0 = −z. Then x = −(y + 1) = − z−1 2 −1= 2 − 1 = −z−1
2 .
co z
In case (ii) we have |z| ≤ 1 (since z ∈ H) and z ≤ 0 (since y = 2 and y ≤ 0). Hence
|z +1| ≤ 1. If x = y +1, go for the l.h.s. of the disjunction D, picking d = 1 and x0 = −(z +1).
−(z+1)−1
Then −(z + 1) ∈ P (since also z ∈ coG and z ≤ 0), and x = y + 1 = z2 + 1 = z+2 2 =− 2 .
0
If x = −(y + 1), go for the l.h.s. of the disjunction D, with d = −1 and x = −(z + 1). Then
again −(z + 1) ∈ P and x = −(y + 1) = −(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 shG : G → B → G and shH : H → B → H defined by
shG(Lrtt (u), b) = Lrb (−1), shH(Fintt (u), b) = Finb (1),
shG(Lrff (u), b) = Lrb (−u), shH(Finff (u), b) = Finb (−u)),
shG(U(v), b) = Lrb (shH(ṽ, ff)), shH(D(v), b) = Finb (shG(ṽ, tt)).
7:22 H. Schwichtenberg and F.Wiesnet Vol. 17:2
Recall that v 7→ ṽ is the function extracted from the proof of Lemma 2.8 stating that coG
and coH are equivalent. If b = tt, we have computational content of the first part of the
lemma. If b = ff, we have the second part.
Lemma 2.10. For x in coG with |x| ≤ 21 we have 2x in coG:
1
∀x∈coG |x| ≤ → 2x ∈ coG .
2
Proof. Let x ∈ coG be given. From the closure axiom for coG we obtain either (i) d ∈ Psd,
0 0
x0 ∈ coG with x = −d x 2−1 , or else (ii) x0 ∈ coH with x = x2 . In case (i) we distinguish cases
0
on d ∈ Psd. In case d = 1 we obtain x = −x2+1 and hence 2x = −x0 + 1. Since |x| ≤ 12 we
have x0 ≤ 0. Now the first part of Lemma 2.9 gives the claim. The case d = −1 is similar,
using the second part of Lemma 2.9. In case (ii) we have 2x = x0 , hence the goal 2x ∈ coG
follows from the equivalence of coG and coH.
Using arguments similar to those in the remark after Lemma 2.9 we can see that the
corresponding algorithm can be written as a function Double : G → G with
Double(Lrtt (u)) := shG(−u, tt),
Double(Lrff (u)) := shG(−u, ff),
Double(U(v)) := ṽ
where shG and v 7→ ṽ are the functions from this remark.
Parallel to Lemma 2.4 we can now prove
coG 1
Lemma 2.11. For x, y in with 4 ≤ y, |x| ≤ y and 0 ≤ x (x ≤ 0) we have 2x − y
( 2x + y) in coG:
1 x + −y
∀x,y∈coG ≤ y → |x| ≤ y → 0 ≤ x → 4 2
∈ coG ,
4 2
1 x + y2 co
∀x,y∈coG ≤ y → |x| ≤ y → x ≤ 0 → 4 ∈ G .
4 2
Proof. We only consider the first claim, and again use Theorem 2.6 on the average. In the
formulas above instead of 2x ± y we have written 4 x+(±y/2)
2 to make Theorem 2.6 applicable.
One can see easily that coG is closed under x 7→ x2 . Formally, this is proved by coinduction,
and the corresponding algorithm is given by a function h : G → G. To prove the first claim,
x+ −y
let x, y in coG with 14 ≤ y, |x| ≤ y and 0 ≤ x. Then clearly −y co
2 ∈ G, and 2
2
∈ coG by
Theorem 2.6. We have the same estimate (2.3) as in the proof of Lemma 2.4; hence we
x+ −y
can apply Lemma 2.10 twice and obtain 4 2
2
∈ coG. The proof of the second claim is
similar.
The computational content are functions AuxL, AuxR : G → G → G with
AuxL(u, u0 ) := Double(Double(Av(u, h(−u0 )))),
AuxR(u, u0 ) := Double(Double(Av(u, h(u0 )))).
Parallel to the essential part of Theorem 2.5 we can now prove that division by y satisfies
to closure axiom for coI:
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:23
Theorem 2.12. For x, y in coG with 14 ≤ y and |x| ≤ y we find a signed digit d such that
2x = x0 + yd for some x0 ∈ coG with |x0 | ≤ y:
x0
1
0 x y + d
∀x,y∈coG ≤ y → |x| ≤ y → ∃d∈Sd ∃x0 ∈coG |x | ≤ y ∧ = .
4 y 2
Proof. We proceed as for Theorem 2.5, now using Lemma 2.11. The proof uses a trifold
application of the coinduction axioms for coG and coH to obtain the first three digits.
The computational content is a function f : G → G → D × G defined by
f (Lrtt (u), u0 ) = (1, AuxR(Lrtt (u), u0 ))
f (Lrff (u), u0 ) = (−1, AuxL(Lrff (u), u0 ))
f (U(v), Fintt (u)) = (1, AuxR(U(v), Fintt (u)))
f (U(v), Finff (u)) = (−1, AuxL(U(v), Finff (u)))
f (U(v), D(Fintt (u))) = (1, AuxR(U(v), D(Fintt (u))))
f (U(v), D(Finff (u))) = (−1, AuxL(U(v), D(Finff (u))))
f (U(v), D(D(v 0 ))) = (0, D(U(v)))
Corollary 2.13. For x, y in coG with 14 ≤ y and |x| ≤ y we have x
y in coG:
1 x
∀x,y∈coG ≤ y → |x| ≤ y → ∈ coG .
4 y
Proof. By coinduction, simultaneously with the same formula where coG is replaced by coH.
Theorem 2.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 2.5.
2.3. Translation to Haskell. The terms extracted from Theorem 2.5 and Corollary 2.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 files3 on
approximations of 13 and 12 . To return the first 19 digits of the result of dividing 1001
3001 by
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 2.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 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
d(u) :: d(G(u, v)) :: d(G(G(u, v), v)) :: d(G(G(G(u, v), v), v), v) . . .
3sddiv.scm and graydiv.scm residing in minlog/examples/analysis
7:24 H. Schwichtenberg and F.Wiesnet Vol. 17:2
number of digits runtime in seconds
10 0.01
25 0.05
50 0.14
75 0.26
100 0.46
250 2.69
500 10.11
750 23.90
1000 42.50
2000 182.92
10000 4567.74
Figure 6: Runtime
of Div(u, v). Therefore, for the first n digits, we have to compute
G(u, v), G(G(u, v), v), . . . , G(. . . G(u, v) . . . )
| {z }
n−1
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 2.5 and Corollary 2.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 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 et(M ) realizes A, i.e., et(M ) r A. In this
proof we make use of “invariance axioms”4 stating that every c.r. formula is invariant under
realizability, formally A ↔ ∃z (z r A). Finally in Section 3.3 we report on a Minlog tool
automatically generating such soundness proofs.
4They are called (A-r) “to assert is to realize” in [Fef79].
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:25
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 I0 in Section 1.4. By another (n.c.)
inductive predicate I0r of arity (R, L) we can express that a list u witnesses (“realizes”) that
the real x is in I0 . We write u r I0 x (u is a realizer of x ∈ I0 ) for (x, u) ∈ I0r . The predicate
I0r is required to be non-computational, since in (x, u) ∈ I0r we already have a realizer u. I0r
is inductively defined by the two clauses
x + d
(0, []) ∈ I0r , ∀d∈Sd ∀(x,u)∈I0r , sd :: u ∈ I0r
2
and the induction axiom
x + d
(0, []) ∈ Q → ∀d∈Sd ∀x∈I0r ∩Q , sd :: u ∈ Q → I0r ⊆ Q.
2
where sd is the signed digit corresponding to d ∈ Sd [SW12, p.334]). We write u r I0 x (u is
a realizer of x ∈ I0 ) for (x, u) ∈ I0r . The predicate I0r is required to be non-computational,
since in (x, u) ∈ I0r we already have a realizer u. I0r is inductively defined by the two clauses
x + d
(0, []) ∈ I0r , ∀d∈Sd ∀(x,u)∈I0r , sd :: u ∈ I0r
2
and the induction axiom
x + d
(0, []) ∈ Q → ∀d∈Sd ∀x∈I0r ∩Q , sd :: u ∈ Q → I0r ⊆ Q.
2
where sd is the signed digit corresponding to d ∈ Sd. Similarly we coinductively define the
n.c. predicate (coI0 )r of arity (R, L) to express that a list u witnesses (“realizes”) that the
real x is in coI0 . We write u r coI0 x (u is a realizer of x ∈ coI0 ) for (x, u) ∈ coI0r . The closure
axiom is
x0 + d
∀(x,u)∈(coI0 )r (x=0 ∧ u=[]) ∨ ∃d∈Sd ∃(x0 ,u0 )∈(coI0 )r x = ∧ u = sd :: u0
2
and the coinduction axiom
∀(x,u)∈Q (x = 0 ∧ u = []) ∨
x0 + d
∃d∈Sd ∃(x0 ,u0 )∈(coI0 )r ∪Q x = ∧ u = sd :: u0 → Q ⊆ (coI0 )r .
2
3.2. Soundness theorem. A formula or predicate is called r-free if it does not contain any
of the I r - or coI r -predicates. A proof M is called r-free if it contains r-free formulas only.
Theorem 3.1 (Soundness). Let M be an r-free proof of a formula A from assumptions
ui : Ci ( i < n). Then we can derive
(
et(M ) r A if A is c.r.
A if A is n.c.
from assumptions (
zui r Ci if Ci is c.r.
Ci if Ci is n.c.
7:26 H. Schwichtenberg and F.Wiesnet Vol. 17:2
Proof. By induction on M . In the base case we have to prove that the extracted terms of
I ± , coI ± 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 (λuA M B )A→B with A c.r. and B n.c. We need a derivation of A → B. By
induction hypothesis we have a derivation of B from z r A. Using the invariance axiom
A → ∃z (z r A) we obtain the required derivation of B from A as follows.
[z r A]
A → ∃z (z r A) A | IH
∃z (z r A) B −
B ∃
Case (M A→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 → B and of et(N ) r A. Now using the
invariance axiom ∀z (z r A → A) we obtain the required derivation of B by →− from the
derivation of A → B and
∀z (z r A → A) et(N ) | IH
et(N ) r A → A et(N ) r A
A
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.
Vol. 17:2 LOGIC FOR EXACT REAL ARITHMETIC 7:27
References
[Ber93] Ulrich Berger. Program extraction from normalization proofs. In M. Bezem and J.F. Groote,
editors, Typed Lambda Calculi and Applications, volume 664 of LNCS, pages 91–106. Springer
Verlag, Berlin, Heidelberg, New York, 1993.
[Ber09] Ulrich Berger. From coinductive proofs to exact real arithmetic. In E. Grädel and R. Kahle,
editors, Computer Science Logic, volume 5771 of LNCS, pages 132–146. Springer Verlag, Berlin,
Heidelberg, New York, 2009.
[Bis67] Errett Bishop. Foundations of Constructive Analysis. McGraw-Hill, New York, 1967.
[BMST16] Ulrich Berger, Kenji Miyamoto, Helmut Schwichtenberg, and Hideki Tsuiki. Logic for Gray-code
computation. In D. Probst and P. Schuster, editors, Concepts of Proof in Mathematics, Philosophy,
and Computer Science, pages 69–110. De Gruyter, 2016.
[CG06] Alberto Ciaffaglione and Pietro Di Gianantonio. A certified, corecursive implementation of exact
real numbers. Theoretical Computer Science, 351:39–51, 2006.
[Ers77] Yuri L. Ershov. Model C of partial continuous functionals. In R. Gandy and M. Hyland, editors,
Logic Colloquium 1976, pages 455–467. North-Holland, Amsterdam, 1977.
[Fef79] Solomon Feferman. Constructive theories of functions and classes. In K. McAloon M. Boffa, D.
van Dalen, editor, Logic Colloquium 78, volume 97 of Studies in Logic and the Foundations of
Mathematics, pages 159–224. North-Holland, Amsterdam, 1979.
[Gia99] Pietro Di Gianantonio. An abstract data type for real numbers. Theoretical Computer Science,
221(1-2):295–326, 1999.
[Kol32] Andrey N. Kolmogorov. Zur Deutung der intuitionistischen Logik. Math. Zeitschr., 35:58–65,
1932.
[MS15] Kenji Miyamoto and Helmut Schwichtenberg. Program extraction in exact real arithmetic. Math-
ematical Structures in Computer Science, 25:1692–1704, 2015.
[Sco70] Dana Scott. Outline of a mathematical theory of computation. Technical Monograph PRG–2,
Oxford University Computing Laboratory, 1970.
[SW12] Helmut Schwichtenberg and Stanley S. Wainer. Proofs and Computations. Perspectives in Logic.
Association for Symbolic Logic and Cambridge University Press, 2012.
[Tsu02] Hideki Tsuiki. Real number computation through Gray code embedding. Theoretical Computer
Science, 284:467–485, 2002.
[Wie17] Franziskus Wiesnet. Konstruktive Analysis mit exakten reellen Zahlen. Master’s thesis, Mathema-
tisches Institut der Universität München, 2017.
[Wie18] Franziskus Wiesnet. Introduction to Minlog. In K. Mainzer, P. Schuster, and H. Schwichtenberg,
editors, Proof and Computation, pages 233–288. World Scientific, 2018.
This work is licensed under the Creative Commons Attribution License. To view a copy of this
license, visit https://creativecommons.org/licenses/by/4.0/ or send a letter to Creative
Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher Strasse
2, 10777 Berlin, Germany