A coinductive approach to verified exact real number computation


Electronic Communications of the EASST
Volume 23 (2009)

Proceedings of the
Ninth International Workshop on

Automated Verification of Critical Systems
(AVOCS 2009)

A coinductive approach to verified exact real number computation

Ulrich Berger and Sion Lloyd

15 pages

Guest Editor: Markus Roggenbach
Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer
ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122

http://www.easst.org/eceasst/


ECEASST

A coinductive approach to verified exact real number computation

Ulrich Berger and Sion Lloyd

University of Wales Swansea, Swansea, SA2 8PP, Wales UK

Abstract: We present an approach to verified programs for exact real number com-
putation that is based on inductive and coinductive definitions and program extrac-
tion from proofs. We informally discuss the theoretical background of this method
and give examples of extracted programs implementing the translation between the
representation by fast converging rational Cauchy sequences and the signed binary
digit representations of real numbers.

Keywords: Proof theory, program extraction, exact real number computation, coin-
duction

1 Introduction

In current implementations of main stream programming languages real numbers are represented
in floating point format, and computation on real numbers is done with respect to this represen-
tation. As is well-known, rounding errors in floating point arithmetic may occur, and inevitably
do so, due to the limited precision of floating point numbers on the one hand and the infinitary
character of the real numbers on the other hand. The problem with this is not so much the fact
that these rounding errors occur already in relatively simple computations, but that the user has
no control over them. As a simple example consider the function

f(x) = 1+x-(xˆ2)*(x+1)*((1/x)-(1/(x+1))) -- Haskell code

and the computations

*Main> f(10ˆ4) :: Float
2.834961

*Main> f(10ˆ4) :: Double
1.0000000006384653

*Main> f(10ˆ9) :: Double
-149.21128177642822

Which of these results can we trust? Actually, in all three cases the correct result is 1.0, which
can be easily seen by applying elementary school algebra to the expression defining the function
f . The situation we encounter here is typical: in order to estimate the accuracy of a floating point
computation one needs, in principle, always a mathematical analysis of the numerical stability
of the problem which can be arbitrarily difficult. Increasing the precision cannot replace such an
analysis because one does not know by how much the precision needs to be increased in order to
obtain a required number of correct digits. In view of safety critical applications of numeric com-
putation, for example autopilot systems for aircrafts, these problems can no longer be neglected,

1 / 15 Volume 23 (2009)



A coinductive approach to verified exact real number computation

but require alternative approaches that have a sound mathematical and technological basis. Such
approaches are currently promoted under the slogan “computing with exact real numbers”. In
exact real number computation results are not necessarily exact, but they are guaranteed to be
correct with any accuracy prescribed by the user. This means the user has full control over errors.
Of course, it still can happen that a given accuracy cannot be obtained due to limited resources
in time and space, but it will never happen that a result is delivered without information about its
accuracy.

A further essential requirement in exact real number computation is that the correctness of a
program has to be proven (in a stringent mathematical sense) in order to justify the user’s trust
in it. The generation of provably correct programs in exact real number computation is the focus
of this paper.

In traditional program verification one takes a program and applies a certain method to prove
that it meets a given specification (see the seminal papers [Flo67, Hoa97, Dij75, Pnu77, Mil80]
and systems supporting program verification, e.g. PVS [ORSS98], Isabelle [NPW02], Coq [Coq],
KIV [BRS+00], ACL2 [KMM00], BLAST [Bez07]). Another approach is to develop or derive
programs according to certain rules that preserve correctness, thus obtaining programs that are
correct “by construction” [Dij97, Gri81, DJ78]. The method we are presenting can be seen as
a rather radical instance of the latter approach. From a formal constructive proof of a mathe-
matical statement A we extract a program that “realises” A. In general, the statement A does not
need to be related to programming, but in specific cases A may be viewed as a specification of
a computational problem that is solved by the extracted program. By a constructive proof we
mean a proof that does not make use of the law of excluded middle or equivalent principles.
Constructive reasoning is being adopted in Intuitionism [vH67, Hey56, Tro73], Constructive
Mathematics [BB85] and Constructive Type Theory [ML84], and is implemented in a number
of interactive proof systems, for example, NuPrL [Con86], Coq [Coq], Minlog [BBS+98] and
Agda [Agd]. The logical basis of program extraction via realisability was laid by Kleene [Kle45]
and Kreisel [Kre59] (for proof-theoretic purposes). It is an instance of what is known in Com-
puter Science as the “Curry-Howard correspondence” or “proofs-as-programs” paradigm which
is applicable to constructive proofs in a wide range of areas. In this paper we concentrate on con-
structive real analysis and we illustrate the method by some simple yet non-trivial examples. We
want to make the case that it is not only possible in principle, but also feasible in practice to ex-
tract interesting programs from proofs (see also [Sch09] for related work on program extraction
in constructive analysis).

An important principle for definitions and proofs we are using is coinduction. A coinductive
definition can be viewed set-theoretically as the largest fixed-points of a monotone set opera-
tor or category-theoretically as the final coalgebra of a functor. Recently, coinductive defini-
tions, coalgebras and coinductive proofs have become very popular for describing concurrent
systems and cryptographic protocols [BS07, JR97, Mos99, Rut00, HW03]. Also, much of the
recent work on exact real number computation uses coinduction to verify real number algorithms
w.r.t. the representation of real numbers by infinite streams of signed digits and similar represen-
tations [EH02, ME07, GNSW07, CD06, Ber07, BH08]. In our paper we go one step further and
extract these algorithms from proofs about coinductive characterisations of real numbers.

