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