Proc. AVOCS 2009 2 / 15



ECEASST

2 Induction and coinduction

We give a brief introduction to coinduction and the dual principle of induction. We begin with
the latter as it is more familiar.

Consider an operator Φ : P(U ) → P(U ), where U is a set and P(U ) is the powerset of
U , and assume that Φ is monotone, i.e. if X ⊆ Y ⊆ U , then Φ(X ) ⊆ Φ(Y ). Since P(U ) is a
complete lattice w.r.t. set inclusion Φ has a least fixed point µ Φ, according to the Knaster-Tarski
Theorem. In fact, µ Φ is the least Φ-closed subset of U where a set X ⊆U is called Φ-closed if
Φ(X ) ⊆ X . Hence we have the closure principle for µ Φ

Φ(µ Φ) ⊆ µ Φ

as well as the induction principle

if Φ(X ) ⊆ X then µ Φ ⊆ X

for all subsets X of U (one often says “induction on µ Φ”). In many cases Φ has a definition of
the form Φ(X ) = {u ∈U|A(u)∨B(X , u)} where A(u) does not depend on X . Then the inclusion
Φ(X ) ⊆ X is equivalent to ∀u ∈ U [(A(u) ⇒ X (u))∨(B(X , u) ⇒ X (u))] and the implications
A(u) ⇒ X (u) and B(X , u) ⇒ X (u) are called induction base and step respectively, B(X , u) is
called induction hypothesis.

It is easy to see that µ , considered as an operation on monotone operators, is itself monotone,
i.e. if Φ(X ) ⊆ Ψ(X ) for all X ⊆U , then µ Φ ⊆ µ Ψ. Indeed, by the induction principle it suffices
to show Φ(µ Ψ) ⊆ µ Ψ. But Φ(µ Ψ) ⊆ Ψ(µ Ψ) ⊆ µ Ψ. From the monotonicity of µ one can infer
the following strong induction principle

if Φ(X ∩µ Φ) ⊆ X then µ Φ ⊆ X

For the proof of strong induction we assume Φ(X∩µ Φ)⊆X which can be rewritten as Ψ(X )⊆X
where Ψ(X ) := Φ(X∩µ Φ). Clearly Ψ is a monotone operator. Thus µ Ψ⊆X . Hence it is enough
to show µ Φ ⊆ µ Ψ. We prove this by induction on µ Φ. By the monotonicity result above we
have the reverse inclusion µ Ψ ⊆ µ Φ. Hence, Φ(µ Ψ) = Φ(µ Ψ∩µ Φ) = Ψ(µ Ψ) ⊆ µ Ψ.

Example 1 (Natural Numbers) Let R be the set of real numbers and define Φ : P(R) → P(R)
by Φ(X ) := {0}∪{y + 1|y ∈ X}. Then µ Φ = N = {0, 1, 2, . . .}. The closure principle for N is
equivalent to N(0)∧∀x (N(x) → N(x + 1)) while the induction principle for N is equivalent to
(X (0)∧∀x (X (x) → X (x + 1)) →∀x (N(x) → X (x)). The strong induction principle is similar,
but with the step formula ∀x (X (x) → X (x + 1)) weakened to ∀x ∈ N (X (x) → X (x + 1)).

Now we turn our attention to coinduction which is dual to induction. For the same reason a
monotone operator Φ has a least fixed point it has a greatest fixed point ν Φ. It is the largest
Φ-coclosed subset of U where a set X ⊆ U is called Φ-coclosed if X ⊆ Φ(X ). Consequently,
we have coclosure: ν Φ ⊆ Φ(ν Φ), and coinduction: if X ⊆ Φ(X ) then X ⊆ ν Φ. With a similar
argument as for µ one can show that ν is monotone and deduce from that a strong coinduction
principle: if X ⊆ Φ(X ∪ν Φ) then X ⊆ ν Φ. We will see examples of coinduction in Sect. 3.

3 / 15 Volume 23 (2009)



A coinductive approach to verified exact real number computation

3 Cauchy and signed digit representations of real numbers

The primary objects of study in this paper are the real numbers in the compact interval

I := [−1, 1] = {x ∈ R | |x|≤ 1}

Since real numbers are per-se abstract objects, it is not possible to compute with them directly:
one has to refer to a specific representation. Two common representations of real numbers x ∈ I
are

(1) Cauchy sequences (qn)n∈N where qn ∈ I is rational with |x−qn|≤ 2−n for all n ∈ N,

(2) power series x = ∑i∈N di2
−(i+1) where di ∈ SD := {0, 1,−1} (signed digits).

We consider the problem of producing a translation between the two representations that is for-
mally proven to be correct. Note that in a traditional approach a quite complex formal system
is required to deal with this problem: We need sorts for reals, rationals, natural numbers, digits
and infinite sequences, and, in addition to the usual arithmetic operations, coercion functions
between these sorts. Furthermore, the system must be able to express the recursive or iterative
definitions of the higher-order functions translating between the two representations. On the
other hand, the approach we are proposing and demonstrating here requires only one sort for
real numbers with the usual first-order axioms for a real closed fields as well as the possibility to
formalise inductive and coinductive definitions that were described in Sect. 2. In the following,
all individual variables (denoted by lower case letters) range over real numbers.

We model the Cauchy representation (1) by the formula A(x) := ∀n ∈ N An(x) where N is
defined as in Example 1 in Sect. 2 and

An(x) := ∃q ∈ Q (|x|≤ 1∧|x−q|≤ 2−n)

Here Q defines the rational numbers as a subset of the real numbers in the usual way with help of
the predicate N. E.g. Q(x) := ∃m, n, k ∈ N (k > 0∧xk = m−n) 1. The formula A(x) replaces the
Cauchy representation in the sense that from a constructive proof of it one can extract a program
implementing an infinite sequence (qn)n ∈ N satisfying (1). Note that this infinite sequence is
not present in the formula A(x). Details of how this extraction works in general will be given in
Sect. 4.

We model the signed digit representation (2) by a coinductive definition, motivated by the
observation that if x = ∑i∈N di2

−(i+1), then |x−d0/2| ≤ 1/2 and 2x−d0 = ∑i∈N di+12−(i+1).
Therefore, we set Id (x) := |x−d0/2|≤ 1/2 and define C as the largest set (of real numbers) such
that

C(x) ⇒∃d ∈ SD(Id (x)∧C(2x−d))

More formally C := νJ where the set operator J : P(R) → P(R) is defined by J (X ) :=
{x|∃d ∈ SD(Id (x)∧X (2x−d))}. Now, the program extracted from a proof of C(x) will be an
infinite stream of digits di ∈ SD such that (2) holds.

In order to extract a program that translates between the representations (1) and (2) it will be
sufficient to prove constructively the equivalence of the formulas ∀n ∈ N An(x) and C(x).
1 The bounded quantifiers we used are just shorthands: ∀x ∈ X B(x) stands for ∀x (X (x) → B(x)) and ∃x ∈ X B(x)
stands for ∃x (X (x)∧B(x)).

Proc. AVOCS 2009 4 / 15



ECEASST

4 Program extraction: theory

In this section we briefly describe the program extraction process in general, giving explanations
of the main ideas priority over complete and formal definitions and correctness proofs.

4.1 The programming language

The programming language that will be the target of the extraction process is a λ -calculus with
constructors and pattern matching and (ML-)polymorphic recursive types. We let α range over
type variables.

Type 3 ρ, σ ::= α | 1 | ρ + σ | ρ ×σ | ρ → σ | fix α . ρ

In the definition of terms we let x range over term variables and C over constructors. It is always
assumed that a constructor is applied to the correct number of arguments as determined by its
arity. We will only use the constructors Nil (nullary), Left, Right (unary), Pair (binary), and
Infix α . ρ (unary) for every fixed point type fix α . ρ .

Term3M, N ::= x |C( ~M) |case M of{C1(~x1)→N1 ; . . . ; Cn(~xn)→Nn}|λ x.M |(M N) | rec x . M

In a pattern Ci(~xi) of a case-term all variables in ~xi must be different. The typing relation Γ`M : ρ
is defined inductively as follows.

Γ, x : ρ ` x : ρ Γ ` Nil : 1 Γ, x : ρ ` M : ρ
Γ ` rec x . M : ρ

Γ, x : ρ ` M : σ
Γ ` λ x.M : ρ → σ

Γ ` M : ρ → σ Γ ` N : ρ
Γ ` M N : σ

Γ ` M : ρ Γ ` N : σ
Γ ` Pair(M, N) : ρ ×σ

Γ ` M : ρ ×σ Γ, x1 : ρ, x2 : σ ` K : τ
Γ ` case M of{Pair(x1, x2) → K} : τ

Γ ` M : ρ
Γ ` Left(M) : ρ + σ

Γ ` M : σ
Γ ` Right(M) : ρ + σ

Γ ` M : ρ + σ Γ, x1 : ρ ` L : τ Γ, x2 : σ ` R : τ
Γ ` case M of{Left(x1) → L ; Right(x2) → R} : τ

Let ρ = ρ(~α) = fix α . ρ0(α,~α):
Γ ` M : ρ0(ρ(~σ ),~σ )
Γ ` Inρ (M) : ρ(~σ )

Γ ` M : ρ(~σ ) Γ, x : ρ0(ρ(~σ ),~σ ) ` K : τ
Γ ` case M of{Inρ (x) → K} : τ

Equipped with a lazy semantics, which is described in [Ber09b], this system can be viewed al-
most literally as a fragment of Haskell. For example, a type fix α . ρ where ρ = ρ(α, β ) has
no free type variables other than α and β , can be modelled in Haskell by the data declaration
data FixRho beta = InFixRho (Rho FixRho beta) provided Rho alpha beta
models ρ . A term rec x . M is modelled by let {x = M} in x. In fact, in Sect. 5 we will
present the extracted programs as Haskell code (however, for the general considerations in the
remainder of this Section the system above is more convenient). It is easy to see that this system
is ML-polymorphic: if ` M : ρ(~α), then ` M : ρ(~σ ) for arbitrary types ~σ .

5 / 15 Volume 23 (2009)



A coinductive approach to verified exact real number computation

4.2 The object language

The object language L which is used to formalise the proofs we want to extract programs from
is a first-order language extended by predicate variables and the possibility to form least and
greatest fixed points of strictly positive (and hence monotone) operators. Terms, r, s,t . . ., are
built from constants, first-order variables and function symbols as usual. Formulas, A, B,C . . .,
are s = t, P(~t) where P is a predicate (predicates are defined below), A∧B, A∨B, A → B, ∀x A,
∃x A. A predicate is either a predicate constant P, or a predicate variable X , or a comprehension
term {~x | A} where A is a formula and ~x is a vector of first-order variables, or an inductive
predicate µ X .P, or a coinductive predicate ν X .P where P is a predicate of the same arity
as the predicate variable X and which is strictly positive in X , i.e. X does not occur free in any
premise of a subformula of P which is an implication. The application, P(~t), of a predicate
P to a list of terms ~t is a primitive syntactic construct, except when P is a comprehension
term, P = {~x | A}, in which case P(~t) stands for A[~t/~x]. We will frequently use common
abbreviations such as P ⊆ Q := ∀~x (P(~x) → Q(~x)), {~t | A} := {~x | ∃~y (~x =~t ∧A)} where ~y are
the variables occurring free in A or t, f ( ~P) := { f (~x) | P1(x1)∧. . .∧Pn(xn)}, and so on.

The proof rules for L are the usual ones for intuitionistic predicate calculus with equality
[Hey56, Kle45, Tro73], plus the axiom schemes for inductive and coinductive predicates that
were discussed in Sect. 2. In addition we allow any axioms expressible by non-computational
formulas that hold in the intended model. Falsity can be defined as ⊥ := µ X .X where X is a
0-ary predicate variable (i.e. a propositional variable). From the induction axiom for ⊥ it follows
immediately ⊥→ A for every formula A.

For our examples it will be sufficient to have only one sort for real numbers in L (a many-
sorted language would be possible as well) together with the usual algebraic equations and in-
equations for the operations on real numbers.

4.3 Realisability

The first step in program extraction is to assign to every L -formula A a type τ(A), the type
of potential realisers of A. If A contains neither predicate variables nor the logical connective
∨ (disjunction), then we call it non-computational (otherwise computational) and set τ(A) = 1
(= () in Haskell). Otherwise, τ(P(~t)) = τ(P) (for predicates P the type τ(P) is defined
below), τ(A∧B) = τ(A)×τ(B), τ(A∨B) = τ(A) + τ(B), τ(A → B) = τ(A) → τ(B), τ(∀x A) =
τ(∃x A) = τ(A), For predicates P we define τ(P) by τ(X ) = αX where αX is a type variable
assigned in a one-to-one fashion to the predicate variable X , τ({~x | A}) = τ(A), and τ(µ X .P) =
τ(ν X .P) = fix αX . τ(P).

As one can see, the mapping τ wipes out all first-order content of a formula (first-order terms
and quantifiers), hence the type τ(A) can be viewed as the “propositional skeleton” of the formula
A. This is necessarily so, since the sorts in our first order language (R in our example in Sect. 3)
have no counterpart in our programming language.

The next step is to define for every formula A and every program term M of type τ(A) what
it means for M to realise A, formally M r A. The latter is a formula in the language r(L ) which
is obtained by adding to L a sort for program terms and extending all other constructions con-
cerning formulas and proofs mutatis mutandis. The r(L )-formula M r A is in fact shorthand for

Proc. AVOCS 2009 6 / 15



ECEASST

r(A)(M) where the r(L )-predicate r(A) is defined by structural recursion on A, relative to a fixed
one-to-one mapping from L -predicate variables X to r(L )-predicate variables X̃ with one extra
argument place for program terms. If the formula A has the free predicate variables X1, . . . , Xn,
then the predicate r(A) has the free predicate variables X̃1, . . . , X̃n. Simultaneously with r(A) we
define a predicate r(P) for every predicate P, where r(P) has one extra argument place for
program terms. If A is non-computational, then r(A) = {() | A}. If P is non-computational,
then r(P) = {((),~x) | P(~x)}. In all other cases: For a non-computational formula A we set
M r A := M = Nil∧A, and

r(P(~t)) = {x | r(P)(x,~t)} r(A → B) = { f | f (r(A)) ⊆ r(B)}
r(A∨B) = inl(r(A))∪inl(r(B)) r(A∧B) = Pair(r(A), r(B))
r(∃y A) = {x | ∃y (r(A)(x))} r(∀y A) = {x | ∀y (r(A)(x))}

r(X ) = X̃ r({~y | A}) = {(x,~y) | r(A)(x)}
r(µ X .P) = µ X̃ .r(P) r(ν X .P) = ν X̃ .r(P)

We see that quantifiers and the quantified variable, although ignored by the program M and its
type, of course do play a role in the definition of realisability, i.e. the specification of the program.

Finally, we sketch how to extract from a proof of a formula A a program term M realising
A. Assuming the proof is given in a natural deduction system the extraction process is straight-
forward and follows in most cases the usual pattern of the Curry-Howard correspondence: Any
non-computational axiom has the trivial program Nil as extracted program. The introduction and
elimination rules for conjunction, disjunction and implication correspond to pairing, projection,
injections into a disjoint sum, pattern matching, lambda-abstraction, and application, respec-
tively. The ∀-introduction rule, ∀-elimination rule, and the ∃-introduction rule are ignored, i.e.
the extracted program of the conclusion is identical to the one of the premise. The ∃-elimination
rule corresponds to application, more precisely, if the proofs of the premises ∃x A and ∀x (A → B)
(where x is not free in B) have extracted programs M : τ(A) and N : τ(A) → τ(B), respectively,
then the extracted program for the conclusion B is simply the application M N : τ(B). The ex-
tracted programs of closure, Φ(µ Φ) ⊆ µ Φ, and induction, (Φ(X ) ⊆ X ) ⇒ Φ(µ Φ) ⊆ X , are
infix α . ρ := λ x.Infix α . ρ (x) and

itfix α . ρ := λ s.rec f . λ x.case x of{Infix α . ρ (y) → s(mapα,ρ f y)}

where it is assumed that τ(Φ(X )) = ρ(α). The term mapα,ρ has type (α → β ) → ρ(α) → ρ(β )
and can be defined by induction on ρ(α). For coclosure, ν Φ ⊆ Φ(ν Φ), and coinduction, (X ⊆
Φ(X ))⇒X ⊆Φ(ν Φ), the extracted programs are outfix α . ρ := λ x.case x of{Infix α . ρ (y)→y} and

coitfix α . ρ := λ s.rec f . λ x.Infix α . ρ (mapα,ρ f (s x))

We have the typings

` infix α . ρ : ρ(fix α . ρ) → fix α . ρ ` itfix α . ρ : (ρ(α) → α) → (fix α . ρ) → α
` outfix α . ρ : (fix α . ρ) → ρ(fix α . ρ) ` coitfix α . ρ : (α → ρ(α)) → α → fix α . ρ

The Soundness Theorem, stating that the program extracted from a proof does indeed realise the
proven formula, is shown in [Ber09b]. Soundness Theorems for similar systems can be found in
[Tat98] and Miranda-Perea [MP05].

7 / 15 Volume 23 (2009)



A coinductive approach to verified exact real number computation

5 Program extraction: applications

In this Section we apply the program extraction procedure described in Sect. 4 to a proof of
the equivalence of the real number representations described in Sect. 3. Below we give a fairly
detailed constructive proof of the equivalence which can be easily formalised in the object system
described in Sect. 4.2, and from which we then extract the program.

Before we do that we discuss a simple example that demonstrates the fact that it is indeed cru-
cial for program extraction that proofs are constructive and no axioms other than the axioms for
inductive and coinductive definitions and true non-computational axioms are used. The formula
∀x, y (x ≤ y∨y > x), although true in the real numbers, must not be used as an axiom because it
is computational. We cannot prove it constructively either, because otherwise we could extract a
(closed) program M : Boole realising it, where Boole := 1 + 1. This would mean that the formula,
setting t := Left(Nil) and f := Right(Nil),

∀x, y ((M = t∧x ≤ y)∨(M = f∧y > x))

holds. Since M is closed, either M = t or M = f. In the first case it would follow ∀x, y (x ≤ y)
in the second case ∀x, y (x > y) which are both false statements (similar unprovability results
were among Kleene’s and Kreisel’s original motivations for studying realisability). Of course,
we can prove constructively the relativised formula ∀x, y ∈ N (x ≤ y∨y > x) (by induction). The
extracted program is a decision procedure for the ordering of natural numbers. Since Nat :=
τ(N(x)) = fix α . 1 + α the program works with the unary representation of natural numbers,
more precisely, its type is Nat → Nat → Boole. Similarly, we can prove constructively ∀x, y ∈
Q (x ≤ y∨y > x) and extract a program deciding the ordering on rational numbers.

A formula which we can safely assume as an axiom is ∀x (A(x) → I(x)). Clearly, this formula
is true and it has the trivial realiser λ f .Nil.

5.1 Proofs

The following Lemma takes care of some simple technicalities in the main proof.

Lemma 1 (a) SD ⊆ Q.

(b) ∀q ∈ Q∃d ∈ SD [q−1/4, q + 1/4]∩I ⊆ Id .

(c) ∀p ∈ Q∃q ∈ Q∩I∀x ∈ I|x−q|≤ |x− p|.

Proof. Part (a) is obvious. For part (b) we do a case analysis on the position of q. For q < −14
choose d = −1, for −14 ≤ q ≤

1
4 choose d = 0 and for

1
4 < q choose d = 1. It is easy to see that

in all cases d is as required. For part (c) let p ∈ Q be given. Depending on whether p < −1 or
|p|≤ 1 or p > 1 we set q := −1 or q := p or q := 1. The required property obviously holds.

Proposition 1 ∀x (C(x) ⇔ A(x)).

Proof. For the implication from left to right we prove ∀n ∈ N(C(x) ⇒ An(x)) by induction on N.
Base n = 0: If C(x), then clearly x ∈ I, i.e. |x|≤ 20. Hence we can take q := 0 to satisfy A0(x).

Proc. AVOCS 2009 8 / 15



ECEASST

Step: The induction hypothesis is ∀x(C(x) ⇒∃q|x−q|≤ 2−n). We have to show ∀x(C(x) ⇒
∃q|x−q|≤2−(n+1)). Assume C(x). By the coclosure principle for C we have Id (x) and C(2x−d)
for some d ∈ SD. Set x′ := 2x−d. By induction hypothesis, |x′−q|≤ 2−n for some q. Hence
|x′−q|

2 ≤
2−(n+1)

2 , i.e.
|2x−d−q|

2 ≤ 2
−(n+1), i.e. |x− d2 −

q
2|≤ 2

−(n+1), i.e. |x− d+q2 |≤ 2
−(n+1), so we

may take q′ := d+q2 using Lemma 1 (a).
For the implication from right to left we need to show A ⊆ C. By applying coinduction it is

sufficient to show A ⊆ J (A), i.e.

∀x(A(x)) ⇒∃d ∈ SD (Id (x)∧A(2x−d)))

Assume A(x). Then I(x) by the axiom discussed above. We have to find d ∈ SD such that

Id (x)∧∀n ∈ N∃q ∈ Q∩I|(2x−d)−q|≤ 2−n

Using the assumption A(x) with n = 2, we obtain a q ∈ Q∩I such that |x−q|≤ 14 . According
to Lemma 1 (b) there is some d ∈ SD such that [q−1/4, q + 1/4]∩I ⊆ Id . Now let n ∈ N. We
have to find q ∈ Q∩I such that |(2x−d)−q|≤ 2−n. We use the assumption A(x) with n + 1
and obtain q′ ∈ Q∩I such that |x−q′|≤ 2−(n+1). Since x ∈ Id and because of Lemma 1 (c) we
may assume without loss of generality that q′ ∈ Id . Hence q := 2q′−d ∈ I and |(2x−d)−q| =
2|x−q′|≤ 2−n.

5.2 Programs

We begin our program extraction by declaring the types of the predicates SD and Q. We do not
bother deriving them pedantically following Sect. 4, but define them in Haskell in a convenient
way. For Q it is most convenient to use the build-in type of exact rational numbers.

data SD = N | Z | P deriving Show
type Rat = Rational

Next we extract programs from Lemma 1. Again, because the proofs are so simple, we do the
extraction in an intuitive and non-pedantic way using build-in operations on the rational numbers.
We also apply, here and in the following, some simplifications to types and extracted programs.
For example, if B is computational, but A is not, we set τ(A∧B) = τ(A → B) = τ(B) (instead of
1×τ(B) and 1 → τ(B)) and adjust realisability and program extraction accordingly.

lema :: SD -> Rat
lema = \d-> case d of {N -> -1; Z -> 0; P -> 1}

lemb :: Rat -> SD
lemb q | q < -1/4 = N

| q > 1/4 = P
| otherwise = Z

lemc :: Rat -> Rat
lemc q | q < -1 = -1

| q > 1 = 1
| otherwise = q

9 / 15 Volume 23 (2009)



A coinductive approach to verified exact real number computation

Now we declare the data type τ(N):

type NAT alpha = Either () alpha
data Nat = ConsNat (NAT Nat)

For later use we define the successor operation and numerals on Nat:

suc :: Nat -> Nat
suc n = ConsNat (Right n)

num :: Int -> Nat
num n = if n <= 0 then ConsNat (Left ()) else suc (num (n-1))

The program suc can be extracted from a proof that N is closed under successor. Now we move
on to a more interesting part, the extracted programs of the axioms for the inductive predicate N
and the coinductive predicate C. Below, Sds stands for “signed digit stream”.

mapNAT :: (alpha -> beta) -> NAT alpha -> NAT beta
mapNAT = \f-> \z->

case z of {Left u -> Left () ; Right x -> Right (f x)}

itNat :: (NAT alpha -> alpha) -> Nat -> alpha
itNat = \step->
let {f = \n-> case n of {ConsNat z -> step (mapNAT f z)}} in f

type SDS alpha = (SD,alpha)
data Sds = ConsSds (SDS Sds)

mapSDS :: (alpha -> beta) -> SDS alpha -> SDS beta
mapSDS = \f-> \z-> case z of {(d,x) -> (d,f x)}

coitSds :: (alpha -> SDS alpha) -> alpha -> Sds
coitSds = \f-> \x-> ConsSds (mapSDS (coitSds f) (f x))

The type of the formula A(x) is

type Approx = Nat -> Rat

Finally, the programs extracted from Prop. 1 are

proplr :: Sds -> Approx
proplr = \a-> \n-> itNat proplrStep n a

proplrStep :: NAT (Sds -> Rat) -> Sds -> Rat
proplrStep = \z-> \a-> case z of
{Left u -> 0; Right ih -> case a of

{ConsSds (d,a’) -> (lema d + ih a’)/2}}

Proc. AVOCS 2009 10 / 15



ECEASST

proprl :: Approx -> Sds
proprl = coitSds proprlStep

proprlStep :: Approx -> SDS Approx
proprlStep = \f->

let d = lemb (f (num 2))
in (d, \n-> lemc (2 * f (suc n) - lema d))

5.3 Results

As an example, we compute the signed digit representation of 1√e ∈ I. Since

1
√

e
= e−

1
2 =

∞

∑
i=0

(−12 )
i

i!

and the series converges at an exponential rate we define

en :=
n

∑
i=0

(−12 )
i

i!
∈ Q

and obtain an infinite sequence e = (en)n∈N realising the formula A(
1√
e ). Feeding e into the

program proplr we obtain a realiser of C( 1√e ), i.e. a signed digit representation of
1√
e . In order

to display the stream in the usual Haskell format we coerce Sds into [SD].

e :: Approx
e n = sum [((-1/2)ˆi) / (fromIntegral (product [1..i]))

| i <- [0..(fromIntegral n’)]]
where n’ = nat2Int n

nat2Int :: Nat -> Int
nat2Int (ConsNat (Left ())) = 0
nat2Int (ConsNat (Right n)) = 1 + nat2Int n

sds2Stream :: Sds -> [SD]
sds2Stream (ConsSds (d,a)) = d : sds2Stream a

sde :: [SD]
sde = sds2Stream (proprl e)

*Main> take 100 sde
[P,Z,P,Z,N,P,Z,N,P,N,Z,Z,P,N,P,Z,N,Z,P,N,P,Z,Z,Z,Z,Z,N,Z,Z,P,
Z,N,P,Z,Z,Z,Z,N,Z,P,N,P,Z,N,Z,Z,Z,Z,P,N,Z,P,Z,Z,Z,Z,Z,Z,Z,N,
Z,P,Z,Z,Z,N,P,N,P,Z,N,Z,P,Z,Z,N,P,N,P,Z,N,P,N,Z,Z,P,Z,N,P,N,
P,N,P,N,P,N,Z,P,Z,N]

11 / 15 Volume 23 (2009)



A coinductive approach to verified exact real number computation

We can check that this stream is correct by computing the corresponding floating point approxi-
mation and comparing it with the result obtained by floating point arithmetic (ironically, relying
on the correctness of the latter).

list2Double :: [SD] -> Double
list2Double = foldr av 0 where

av d x = ((fromRational (lema d))+x)/2

*Main> exp (-0.5)
0.6065306597126334

*Main> list2Double (take 100 sde)
0.6065306597126334

6 Conclusion

We presented a method for extracting certified programs from constructive proofs. The method
is based on a variant of realizability that strictly separates the (abstract) mathematical model
from the data types the extracted program is dealing with. The latter are determined completely
by the propositional structure of formulas and proofs. This has the advantage that the abstract
mathematical structures do not need to be ‘constructivised’. In addition, formulas that do not
contain disjunctions are computationally meaningless and can therefore be taken as axioms as
long as they are true. This enormously reduces the burden of formalization and turns - in our
opinion - program extraction into a realistic method for the development of nontrivial certified
algorithms.

We used the problem of translating between different representations of real numbers as an
example to illustrate the method in general, and to show the use of inductive and coinductive
definitions in program extraction.

Currently, we are working on an extension of this work to the situation where not only real
numbers, but also real functions are coinductively represented and where the underlying do-
main is extended to arbitrary separable metric spaces or even more general structures [Ber09b,
Ber09a].

An important aspect of the program extraction method is the ability to import existing cer-
tified software. This is partly accounted for by the possibility to add statements as axioms for
which programs provably realising them are given. But as least as important is the possibility
to include existing trusted data structures (large integers exact rationals, etc.) together with effi-
cient (and certified) implementations of basic operations. It is possible to extend our approach in
this respect, for example, using a general theory of realisability based on equilogical spaces and
assemblies [BBS04].

The method of program extraction including inductive definitions is implemented for example
in the Minlog system [BBS+98]. Carrying out in Minlog case studies involving coinduction as
presented here requires an appropriate extension of the system. This is work in progress.

Proc. AVOCS 2009 12 / 15



ECEASST

Bibliography

[Agd] Agda. http://wiki.portal.chalmers.se/agda/.

[BB85] E. Bishop, D. Bridges. Constructive Analysis. Grundlehren der mathematischen
Wissenschaften 279. Springer, Berlin, Heidelberg, NewYork, Tokyo, 1985.

[BBS+98] H. Benl, U. Berger, H. Schwichtenberg, M. Seisenberger, W. Zuber. Proof theory
at work: Program development in the Minlog system. In Bibel and Schmitt (eds.),
Automated Deduction – A Basis for Applications. Applied Logic Series II, pp. 41–
71. Kluwer, Dordrecht, 1998.

[BBS04] A. Bauer, L. Birkedal, D. S. Scott. Equilogical spaces. Theor. Comput. Sci.
315(1):35–59, 2004.
doi:http://dx.doi.org/10.1016/j.tcs.2003.11.012

[Ber07] Y. Bertot. Affine functions and series with co-inductive real numbers.
Math. Struct. Comput. Sci. 17:37–63, 2007.

[Ber09a] U. Berger. From coinductive proofs to exact real arithmetic. In Grädel and Kahle
(eds.), Computer Science Logic. LNCS 5771, pp. 132–146. Springer, 2009.

[Ber09b] U. Berger. Realisability and Adequacy for (Co)induction. In Bauer et al. (eds.),
6th Int’l Conf. on Computability and Complexity in Analysis. Schloss Dagstuhl -
Leibniz-Zentrum fuer Informatik, Germany, Dagstuhl, Germany, 2009.
http://drops.dagstuhl.de/opus/volltexte/2009/2258

[Bez07] M. Bezem. The Software Model Checker Blast. Journal on Software Tools for Tech-
nology Transfer 9(5-6):505–525, 2007.

[BH08] U. Berger, T. Hou. Coinduction for Exact Real Number Computation. Theory of
Computing Systems 43:394–409, 2008.
doi:DOI: 10.1007/s00224-007-9017-6

[BRS+00] M. Balser, W. Reif, G. Schellhorn, K. Stenzel, A. Programmiermethodik. Formal
system development with KIV. In Fundamental Approaches to Software Engineer-
ing, number 1783 in LNCS. Pp. 363–366. Springer, 2000.

[BS07] J. Bradfield, C. Stirling. Modal mu-calculi. In Blackburn et al. (eds.), Handbook of
Modal Logic. Studies in Logic and Practical Reasoning 3, pp. 721–756. Elsevier,
2007.

[CD06] A. Ciaffaglione, P. Di Gianantonio. A certified, corecursive implementation of exact
real numbers. Theor. Comput. Sci. 351:39–51, 2006.

[Con86] R. Constable. Implementing Mathematics with the Nuprl Proof Development Sys-
tem. Prentice–Hall, New Jersey, 1986.

[Coq] The Coq Proof Assistant. http://coq.inria.fr/.

13 / 15 Volume 23 (2009)

http://wiki.portal.chalmers.se/agda/
http://dx.doi.org/http://dx.doi.org/10.1016/j.tcs.2003.11.012
http://drops.dagstuhl.de/opus/volltexte/2009/2258
http://dx.doi.org/DOI: 10.1007/s00224-007-9017-6
http://coq.inria.fr/


A coinductive approach to verified exact real number computation

[Dij75] E. Dijkstra. Guarded Commands, Nondeterminacy and Formal Derivation of Pro-
grams. Comm. ACM 18:453–457, 1975.

[Dij97] E. W. Dijkstra. A Discipline of Programming. Prentice Hall PTR, Upper Saddle
River, NJ, USA, 1997.

[DJ78] B. Dines, C. Jones. The Vienna Development Method: The Meta-Language.
LNCS 61. Springer, Berlin, Heidelberg, New York, 1978.

[EH02] A. Edalat, R. Heckmann. Computing with Real Numbers: I. The LFT Approach to
Real Number Computation; II. A Domain Framework for Computational Geometry.
In Barthe et al. (eds.), Applied Semantics - Lecture Notes from the International
Summer School, Caminha, Portugal. Pp. 193–267. Springer, 2002.

[Flo67] R. Floyd. Assigning meaning to Programs. In Mathematical Aspects of Computer
Science. Pp. 19–32. American Mathematical Society, 1967.

[GNSW07] H. Geuvers, M. Niqui, B. Spitters, F. Wiedijk. Constructive analysis, types and exact
real numbers. Math. Struct. Comput. Sci. 17(1):3–36, 2007.

[Gri81] D. Gries. The Science of Programming. Springer, 1981.

[vH67] J. van Heijenoort (ed.). From Frege to Gödel. A Source Book in Mathematical Logic
1879–1931. Harvard University Press, Cambridge, MA., 1967. Reprinted 1970.

[Hey56] A. Heyting. Intuitionism: An Introduction. North-Holland, Amsterdam. Third Re-
vised Edition 1971, 1956.

[Hoa97] T. Hoare. An Axiomatic Basis for Computer Programming. Comm. ACM 12:567–
580, 1997.

[HW03] J. Hughes, M. Warnier. The Coinductive Approach to Verifying Cryptographic Pro-
tocols. In Wirsing et al. (eds.), Recent Trends in Algebraic Development Techniques.
LNCS 2755, pp. 268–283. Springer, Berlin, 2003.

[JR97] B. Jacobs, J. Rutten. A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bul-
letin 62:222–259, 1997.

[Kle45] S. C. Kleene. On the interpretation of intuitionistic number theory. Jour. Symb. Logic
10:109–124, 1945.

[KMM00] M. Kaufmann, P. Manolios, J. S. Moore. Computer-Aided Reasoning: An Approach.
Kluwer, 2000.

[Kre59] G. Kreisel. Interpretation of analysis by means of constructive functionals of finite
types. Constructivity in Mathematics, pp. 101–128, 1959.

[ML84] P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

Proc. AVOCS 2009 14 / 15



ECEASST

[ME07] J. R. Marcial-Romero, M. H. Escardo. Semantics of a sequential language for exact
real-number computation. Theor. Comput. Sci. 379(1-2):120–141, 2007.

[Mil80] R. Milner. A Calculus of Communicating Systems. Springer, 1980.

[MP05] F. Miranda-Perea. Realizability for Monotone Clausular (Co)Inductive Definitions.
Electr. Notes in Theoret. Comput. Sci. 123:179–193, 2005.

[Mos99] L. S. Moss. Coalgebraic Logic. Annals of Pure and Applied Logic 96, 1999.

[NPW02] T. Nipkow, L. C. Paulson, M. Wenzel. Isabelle/HOL — A Proof Assistant for
Higher-Order Logic. LNCS 2283. Springer, 2002.

[ORSS98] S. Owre, J. Rushby, N. Shankar, D. Stringer-Calvert. PVS: An Experience Report.
In Hutter et al. (eds.), Applied Formal Methods—FM-Trends 98. Lecture Notes in
Computer Science 1641, pp. 338–345. Springer-Verlag, Boppard, Germany, oct
1998.
http://www.csl.sri.com/papers/fmtrends98/

[Pnu77] A. Pnueli. The Temporal Logic of Programs. In In Proc. 18th IEEE Symposium on
Foundation of Computer Science. LNCS 902, pp. 350–364. IEEE, 1977.

[Rut00] J. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science
249(1):3–80, 2000.

[Sch09] H. Schwichtenberg. Realizability interpretation of proofs in constructive analysis.
Theory Comput. Sys., to appear, 2009.

[Tat98] M. Tatsuta. Realizability of Monotone Coinductive Definitions and Its Application
to Program Synthesis. In Parikh (ed.), Mathematics of Program Construction. Lec-
ture Notes in Mathematics 1422, pp. 338–364. Springer, 1998.

[Tro73] A. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Anal-
ysis. Lecture Notes in Mathematics 344. Springer, 1973.

15 / 15 Volume 23 (2009)

http://www.csl.sri.com/papers/fmtrends98/

	Introduction
	Induction and coinduction
	Cauchy and signed digit representations of real numbers
	Program extraction: theory
	The programming language
	The object language
	Realisability

	Program extraction: applications
	Proofs
	Programs
	Results

	Conclusion