1: \documentclass{mscs}
2: \usepackage{alltt}
3: \usepackage{amsmath,amsfonts,amssymb,amstext,eucal}
4: \setlength{\hfuzz}{2pt}
5: \usepackage{url}
6: \title{Affine functions and series with co-inductive real numbers}
7: \newcommand{\coq}{{\sc Coq}}
8: \author{Yves Bertot}
9: \date{November 2005}
10: \begin{document}
11: \maketitle
12: \begin{abstract}
13: We extend the work of A. Ciaffaglione and P. di Gianantonio on
14: mechanical verification of algorithms for exact computation on real numbers,
15: using infinite streams of digits implemented as a co-inductive type.
16: Four aspects are studied: the first aspect concerns the proof
17: that digit streams can be related to axiomatized real numbers when they
18: are already present in the proof system. The second aspect re-visits
19: the definition of an addition function, looking at techniques to let the
20: proof search engine
21: perform the effective construction of an algorithm that is correct by
22: construction. The third aspect concerns the definition of a
23: function to compute affine formulas with positive rational
24: coefficients. This is an example where we need to
25: combine co-recursion and recursion. The fourth aspect concerns the
26: definition of a function to compute series, with an application on the
27: series that is used to compute Euler's number \(e\). All these
28: experiments should be reproducible in any proof system that supports
29: co-inductive types, co-recursion and general forms of terminating
30: recursion. We used the \coq{} system \cite{coq,coqart,Gimenez94}.
31: \end{abstract}
32: \section{Introduction}
33: Several proof systems provide data-types to describe real numbers,
34: together with basic operations and theorems giving
35: an ordered, complete, and archimedian field
36: \cite{HOL-light,HarrisonThesis, mayero-thesis}. In the \coq{} system, several
37: approaches have been taken; depending on whether developers wanted to
38: adhere to pure constructive mathematics or more classical approaches.
39: In the classical approach, the type of real numbers is merely
40: ``axiomatized'', the existence of the type and the elementary
41: operations is assumed and the properties of these operations are
42: asserted as axioms. This approach has been used extensively to
43: provide a large collection of results, going all the way to the
44: description of trigonometric functions, calculus and the like.
45: However, because the type of real numbers is axiomatized, there is no
46: ``physical representation of numbers'' and the basic operations
47: correspond to no algorithm.
48:
49: In an alternative approach, a type of {\em constructive} numbers may be
50: defined as a data-type and the basic operations may
51: be described as algorithms manipulating elements of this data-type.
52: This approach is used for instance in C-CoRN
53: \cite{DBLP:conf/mkm/Cruz-FilipeGW04}.
54: A.~Ciaffaglione and P.~di~Gianantonio \cite{ciaffaglione.00} showed that
55: a well-known representation of real numbers as infinite sequences
56: of redundant digits could easily be implemented inside theorem provers
57: with co-inductive types. We say the digits are redundant
58: because several representation are possible for every number. In the
59: case of \cite{ciaffaglione.00} the representation is simply inspired
60: by the usual binary representation of fractional numbers and
61: made more redundant by adding the possibility to use a negative digit.
62: A.~Ciaffaglione and P.~di~Gianantonio then provide addition,
63: multiplication, and show that these operations enjoy the properties
64: that are expected from a constructive field of real numbers.
65:
66:
67: In our approach there is also an extra digit, but its meaning is
68: intermediary between the existing 0 and 1. Edalat and Potts \cite{edalat.98}
69: show that both approaches are special cases of a more general family of
70: representations based on {\em linear fractional transformations}.
71:
72: Once we have chosen the way to represent real numbers as a data-type,
73: we proceed by establishing a relation between this data-type and the
74: axiomatized type of real numbers. This is a departure from the
75: prescription of pure constructive mathematics, because we rely on the
76: non-constructive axioms of that theory to state the correctness of our
77: algorithms. Still, we also describe the relation between our representation
78: and constructive approaches to real numbers, by showing how infinite
79: sequences of digits can be produced from constructive views of Dedekind
80: cuts or Cauchy sequences.
81:
82: Once we have provided the basic data-type and its relation with the
83: axiomatized theory of real numbers, we proceed by defining an addition
84: function. We rely on proof search tools to
85: construct the addition algorithm: we only provide
86: guidelines for the construction of the algorithm, without actually describing
87: all 25 cases in the function. The correctness proof then consists
88: in showing that there is a morphism between the data-type and the
89: axiomatized type. Our contribution in this part is to show how to
90: use the proof search engine to construct a well formed addition function.
91:
92: We then focus on affine formulas combining two
93: real values with rational coefficients. For these more general
94: operations, we need to combine co-recursion and well-founded
95: recursion. We show that the function responsible for producing the
96: infinite stream of digits representing the result can be decomposed
97: in two recursive functions. One of the functions is a guarded
98: co-recursive function as proposed in \cite{Gimenez94}, the second
99: function is a well-founded recursive function as in \cite{nordstrom88}. Each
100: function satisfies a different form of constraint: the co-recursive
101: function does not need to be terminating, but it must produce at least
102: a digit at each recursive call, while the well-founded function does
103: not need to produce a digit at each recursive call, but it must
104: terminate. Our main contribution in this part is to show that some
105: functions that appear at first sight to be outside the expressive
106: power of guarded co-recursion can actually be modeled and proved
107: correct.
108:
109: In a fourth part, we focus on constructively converging infinite sums.
110: We show how to avoid having to consider the infinity of
111: terms that are parts of the sum. We exhibit a
112: framework that can be re-used from one series to the other. As
113: applications, we show how to compute the infinite stream representing
114: Euler's number \(e\) and to multiply two real numbers represented as
115: infinite streams of digits. In particular, the algorithm we obtain can be
116: executed directly using the reduction mechanism provided in \coq{} to
117: compute \(e\) to a great precision in a reasonable time.
118:
119: Our account stops here, although the experiments described in this paper
120: seem to open the door for a more complete study of real functions,
121: especially analytic functions.
122:
123: \section{Related work}
124: For numerical computation, real numbers are usually represented as
125: approximates using floating point numbers. These floating point
126: numbers are composed of a mantissa and an exponent, so that the
127: value of the least significant bit in the mantissa varies with the
128: exponent. Still both the exponent and the mantissa have a fixed size,
129: so that there is only a finite number of floating point numbers and real
130: values must be rounded to find the closest floating point numbers.
131: Floating-point based computations are thus only approximative and
132: errors stemming from successive rounding operations may accumulate to
133: the point that some computations can become grossly wrong
134: \cite{JMMuller}.
135:
136: In spite of their limitations, Floating-point numbers are used
137: extensively: most processors
138: directly provide an implementation of the elementary operations
139: (addition, subtraction, multiplication, division) according to a
140: standard that gives a precise mathematical meaning to the rounding
141: operations \cite{IEEE754}. This standard provides the basis to
142: implement computations with a guaranteed precision
143: \cite{JMMuller,MPFR}, sometimes with correctness proofs that can be
144: verified with the help of computer-aided proof tools
145: \cite{DauRidThe01, tphols2000-Harrison,Russinoff99,
146: Boldo04}. In particular, some approaches, named {\em expansions} make
147: it possible to increase drastically the number of representable numbers
148: by extending the length of the mantissa \cite{BolDauMorThe02}.
149:
150: An alternative to floating point and rounding concentrates on
151: data-structures that support exact computation.
152: Among the possible approaches, the best well-known are based
153: on continued fractions \cite{gosper.72, vuillemin.90} or
154: representations with mantissas that grow as needed
155: \cite{MenissierReals95}. In the latter case, the representation is
156: very close to the floating-point representations with rounding modes.
157: One way to understand this ``growing mantissa'' is to view it
158: as an infinite sequence of digits, where only a finite prefix is
159: known at any time. An introduction to exact real arithmetics
160: can be found in \cite{edalat.98}.
161: Implementations are provided in the setting of conventional programming
162: languages {\cite{DBLP:conf/cca/Lambov05,DBLP:conf/cca/Muller05}},
163: or in the setting of functional programming
164: {\cite{DBLP:conf/lfp/BoehmCRO86,menissier.94,BauerEscardoSimpson02}}.
165:
166: Formal proofs about computations on infinite data-structures are a
167: privileged ground for the use of co-inductive types
168: \cite{CoquandInfinite93,Gimenez94}. First experiments on the topic
169: of exact real number computations using co-inductive types were
170: performed by Ciaffaglione and di~Gianantonio {\cite{ciaffaglione.00}}
171: who showed that one could represent infinite sequences of digits with
172: co-inductive types and the basic operations of arithmetics (addition,
173: multiplication, comparison) with simple co-recursive functions, as
174: long as the set of digits was extended to allow for enough redundancy.
175: Niqui \cite{NiquiThesis} also studies the problems of modeling real
176: number arithmetic for use in formal proofs, providing a single point
177: of view to account for both continued fractions and infinite sequences of
178: digits. Our approach is very similar to Ciaffaglione and
179: di~Gianantonio's, it only differs in the collection of digits that we
180: consider.
181:
182: The example of combination of co-recursive functions and well-founded
183: recursive functions that we exhibit in our treatment of affine
184: formulas is related to work by di Gianantonio and Miculan
185: \cite{diGianantonioMiculan} and our own work on partial co-recursive
186: functions \cite{bertot05a}.
187:
188: Concerning the computation of series, we are aware through personal
189: communication that computations of \(e\) had already been done using the
190: real numbers as they are formalized in the C-CoRN library
191: \cite{DBLP:conf/mkm/Cruz-FilipeGW04}; it seems that co-inductive presentations
192: make it possible to achieve a higher efficiency. While the C-CoRN library
193: aims at providing a comprehensive study of constructive mathematics, our
194: work abandons some of the foundations of constructive mathematics:
195: we let our logical
196: reasoning depend on non-constructive arguments, although we do provide
197: algorithms working on concrete data-structure to represent real numbers and
198: the basic operations. We believe the algorithms we develop will be useful
199: even in the context of constructive mathematics, but the proofs of correctness
200: will probably have to be re-done.
201:
202: \section{Redundant digit representation for real numbers}
203: We are all used to the notation with a decimal point to represent
204: real numbers. For instance, we usually write a number between 0 and 1
205: as a string of the form \(0.1354647\cdots\) and we know that the
206: sequence of digits must be infinite for some numbers, actually all
207: those that are not of the form \(\frac{a}{10^b}\), where \(a\) and
208: \(b\) are positive integers. It is a bit less natural, but still easy
209: to understand, that all numbers can be represented by an infinite
210: sequence: for those that have a finite representation, it suffices to
211: add an infinite sequence of zeros. Moreover the number 1 can also be
212: represented by the sequence \(0.999\cdots\)
213:
214: When we know a prefix of one of these infinite sequences, we actually
215: know the number that is represented up to a certain precision. If the
216: prefix has length \(p\), we actually know precisely the bounds of an interval
217: of width \(\frac{1}{10^p}\) that contains the number. We are accustomed
218: to reasoning with these prefixes of infinite sequences and we expect
219: tools to return correct prefixes of an operation's output when this
220: operation has been fed with correct prefixes for the inputs.
221:
222: In the conventional representation, the number {\emph{ten}}
223: plays a special role:
224: it is the {\em base}. We can change the base and use digits that are
225: between 0 and the base. For instance, we can use {\emph{two}} as the base, so
226: that the digits are only 0 and 1. The number \(\frac{1}{2}\) can then
227: be represented by the sequence \(0.1000\cdots\) and the number 1 can
228: be represented by the sequence \(0.1111\cdots\). For a sequence
229: \(0.d_1d_2\cdots\), the number being represented is:
230: \[\sum_{i=1}^\infty \frac{d_i}{2^i}.\]
231: the following equalities hold:
232: \begin{eqnarray*}
233: 0.0s&=&\frac{0.s}{2}\\
234: 0.1s&=&\frac{0.s+1}{2}
235: \end{eqnarray*}
236: A prefix with \(p\) digits gives
237: an interval of width \(\frac{1}{2^p}\) that contains the number
238: represented by the infinite sequence. In the rest of this paper, we
239: will carry on using base 2 (but the set of
240: digits will change).
241:
242: For the computation of basic operations, the base-2 conventional
243: representation is not really well adapted. Here is an example that
244: exhibits the main flaw of this representation. The numbers
245: \(\frac{1}{3}\) and \(\frac{1}{6}\) add up to give \(\frac{1}{2}\).
246: However, the infinite sequences for these numbers are given in the
247: following equations:
248: \begin{eqnarray*}
249: \frac{1}{3}&=&0.01010101\cdots\\
250: \frac{1}{6}&=&0.00101010\cdots\\
251: \frac{1}{2}&=&0.10000000\cdots = 0.01111111\cdots
252: \end{eqnarray*}
253: The following reasoning steps justify the first equation:
254: \[
255: 0.01010101\cdots=\sum_{i=1}^\infty \frac{1}{2^{2i}}
256: =\frac{1}{1-\frac{1}{4}}-1=\frac{1}{3}\]
257:
258: Similar justifications can be used for the other equations.
259: If \(w\) is a prefix of \(0.0101\cdots\), then \(w\) is also the prefix
260: of all numbers between \(w00\cdots\) and \(w111\cdots\). These two
261: numbers are rational numbers of the form \(\frac{a}{2^b}\) and neither
262: can be equal to \(\frac{1}{3}\). Thus, we actually have
263: an interval of possible values that contains both values that are
264: smaller and values that are larger than \(\frac{1}{3}\). The same
265: property occurs for the representation of \(\frac{1}{6}\). When
266: considering the sum of values in the interval around \(\frac{1}{3}\)
267: and values in the interval around \(\frac{1}{6}\), the results are in
268: an interval that contains both values that are smaller and values that
269: are larger than \(\frac{1}{2}\). However, numbers of the form
270: \(0.1\cdots\) can only be larger than or equal to \(\frac{1}{2}\) and
271: numbers of the form \(0.0\cdots\) can only be smaller than or equal to
272: \(\frac{1}{2}\).
273: Thus, even if we know the inputs with a great precision, we must
274: indefinitely delay the decision and require more precision on the
275: input before choosing the first digit of the result: we need to know
276: the inputs with infinite precision before deciding the first digit of
277: the output.
278:
279: We solve this problem by adding a third digit in the notation. This
280: digit provides a way to express that the interval given by a prefix
281: has \(\frac{1}{2}\) in its interior. This new digit adds more
282: redundancy in the representation. We now have three digits, even
283: though we still work in base 2. We choose to name the three
284: digits {\tt L} (for {\em left}), {\tt R} (for {\em Right}), and
285: {\tt C} (for {\em center}).
286: \begin{itemize}
287: \item The digit {\tt L} is used like the digit \(0\). If \(x\) is
288: an infinite sequence of digits representing the number \(v\), the
289: sequence \({\tt L}x\) represents \(v/2\).
290: \item The digit {\tt R} is used like the digit \(1\). If \(x\) is
291: an infinite sequence of digits representing the number \(v\), the
292: sequence \({\tt R}x\) represents \(v/2+1/2\).
293: \item The digit {\tt C} is used with the following meaning: if \(x\) is
294: an infinite sequence of digits representing the number \(v\), the
295: sequence \({\tt C}x\) represents \(v/2+1/4\).
296: \end{itemize}
297: The fact that {\tt L} is like 0, {\tt R} is like 1, etc can also be
298: expressed using a function \(\alpha\) such that \(\alpha({\tt L})=0\),
299: \(\alpha({\tt R})=1\) and \(\alpha({\tt C})=\frac{1}{2}\). With this
300: function we can still interpret a digit sequence \(0.d_1d_2\cdots\) as
301: an an infinite sum:
302: \[\sum_{i=1}^\infty \frac{\alpha(d_i)}{2^i}\]
303:
304: From now on, we consider only numbers in the interval \([0,1]\) and we
305: drop the first characters ``0.'' when writing a sequence of digits.
306: We use the same notation for a sequence of digits and the
307: real number it
308: represents. In the same spirit, we use the same notation for a
309: digit \(d\) and the function it represents, the function that maps \(x\) to
310: \(\frac{x+\alpha(d)}{2}\). Last, we
311: associate the digits {\tt L}, {\tt R}, {\tt C} to the intervals
312: \([0,\frac{1}{2}]\), \([\frac{1}{2},1]\), and
313: \([\frac{1}{4},\frac{3}{4}]\), respectively. These interval are
314: called {\em basic intervals}.
315:
316:
317: The redundancy of the new digit gives a very simple property:
318: a number that can be written \({\tt
319: CL}x\) can also be written \({\tt LR}x\) and a number that
320: can be written \({\tt CR}x\) can also be written \({\tt RL}x\). This
321: property is used several times in this paper.
322:
323: \subsection{Formal details of infinite sequences and real numbers}
324: In our formalization, we benefit from theories that state the main
325: properties of natural numbers (type {\tt nat}), integers (type {\tt
326: Z}), and real numbers (the type is usually written {\tt R}, but in
327: this article we shall write it as {\tt Rdefinitions.R} to avoid
328: ambiguity with the ``digit'' {\tt R}). The two integer types come
329: with addition, subtraction, and multiplication, while the type of real
330: numbers is also equipped with division. The integer types are actually
331: described as inductive types and the basic operations are implemented
332: as recursive functions. For the real numbers, the existence of the
333: type, two constants 0 and 1, the operations, comparison predicates,
334: and the properties of these operations (associativity, distributivity,
335: inverse, etc.) are assumed. Among the assumed features, there is an
336: axiom that expresses completeness, which states that every bound and non-empty
337: subset of \(\mathbb{R}\) has a least upper bound in \(\mathbb{R}\).
338: This means that whenever we exhibit a property \(E\)
339: and prove that it is bound, we can construct a function that returns
340: its least upper bound. This completeness axiom is inherently non-constructive.
341: To be more precise, our work describes a collection of algorithms on
342: a representation of real numbers, in some sense a constructive of
343: real numbers, but many justifications of correctness, which rely on
344: the axiomatized real numbers, are non-constructive.
345:
346: The axiomatization
347: of real numbers also provides a few decision procedures. The decision
348: procedure {\tt field} \cite{del.may.2001} solves equalities between
349: rational expressions, occasionally leaving proof obligations to make
350: sure denominators are non-zero. The decision procedure {\tt fourier}
351: determines when a collection of in-equations concerning affine formulas
352: with rational coefficients is satisfiable.
353:
354: The type of digits is described as an enumerated type:
355: \begin{alltt}
356: Inductive idigit: Set := L | R | C.
357: \end{alltt}
358: We provide both a {\em numeric} interpretation (named {\tt alpha}) and a
359: {\em functional} interpretation (named {\tt lift}) to these digits. These
360: can be defined in {\coq} with the following text:
361:
362: \begin{alltt}
363: Definition alpha (d:idigit): Rdefinitions.R :=
364: match d with L => 0 | C => 1/2 | R => 1 end.
365:
366: Definition lift (d:idigit)(x:Rdefinitions.R) := (x+ alpha d)/2.
367: \end{alltt}
368: The type of infinite sequences of digits is based on a polymorphic
369: type of streams, which is defined as a co-inductive type using a declaration
370: with the following form:
371: \begin{alltt}
372: CoInductive stream (A:Set): Set := Cons: A -> stream A -> stream A.
373: \end{alltt}
374: This definition defines {\tt stream A} to be a data-type for any type
375: {\tt A}. It also defines the constructor {\tt Cons}, with the type
376: given in the definition. This definition is similar to a recursive
377: data-type definition in a conventional functional programming language.
378: In our mathematical notation, we will simply
379: write \(ds\) instead of {\tt Cons \(d\) \(s\)}. In {\coq} excerpts,
380: we will also use the notation \(d{\tt ::}s\).
381:
382: In proof systems, recursion is seldom unrestricted. In the {\coq} system,
383: it is mostly provided as a companion to inductive and co-inductive
384: data-structures. For inductive structures, the form of recursion that
385: is provided is called {\em structural} recursion, and it basically imposes
386: that a recursive function takes an element of inductive type as argument
387: and a recursive call can only be performed if the argument is
388: a sub-term of the initial argument. For co-inductive structures, the form
389: of recursion that is provided is called {\em guarded co-recursion}, and
390: it basically imposes that a co-recursive value must be
391: an element of a co-inductive type and that co-recursive calls can only be used
392: to produce sub-terms of the output. More general forms of recursion are
393: also provided, for instance {\em well-founded recursion}, where recursive
394: calls are allowed only if the argument of the recursive call is a predecessor
395: of the initial argument with respect to a relation that is known to be
396: well-founded (which intuitively means that this function contains no infinite
397: chain of predecessors). Well-founded recursion can actually be shown to
398: be a special case of structural recursion \cite{nordstrom88,moh93,coqart}.
399:
400: Co-recursive values need not be functions. For instance, 0 and 1 are
401: represented by the infinite sequences {\tt LLL\dots} and {\tt
402: RRR\dots}, these are defined as co-recursive values with the following
403: definition:
404: \begin{verbatim}
405: CoFixpoint zero: stream idigit := L::zero.
406:
407: CoFixpoint one: stream idigit := R::one.
408: \end{verbatim}
409: To relate infinite streams of digits with real numbers
410: we define a co-inductive relation.
411: \begin{verbatim}
412: CoInductive represents: stream idigit -> Rdefinitions.R -> Prop:=
413: repr: forall d s r,
414: represents s r -> 0 <= r <= 1 -> represents (d::s) (lift d r).
415: \end{verbatim}
416: This definition introduces both the two-place predicate {\tt represents}.
417: and a constructor, named {\tt repr}, which can be used as a theorem to
418: prove instances of this predicate. The statement of this theorem can
419: be read as ``for every {\tt s} and {\tt r}, if the proposition
420: {\tt represents s r} holds and the proposition {\tt 0 <= r <= 1} hold,
421: then the proposition {\tt represents (d::s) (lift d r)} holds''.
422: This relation really states that infinite streams are only used to
423: represent numbers between 0 and 1 and it confirms the correspondence
424: between the digits and their function interpretations.
425:
426: An alternative approach to relating sequences of digits and real numbers
427: is to build a function that maps an infinite sequence to a real value.
428: Every prefix of an infinite sequence corresponds to an interval that
429: contains all the values that could have the same prefix.
430: As the prefix grows, the new intervals are included in each other,
431: and the size is divided by 2 at each step, while the bounds remain rational.
432: We defined a function {\tt
433: bounds} to compute the interval corresponding to the prefix of a
434: given length for a given sequence. This function takes as
435: arguments a digit sequence and a number \(n\) and it computes the
436: bounds of an interval that contains all the real numbers whose
437: representation shares the same prefix of length \(n\). This function
438: is primitive recursive in \(n\) (in other words, it is structural recursive
439: with respect to the conventional representation of natural numbers as
440: an inductive type).
441: \begin{eqnarray*}
442: {\tt bounds}(\ldots, 0)&=&[0,1]\\
443: {\tt bounds}(ds, n+1)&=&[{\tt lift}~d~a,{\tt lift}~d~b]\quad\hbox{where}\quad{\tt bounds}(s, n)=[a,b]
444: \end{eqnarray*}
445: In practice, we do not manipulate real numbers in this function, but only
446: integers. The result of the function is a structure \(((a,b),k)\) such
447: that the interval is \([\frac{a}{2^k},\frac{b}{2^k}]\).
448:
449: We then define a function that maps a stream of digits to a sequence
450: of real numbers, which are the lower bounds of the intervals.
451: This function is called {\tt si\_un} and is defined by the following
452: text, where {\tt IZR} is the function that injects integers
453: in the type of real numbers.
454: \begin{verbatim}
455: Definition si_un (s:stream idigit) (n:nat): Rdefinitions.R :=
456: let (p,k) := bounds n s in let (a,b) := p in IZR a/IZR(2^k).
457: \end{verbatim}
458: We prove that for every \(d\), {\tt lift \(d\)} is monotonic, so that
459: {\tt si\_un \(s\)} is a growing sequence bounded by 1.
460: All this leads us to a proof that {\tt si\_un \(s\)} has a limit and
461: that this limit is in [0,1]. This makes it possible to define
462: the function {\tt real\_value} that associates an infinite sequence
463: of digits to the limit.
464:
465: We then prove that adding a digit in front of a sequence is the
466: same as using this digit as a function.
467: \begin{verbatim}
468: Theorem real_value_lift:
469: forall d s, real_value (d::s) = lift d (real_value s).
470: \end{verbatim}
471: This makes it possible to show that {\tt real\_value} and {\tt represents}
472: follow the same structure and to obtain the following theorem.
473: \begin{verbatim}
474: Theorem represents_real_value: forall s, represents s (real_value s).
475: \end{verbatim}
476: To complete the correspondence between the two notions we need to
477: express that the relation {\tt represents} is actually a function.
478: We do this by expressing that the distance between two possible
479: values represented by a sequence is smaller than \(\frac{1}{2^n}\):
480: This is proved by induction over \(n\).
481: \begin{verbatim}
482: Theorem represent_diff_2pow_n :
483: forall n x r1 r2, represents x r1 -> represents x r2 ->
484: -1/(2^n) <= r1 - r2 <= 1/(2^n).
485: \end{verbatim}
486: It is then easy to conclude with the following theorem.
487: \begin{verbatim}
488: Theorem represents_equal: forall s r, represents s r -> real_value s = r.
489: \end{verbatim}
490: We thus have two ways to express that a given sequence represents a
491: real number. The function {\tt real\_value} is more pleasant to use
492: in theorem statements, but the co-inductive property makes proofs more
493: elegant. Actually, all proofs of function correctness presented in
494: this paper are performed using a proof by co-induction based on
495: {\tt represents}, even though theorem statements are sometimes
496: expressed using {\tt real\_value}.
497:
498: This raises a third question: {\em given an arbitrary real number, is
499: there a digit stream that represents it?} The answer to this question is
500: related to question of constructivism in mathematics. If you have
501: a constructive description of your real number, then this may for instance
502: be tantamount
503: to a boolean predicate on rational numbers corresponding to this
504: number viewed as a Dedekind cut (a boolean predicate that is {\tt false}
505: for every rational number smaller than represented real number and
506: {\tt true} for any rational number that is larger).
507: We can produce the co-recursive value
508: corresponding to any boolean predicate using a co-recursive function. Here
509: is an example, where the rational numbers are viewed as pairs of
510: integers ({\tt p (\(a\), \(b\)) = true} means that the real number of interest
511: is smaller than or equal to \(\frac{a}{b}\)):
512: \begin{alltt}
513: CoFixpoint stream_of_cut (p:Z*Z->bool) : stream idigit :=
514: match p (1, 2) with
515: true => R::stream_of_cut (fun r => let (a,b) := r in p (a+b, 2*b))
516: | false => L::stream_of_cut (fun r => let (a,b) := r in p (a, 2*b))
517: end.
518: \end{alltt}
519: Alternatively, the real number of interest can be given by a Cauchy sequence
520: of rational numbers and a constructive proof that it satisfies the Cauchy
521: criterion. One way to describe Cauchy sequences is to fix a function
522: \(h\) from {\tt nat} to \(\mathbb{R}\), with its limit in 0 when the argument
523: goes to infinity. A Cauchy sequence may then be given by a function \(f\)
524: from {\tt Z} to \(\mathbb{Q}\) and the Cauchy criterion may be given
525: by a monotonic function \(g\) from {\tt Z} to {\tt Z} such that
526: \[\forall n~m~p, g(n)\leq m \wedge g(n)\leq p \Rightarrow |f(m)-f(p)| < h(n)\]
527: To construct the infinite list of digits for a given Cauchy sequence, we
528: simply need to repeat the following process:
529: \begin{enumerate}
530: \item compute the \(n\) first elements of the stream, this actually gives
531: an interval of width \(\frac{1}{2^n}\), compute the lower bound
532: \(b\) of this interval,
533: \item find the least \(n\) such that \(h(n)\leq \frac{1}{2^{n+3}}\),
534: \item compute \(f(g(n))\), we know that the distance between this value and
535: the sequence's limit is less than \(\frac{1}{2^{n+3}}\),
536: \item compute the value \(a=2^n(f(g(n))-b)\), this value is in [0,1]
537: by an invariant of the recursive process,
538: \item if \(a\leq \frac{3}{8}\), then we know that for every \(m\geq g(n)\),
539: \(f(m) \leq \frac{1}{2}\) and we choose the \(n+1\)th digit to be {\tt L},
540: \item if \(\frac{3}{8}\leq a \leq \frac{5}{8}\), then we know that for
541: every \(m\geq g(n)\), \(\frac{1}{4}\leq f(m)\leq \frac{3}{4}\), and we
542: choose the \(n+1\)th digit to be {\tt C},
543: \item if \(\frac{5}{8}\leq a\), then we know that for every \(m\geq g(n)\),
544: \(\frac{1}{2}\leq f(m)\), and we choose the {n+1}th digit to be
545: {\tt R}
546: \end{enumerate}
547: We contend that this technique gives a constructive process to associate
548: a sequence of digits to a sequence of rational numbers associated with
549: a constructive proof that this sequence satisfies the Cauchy criterion.
550:
551: When implementing this recursive process as a co-inductive function,
552: we propose to represent rational numbers with pairs of integers and
553: to replace comparisons of rational numbers with comparisons of integers.
554: It is also more convenient to restrict ourselves to the case where
555: \(h(n)=\frac{1}{2^n}\). In the recursive process, we do not need to
556: keep the list of the \(n\) first digits, we only need to know \(n\) and
557: the lower bound of the represented interval, these are given as arguments
558: to the co-recursive function:
559: \begin{alltt}
560: CoFixpoint stream_of_cauchy (f: Z -> Z*Z)(g: Z -> Z)
561: (n:Z)(b:Z*Z) : stream idigit :=
562: let (vn,vd) := f(g n) in
563: let (bn,bd) := b in
564: let (d, r) :=
565: if is_smaller (8*2^n*(vn*bd-vd*bn)) (3*vd*bd) then
566: (L,b)
567: else if is_smaller (8*2^n*(vn*bd-vd*bn)) (5*vd*bd) then
568: (C,(4*2^n*bn+bd,4*2^n*bd))
569: else (R, (2*2^n*bn+bd,2*2^n*bd)) in
570: let (new_bn, new_bd) := r in
571: d::stream_of_cauchy f g (n+1) (new_bn, new_bd).
572: \end{alltt}
573: The functions {\tt stream\_of\_cut} and {\tt stream\_of\_cauchy} are
574: only given here to show the feasibility of connecting streams of
575: digits with the usual notions of real number constructions,
576: but more efficient ways to handle rational numbers should
577: be used if these functions were to be used effectively, for instance
578: least common denominators should be computed between fraction numerators
579: and denominators.
580:
581: For an arbitrary real number between 0 and 1 given non constructively,
582: but known by its binary representation (an infinite sequence of 0 and 1
583: digits), this real number is simply represented by the corresponding
584: infinite stream where 0 is replaced with {\tt L} and 1 is replaced with
585: {\tt R}; however, the fact that the real number is given non constructively
586: is reflected by the fact that we can't write a co-recursive function that
587: produces the stream.
588:
589: \subsection{Addition}
590: It is well-known\footnote{P. Martin-L{\"o}f suggested to the author
591: that Cauchy had already devised an algorithm for addition in a similar
592: representation. Di Gianantonio refers to Cauchy and Leslie, but the
593: reference to Cauchy's work is wrong and the reference to Leslie could not
594: found at the time of writing.} that adding
595: two infinite sequences of redundant digits
596: can be described as a simple automaton that reads digits from both
597: inputs and produces digits at every recursive call. Two approaches
598: can be taken: either this automaton is understood as a program that
599: keeps a carry as it processes the inputs, or it can be viewed as a
600: program that performs a little look-ahead before outputting the result
601: and processing the rest, maybe with a slight modification of the first
602: digit in both inputs. The algorithm we describe follows the second
603: approach.
604:
605: Our algorithm has two parts. The first part is a function that
606: computes the arithmetic mean of two values (in other words, the
607: half-sum). The second part is a function that computes the double
608: of a value. The first algorithm maps two real numbers in \([0,1]\) to
609: a value in \([0,1]\). The doubling function only returns a meaningful
610: value when the input is smaller than or equal to \(\frac{1}{2}\).
611:
612: For the half-sum, the structure of the algorithm is as follows: if the
613: inputs have the form \(d_1d_2x\) and \(d_3d_4y\), then the algorithm
614: outputs a digit \(d\) and calls itself recursively with the new arguments
615: \(d_5x\) and \(d_6y\). Written as an equation, this yields the following
616: formula:
617: \[\hbox{\tt half\_sum}(d_1d_2x,d_3d_4y)=d({\tt half\_sum}(d_5x,d_6y)).\]
618:
619: Here is an example, suppose that \(d_1={\tt L}\) and \(d_3={\tt R}\),
620: in this case we can choose \(d={\tt C}\) and \(d_5=d_2\) and
621: \(d_6=d_4\), because the following equalities hold, using the
622: interpretations of digits as functions:
623: \begin{eqnarray*}
624: \hbox{\tt half\_sum}({\tt L}d_2x,{\tt R}d_4y)&=&
625: \frac{ {\tt L}d_2x+{\tt R}d_4y}{2}\\
626: &=&\frac{
627: \frac{d_2x}{2}+\frac{d_4y}{2}+\frac{1}{2}}
628: {2}\\
629: &=&\frac{d_2x}{4}+\frac{d_4y}{4}+\frac{1}{4}\\
630: &=&\frac{\frac{d_2x+d_4y}{2}}{2}+\frac{1}{4}\\
631: &=&{\tt C}(\hbox{\tt half\_sum}(d_2x,d_4y)).
632: \end{eqnarray*}
633: In this case, it is not necessary to scrutinize \(d_2\) and \(d_4\) to
634: decide the value of \(d\) and the arguments for the recursive call.
635: The equation can be re-written as
636: \[{\tt half\_sum}({\tt L}x,{\tt R}y)={\tt C}(\hbox{\tt half\_sum}(x,y)).\]
637:
638: Here is a second example where \(d_5\) and \(d_6\) are modified with
639: respect to \(d_2\) and \(d_4\). We suppose \(d_1={\tt C}\),
640: \(d_2={\tt L}\), and \(d_3={\tt L}\). In this case, the following
641: equalities hold:
642: \begin{eqnarray*}
643: {\hbox{\tt half\_sum}}({\tt CL}x,{\tt L}d_4y)
644: &=&\frac{\frac{x}{4}+\frac{1}{4}+\frac{d_4y}{2}}
645: {2}\\
646: &=&\frac{\frac{x}{2}+\frac{1}{2}+\frac{d_4y}{2}}
647: {2}\\
648: &=&{\tt L}(\hbox{\tt half\_sum}({\tt R}x,d_4y))
649: \end{eqnarray*}
650: In this case, it is not necessary to scrutinize \(d_4\), but the value
651: \(d_5\) is modified with respect to \(d_6\). The equation can be re-written
652: as
653: \[{\hbox{\tt half\_sum}}({\tt CL}x,{\tt L}y)=
654: {\tt L}(\hbox{\tt half\_sum}({\tt R}x,y)).\]
655:
656: If we had designed the algorithm to scrutinize two digits in each
657: input, there would be 81 cases, but since some cases can be handled
658: with a scrutiny of only the first digit in each input, or only one
659: digit in one of the inputs, the number of cases is brought down to 25
660: cases. Moreover, the exact behavior of the algorithm in each case can
661: be found automatically with the help of proof search procedures.
662:
663: \subsection{Automatic generation of function code}
664: We use the proof engine to actually construct the half-sum function by
665: making this program use its proof search facility to construct a
666: term with the right type, which should be
667: \begin{alltt}
668: stream idigit -> stream idigit -> stream idigit
669: \end{alltt}
670: We have enough control on the proof search mechanism to express
671: that the value of this type that we want to construct should be
672: a co-recursive function and that it should analyze the first digit
673: of the two input streams. This is simply done by stating that a
674: case analysis on these arguments should be performed. Doing a
675: case analysis on the first digit of the first input yields three
676: arguments, doing a case analysis on the first digit of the second argument
677: also gives three cases, so that there are at least nine cases to consider.
678: Some cases are easily solved directly, by simply finding an output
679: digit that makes the addition correct. For instance, if the two
680: inputs are \(dx\) and \(dy\) (in other words, they have the same
681: initial digit) then the result should be \(d({\tt half\_sum}~x~y)\).
682: This because the formula holds:
683: \[\frac{(\frac{x}{2}+\frac{\alpha(d)}{2})+(\frac{y}{2}+\frac{\alpha(d)}{2})}
684: {2}=\frac{\frac{x+y}{2}}{2}+\frac{\alpha(d)}{2}.\]
685: When no output digit can be computed to make the formula work directly,
686: more information is gathered from the inputs by imposing more case analysis.
687: When this case analysis is performed, we look at possible values of
688: the second digit of one of the inputs and we decide if we have enough
689: information to decide what the first output digit should be. This decision
690: is taken by performing some interval reasoning. If two digits of one of
691: the inputs are fixed, then this input belongs in an interval of length
692: \(\frac{1}{4}\), adding this interval with an input for which only one digit
693: is known, this gives an interval of length \(\frac{3}{4}\), taking the half
694: of this gives an interval of length \(\frac{3}{8}\). If the lower bound
695: of this interval is 0, \(\frac{1}{16}\), \(\frac{1}{8}\), \(\frac{1}{4}\),
696: \dots then we know what the output first digit can be, but if the
697: lower bound of this interval is \(\frac{3}{16}\) (this happens when one of
698: the inputs is {\tt LC}\(x\) and the other is {\tt C}\(y\)), then the upper
699: bound is \(\frac{9}{16}\) and we cannot conclude because
700: this interval may contains values lower than \(\frac{1}{4}\) (which should
701: not start with a {\tt C} or a {\tt R}) and values
702: larger than \(\frac{1}{2}\) (which should not start with a {\tt L}): for
703: these cases an extra case analysis on the second input is required.
704:
705: When the first digit of the output is fixed, we still need to decide what
706: the first digit of the arguments to recursive calls will be. This may
707: include a change with the initial second digit of the input. This
708: difference is often related to the equivalence between {\tt LR} and {\tt CL}
709: prefixes on the one hand and between {\tt RL} and {\tt CR} on the other
710: hand.
711:
712: For instance, if the first input has the form {\tt CL}\(x\) and the
713: second input has the form {\tt L}\(y\), the function can return
714: {\tt L}({\tt half\_sum}({\tt R}\(x\) \(y\))), because the half sum
715: of the two inputs is equivalent to the half sum of {\tt LR}\(x\) and
716: {\tt L}\(y\).
717:
718: To determine the first digits of inputs in recursive calls, we must
719: first respect an important rules: variables that represent sub-streams
720: should appear behind the same number of digits in the input pattern and
721: in the output pattern. This rules comes from the fact that the real number
722: represented by these variables is divided by 2 every time a digit is added
723: in front of it. If we want the half-sum equation to be satisfied we must
724: make sure that the number of divisions by 2 is preserved between the inputs
725: and the output. Thus, we can only prescribe the
726: first digit of one the arguments
727: to the co-recursive call of {\tt half\_sum} if the corresponding input had
728: two digits in the input pattern.
729:
730: To determine what first digit can be used for the recursive call on an
731: argument, the proof search procedure compares the lower bound of the
732: output as prescribed by its first digit to the lower bound of possible results
733: that we can predict from the shape of the input patterns.
734: In the example, the lower bound of the output as prescribed by the first
735: digit {\tt L} is 0, the lower bound predicted from the half-sum of
736: {\tt CL}\(x\) and {\tt L}\(y\) is \(\frac{1}{8}\). The discrepancy must be
737: resolved by making sure that the sum of all the digits
738: appearing as head of recursive call
739: arguments adds up to \(\frac{1}{2}\) (which does fit with a target
740: \(\frac{1}{8}\) since we are computing a half-sum and place the output's
741: first digit {\tt L} in front). Here there is only one
742: digit available, and we can only choose its value to be {\tt R}.
743:
744: Although the half-sum function is obtained by mechanical means to be
745: correct by construction, its type is only
746: \begin{alltt}
747: stream idigit -> stream idigit -> stream idigit
748: \end{alltt}
749: This type does not express what the function does.
750: We need to add a theorem to state that it has the right behavior with
751: respect to the real numbers represented by the inputs and outputs. The
752: statement has the following shape.
753: \begin{verbatim}
754: Theorem half_sum_correct :
755: forall x y u v, represents x u -> represents y v ->
756: represents (half_sum x y) ((u + v)/2).
757: \end{verbatim}
758: The proof of this statement relies on a proof by co-induction: we assume
759: that the statement is already satisfied
760: for any output stream that is a strict sub-stream of the current output and
761: we show that this is enough to prove the result for the current output.
762: The proof analyzes the behavior of the {\tt half\_sum}
763: function and explores all the 25 cases that were found at the
764: time the function was constructed. In all cases, it is a simple matter
765: to verify the equality between the algebraic formula corresponding to
766: the half-sum of the inputs and the output pattern present in the
767: {\tt half\_sum} function, using a tactic named {\tt field} \cite{del.may.2001}
768: that solves equalities between rational expressions in a field;
769: a second statement that needs to be verified is
770: that the half-sum of the inputs does belong to [0,1] if the two inputs do,
771: this is easily done using a tactic named {\tt fourier} that solves affine
772: comparisons between real values with rational coefficients.
773:
774: We believe that our definition technique can easily be reproduced
775: for different sets of digits or for other simple binary operations
776: like subtraction.
777:
778: \subsection{Multiplication by 2}
779: We also need to provide a
780: function to multiply the output of {\tt half\_sum} by 2.
781: This function is based on
782: the following remarks.
783:
784: \begin{itemize}
785: \item The double of a number of the form \({\tt L}x\) is simply \(x\),
786: \item The double of a number of the form \({\tt R}x\) is either 1
787: or outside the interval [0,1],
788: \item The double of a number of the form \({\tt C}x\) is a number
789: of the form \({\tt R}x'\) where \(x'\) is the double of
790: \(x\) (hence the algorithm exhibits a co-recursive call).
791: \end{itemize}
792:
793: Here is the formal definition:
794: \begin{verbatim}
795: Cofixpoint mult2 (v:stream idigit): stream idigit :=
796: match v with L::x => x | C::x => R::mult2 x | R::x => one end.
797: \end{verbatim}
798:
799: The correctness of this function is expressed with the following statement:
800: \begin{verbatim}
801: Theorem mult2_correct : forall x u,
802: 0 <= u <= 1/2 -> represents x u -> represents (mult2 x)(2*u).
803: \end{verbatim}
804: Please note that this theorem explicitly states that the result value
805: is specified correctly only when the input is
806: smaller than \(\frac{1}{2}\).
807: \subsection{Subtraction}
808: In this section we discuss several approaches to subtraction. One
809: first approach uses a few intermediary functions. The first
810: intermediary function mimics the opposite function. Of course the
811: opposite function cannot be defined from [0,1] to [0,1], but
812: we can define the function
813: that maps \(x\) to \(1-x\). Here is the general definition, where we
814: name the function {\tt minus\_aux}:
815: \begin{eqnarray*}
816: \hbox{\tt minus\_aux}({\tt L} (x)) &=& {\tt R}(\hbox{\tt minus\_aux}(x))\\
817: \hbox{\tt minus\_aux}({\tt C} (x)) &=& {\tt C}(\hbox{\tt minus\_aux}(x))\\
818: \hbox{\tt minus\_aux}({\tt R} (x)) &=& {\tt L}(\hbox{\tt minus\_aux}(x))
819: \end{eqnarray*}
820: These equations are justified through simple computations. For instance,
821: the last equation is justified with the following reasoning steps:
822: \begin{eqnarray*}
823: \hbox{\tt minus\_aux}({\tt R} (x)) &=&
824: 1-(\frac{x}{2}+\frac{1}{2})\\
825: &=& \frac{1}{2}-\frac{x}{2}\\
826: &=& \frac{1}{2}(1-x)\\
827: &=& {\tt L}({\tt minus\_aux}(x))
828: \end{eqnarray*}
829:
830: Combining {\tt minus\_aux} with addition, we can easily compute the
831: binary function that maps \(x\) and \(y\) to \(1+x-y\). Of course, this function
832: returns a meaningful result only when \(x\) is smaller than \(y\).
833:
834: Alternatively, we can combine
835: {\tt minus\_aux} with {\tt half\_sum} to have a function that maps
836: \(x\) and \(y\) to
837: \(\frac{1+x-y}{2}\). Now, if we really want to have a subtraction, we can
838: remove the \(\frac{1}{2}\) offset. We use another auxiliary function,
839: which we name
840: {\tt minus\_half} and is defined by the following equations:
841: \begin{eqnarray*}
842: \hbox{\tt minus\_half}({\tt R} x) &=& {\tt L} x\\
843: \hbox{\tt minus\_half}({\tt L} x) &=& {\tt zero}\\
844: \hbox{\tt minus\_half}({\tt C} x) &=& {\tt L}(\hbox{\tt minus\_half}(x))
845: \end{eqnarray*}
846: The first of these equations is trivial to justify. The second is justified by the
847: fact that the only value inside \([0,\frac{1}{2}]\) for which \(x-\frac{1}{2}\) belongs
848: to \([0,1]\) is \(\frac{1}{2}\) and the result is 0 in this case. The third equation
849: is justified by the following reasoning steps:
850: \begin{eqnarray*}
851: \hbox{\tt minus\_half}({\tt C} x) &=& \frac{x}{2}+\frac{1}{4} - \frac{1}{2}\\
852: &=&\frac{x}{2}-\frac{1}{4}\\
853: &=&\frac{x-\frac{1}{2}}{2}\\
854: &=&{\tt L}(\hbox{\tt minus\_half}(x))
855: \end{eqnarray*}
856: \section{Parameterized affine operations}
857: In this section, we study another approach to addition, with the encoding
858: of a more general function that computes affine formulas in two real
859: values with rational coefficients. More precisely, we want to compute
860: the value
861: \[\frac{a}{a'}x+\frac{b}{b'}y+\frac{c}{c'}\]
862: When \(a\), \(b\), \(c\) are non-negative integers and \(a'\), \(b'\),
863: \(c'\)
864: are positive integers (\(a\), \(b\), \(c\) may be null, but not
865: the others), and \(x\) and \(y\) are real numbers, given as infinite
866: sequences of digits.
867:
868: The interpretation of digits as affine functions (using our function
869: {\tt lift}) makes them a special case of what Edalat and Potts call {\em
870: Linear Fractional Transformations} \cite{edalat.98}. They actually show that
871: a more general form of two argument transform can be programed on this
872: form of real number transformation, namely the computation of the
873: following transform, called a {\em M{\"o}bius transform}, where \(a\), \(b\), etc.
874: are integers:
875: \[\frac{axy +bx+cy+d}{exy+fx+gy+h}.\]
876: Studying only affine formulas correspond to restricting the general study
877: proposed by Edalat and Potts to the case of where \(e\), \(f\), and \(g\)
878: are 0. A good reason to study separately the restricted case is that the
879: formal proofs stay inside the realm of proofs about equalities and
880: comparisons of affine formulas with rational coefficients, a realm for which
881: automatic proof tools exist at the time of writing this article, while
882: verifying the correctness of the general M{\"o}bius transform requires
883: incursions
884: into the realm of proofs about equalities and comparisons of polynomial
885: formulas, a domain for which proof procedures are only under development
886: \cite{MahboubiPottier2002,mclaughlin-harrison,Mahboubi06}.
887:
888: \subsection{Main structure of the algorithm}
889: Choosing the digits of the result is based on the following remarks:
890: \begin{enumerate}
891: \item Even without observing \(x\) and \(y\), we already know that
892: they are between \(0\) and \(1\). The result lies between
893: the extrema
894: \[\frac{c}{c'}\qquad \hbox{and} \qquad \frac{ab'c'+a'bc'+abc'}{a'b'c'}.\]
895: \item\label{corec} if the extrema belong to the same basic interval,
896: it is possible to produce a digit and perform a co-recursive call with a
897: new affine formula. In this sense, the output does not depend on reading
898: more digits from the input and the algorithm can be described as a streaming
899: algorithm in the sense of \cite{DBLP:conf/mpc/Gibbons04}.
900: \item \label{rec} If the extrema are badly placed, we cannot choose an
901: interval associated to a digit that is sure to contain the result.
902: In this case, we scrutinize \(x\) and \(y\) and observe their first
903: digit. As a result, we obtain a new estimate of the interval that
904: may contain the result, whose size is half the previous size. We
905: can then perform a recursive call with a new affine formula. In the
906: long run, we are forced to get to a situation where the extrema are
907: inside a basic interval and a co-recursive call can be performed.
908: In fact, this
909: condition is guaranteed as soon as the distance between extrema is
910: shorter than \(1/4\).
911: \end{enumerate}
912:
913: Let us study two examples. In the first example, suppose that the
914: property \(\frac{c}{c'}\ge 1/2\) holds. We know that the result is larger
915: than \(1/2\) and we can produce a {\tt R} digit. The following
916: computation takes place:
917: \begin{eqnarray*}
918: \frac{a}{a'}x+\frac{b}{b'}y+\frac{c}{c'}&=&
919: {\tt R}(2\times(\frac{a}{a'}x+\frac{b}{b'}y+\frac{c}{c'})-1)\\
920: &=&R(\frac{2a}{a'}x+\frac{2b}{b'}y+\frac{2c-c'}{c'})
921: \end{eqnarray*}
922: There is a recursive call with a new affine formula, where all the
923: coefficient are positive integers or non-negative integers as required.
924:
925: In a second example, suppose that the properties \(x={\tt L}x'\) and
926: \(y={\tt R}y'\) hold. The following computation can take place:
927: \begin{eqnarray*}
928: \frac{a}{a'}x+\frac{b}{b'}y+\frac{c}{c'}&=&
929: (\frac{a}{a'}\frac{x'}{2})+(\frac{b}{b'}\frac{y'+1}{2})+\frac{c}{c'}\\
930: &=&\frac{a}{2a'}x'+\frac{b}{2b'}y'+\frac{bc'+2b'c}{2b'c'}
931: \end{eqnarray*}
932: Here again, we can have a recursive call with a new affine formula,
933: no digit has been produced (therefore the recursive call cannot be a
934: co-recursive call) but the distance between the extrema in the new
935: formula is \(a/2a'+b/2b'\), the half of \(a/a'+b/b'\), which was the
936: distance between extrema for the initial affine formula.
937:
938: \subsection{Formal details for affine formulas}
939: When providing the formal description of the recursive algorithm for
940: the computation of affine formulas, we need to pay attention to
941: the following two important aspects:
942: \begin{enumerate}
943: \item The function needs to be partial, because we must ensure the
944: sign conditions on the coefficients of the affine formula,
945: \item Not all recursive calls are acceptable co-recursive calls, because
946: recursive calls after the consumption of digits from the two input
947: streams are associated to no production of an output digit.
948: \end{enumerate}
949: We define a record type named {\tt affine\_data} that collects the eight
950: elements of an affine formula and a predicate named
951: {\tt positive\_coefficients} that states that the
952: coefficients satisfy the sign conditions.
953:
954: The computation is then represented by a main function called
955: {\tt axbyc} to compute the affine formula. This function has a dependent
956: type: it takes as first argument an affine formula and as second argument
957: a proof that its coefficients satisfy the sign conditions.
958: \begin{verbatim}
959: axbyc: forall x: affine_data, positive_coefficients x -> stream idigit.
960: \end{verbatim}
961: This function is defined as a co-recursive function. The constraints
962: on recursive programming impose that this function can only perform the
963: recursive calls that are associated to the production of a digit in the
964: output (phase~\ref{corec} in the previous section). We need to define an
965: auxiliary function, not a co-recursive
966: one, which takes charge of the recursive calls that are only associated
967: to the consumption of digits from the input streams (phase~\ref{rec} in
968: the previous section).
969:
970: The auxiliary function is named {\tt axbyc\_rec}. It takes as arguments
971: an affine formula and a proof that it satisfies the predicate
972: {\tt positive\_coefficients}. It returns an equivalent affine formula,
973: one for which the decision of producing the next output digit
974: can be taken. This is represented by the fact that output of this
975: function is in a type with three constructors,
976: called {\tt caseR}, {\tt caseL}, or {\tt caseC}. Each constructor
977: contains as first field the new affine formula, as second field a proof
978: that this new formula satisfies the sign conditions. The next field
979: (for the constructors {\tt caseR} and {\tt caseL})
980: or the next two fields (for the constructor {\tt caseC}) express that the
981: right interval conditions are satisfied to output a digit, The last field
982: is a proof that the new affine formula is equivalent to the initial one.
983:
984: The recursive structure of the function {\tt axbyc\_rec} is based on
985: well-founded recursion. More precisely, it relies on the fact that
986: the distance between extrema decreases at each recursive step. This
987: can be translated into an integer formula that decreases while remaining
988: positive. When this integer formula is 0, we can prove that one of the
989: interval conditions to output a digit is necessarily satisfied.
990:
991:
992: Two other collections of auxiliary function perform the elementary operations.
993: Functions named {\tt prod\_R}, {\tt prod\_L}, and {\tt prod\_C} perform
994: the coefficients transformations that should be performed after producing
995: an output digit. For instance {\tt prod\_R} maps the affine formula
996: \[\frac{a}{a'}x+\frac{b}{b'}y+\frac{c}{c'}\]
997: to the formula
998: \[\frac{2a}{a'}x+\frac{2b}{b'}y+\frac{2c-c'}{c'}\]
999: as we already justified in the first example of the previous section.
1000:
1001: The lemmas named {\tt A.prod\_R\_pos}, {\tt A.prod\_L\_pos}, and
1002: {\tt A.prod\_C\_pos} ensure that the functions {\tt prod\_R}, {\tt prod\_L}
1003: and {\tt prod\_C} preserve the sign conditions on the coefficients,
1004: respectively. These lemmas rely on the interval conditions produced
1005: by {\tt axbyc\_rec}. For instance, for {\tt A.prod\_R\_pos} the extra interval
1006: condition is \(c'\leq 2c\). In our description of the co-recursive
1007: function, this information is transferred from {\tt axbyc\_rec} to
1008: {\tt A.prod\_R\_pos} with the help of a variable named {\tt Hc}.
1009:
1010: With these auxiliary functions, the main function can be given a simple
1011: structure:
1012: \begin{verbatim}
1013: CoFixpoint axbyc (x:affine_data)
1014: (h:positive_coefficients x):stream idigit :=
1015: match axbyc_rec x h with
1016: caseR y Hpos Hc _ =>
1017: R::(axbyc (prod_R y) (A.prod_R_pos y Hpos Hc))
1018: | caseL y Hpos _ _ =>
1019: L::(axbyc (prod_L y) (A.prod_L_pos y Hpos))
1020: | caseC y Hpos H1 H2 _ =>
1021: C::(axbyc (prod_C y) (A.prod_C_pos y Hpos H2))
1022: end.
1023: \end{verbatim}
1024:
1025: With the help of the function {\tt real\_value} we can also define
1026: a function {\tt af\_real\_value} that maps any affine formula
1027: represented by an element of {\tt affine\_data} to the real number it
1028: represents. This function is used to express the correctness of our
1029: algorithm to compute the affine formula:
1030: \begin{verbatim}
1031: axbyc_correct:
1032: forall x, forall H :positive_coefficients x,
1033: 0 <= af_real_value x <= 1 ->
1034: real_value (axbyc x H) = af_real_value x.
1035: \end{verbatim}
1036: This proof is based on a lemma that is proved by co-induction:
1037: \begin{verbatim}
1038: axbyc_correct_aux :
1039: forall x:affine_data, forall H :positive_coefficients x,
1040: 0 <= (af_real_value x) <= 1 ->
1041: represents (axbyc x H) (af_real_value x).
1042: \end{verbatim}
1043: This algorithm is interesting because it provides ways to
1044: add two real numbers, to multiply them by rational numbers, and to encode
1045: rational numbers as real numbers. Having formalized this algorithm may
1046: make the direct implementation of addition described earlier seem useless.
1047: It is not useless, because the direct implementation of addition makes no
1048: use of dependent types, proof arguments, or well-founded recursion. As a
1049: result, the direct addition can be executed directly inside the theorem
1050: prover using its internal reduction mechanism, while the affine formula
1051: computation can only be executed outside the theorem prover as extracted
1052: code. Algorithms that can be reduced inside the proof system may play
1053: a role in reflection-based proof procedures \cite{Boutin97b}.
1054: \section{Computing series}
1055: A series is an infinite sum of values. Knowing how to compute series
1056: can help in computing famous constants like \(e\) (Euler's number) or
1057: \(\pi\) and
1058: to implement the multiplication of two real numbers.
1059: \subsection{Main structure of the algorithm}
1060: We consider the problem of computing values of the form
1061: \(\sum_{i=0}^{\infty} a_i\) where the \(a_i\) terms are real numbers.
1062:
1063: Studying series is very close to
1064: studying converging sequences, since it is enough to consider the
1065: sequence \(u_n=\sum_{i=0}^n a_i\). Each element of the sequence can
1066: then be computed as a finite combination of additions.
1067:
1068: Computing the first \(p\) digits of the limit
1069: means computing the limit up to a precision of \(2^{-p}\). If we know that a
1070: given element \(u_n\) is closer than \(2^{-(p+1)}\) to the
1071: limit and if we can compute \(u_n\) to a precision better than
1072: \(2^{-{p+1}}\), then we are able to compute the limit to the
1073: required precision. In other words, if we know that
1074: \(|\sum_{i=n}^{\infty} a_i|\) is smaller than \(2^{-(p+1)}\), and we
1075: know a value \(v\) whose distance to \(\sum_{i=0}^n a_i\) is less
1076: than \(2^{-(p+1)}\), then we also know that the distance of \(v\) to
1077: is less than \(\sum_{i=0}^{\infty} a_i\). In fact, we need to use
1078: slightly stronger precisions, because an interval of length \(2^{-p}\) rarely
1079: fits in one of the intervals representable by finite sequences of digits.
1080: Still, this approach shows that we can avoid considering the whole infinite sum
1081: to produce the first digit of the output.
1082:
1083:
1084: We restrict our study to series whose convergence is described
1085: constructively by a function \(\mu\) that satisfies the following properties:
1086: \[\forall m.\quad n\le m \Rightarrow |\sum_{i=m}^\infty a_i| < \mu(n)
1087: \qquad \lim_{n\rightarrow\infty}\mu(n)=0\]
1088: We actually formalize the computation of a function \(f\) that has the
1089: following informal specification:
1090: \[ f(x,y,n) = x + y\times\sum_{i=n}^\infty a_i,\]
1091: where \(x\) is a real number, \(y\) is a rational number,
1092: and \(n\) is a natural number. Intuitively, \(y\) represents the inverse of
1093: the precision that is reached in the computation (\(y=2^p\)).
1094: If we know that \(y\times\mu(n)\leq \frac{1}{16}\) and we know \(x\)
1095: to a precision of three digits then we are able
1096: to choose the first digit \(d\) of \(x+y\sum_{i=n}^\infty a_i\).
1097: We can then perform the following computation
1098: \[f(x,y,n)=d\,f(2x-\alpha(d),2y,n),\]
1099: In most cases, we also have \(x=dx'\) for some \(x'\), and
1100: the value \(2x-\alpha(d)\) is simply
1101: represented by \(x'\). If \(y\times\mu(n)> \frac{1}{16}\), we compute
1102: a new value \(\phi(y,n)\) such that \(y\times\mu(\phi(y,n))\leq\frac{1}{16}\).
1103: This value is bound to exist because \(\mu\) converges to 0 at infinity.
1104: We can then proceed with the following step.
1105: \[f(x,y,n)=f(x+y\times\sum_{i=n}^{\phi(y,n)-1}a_i,y,\phi(y,n))\]
1106:
1107: In practice we first compute \(\phi(y,n)\), then we compute
1108: \(v=x+y\times \sum_{i=n}^{\phi(y,n)-1} a_i\) by repeated
1109: binary additions. Let us assume that
1110: \(\rho\) is defined as \(y\times \sum_{i=\phi(y,n)}^\infty a_i\).
1111: The number we want to compute is \(v+\rho\) and we know that
1112: \(|\rho|\leq \frac{1}{16}\). We then perform the following case
1113: analysis:
1114: \begin{enumerate}
1115: \item If \(v\) has the form \({\tt R}v'\), and \(v'\) has the form
1116: {\tt R}\(v''\), \({\tt C}v''\), {\tt LC\(v''\)}, or {\tt LR\(v''\)},
1117: we can deduce that \(v\geq 9/16\), therefore
1118: \(v+\rho \geq \frac{1}{2}\) and the first
1119: digit of the result can be {\tt R}. The
1120: result is \({\tt R}(f(v',2y,\phi(y,n)))\).
1121: \item If \(v\) has the form {\tt C}\(v'\), where \(v'\) has the form
1122: {\tt C}\(v''\), {\tt LC}\(v''\), {\tt LR}\(v''\), {\tt RL}\(v''\), or
1123: {\tt RC}\(v''\), then we are certain that
1124: \(\frac{5}{16}\leq v\leq \frac{11}{16}\), therefore \(\frac{1}{4}\leq v+\rho
1125: \leq \frac{3}{4}\), the result is \({\tt C}(f(v',2y,\phi(y,n)))\).
1126: \item If \(v\) has the form {\tt L}\(v'\), where \(v'\) has the form
1127: {\tt L}\(v''\), {\tt C}\(v''\), {\tt RL}\(v''\), {\tt RC}\(v''\), then we
1128: are certain that \(v\leq \frac{7}{16}\) and \(v+\rho\leq \frac{1}{2}\)
1129: the result is \({\tt L}(f(v',2y,\phi(y,n)))\).
1130: \item if \(v\) has the form {\tt RLL}\(v''\), then \(v\) could also be
1131: represented using {\tt CRL}\(v''\) and this case is already
1132: considered above. The same goes for the cases {\tt LRR}, {\tt CLL}, and
1133: {\tt CRR}, using {\tt CLR}, {\tt LRL}, and {\tt RLR} as respective
1134: alternatives.
1135: \end{enumerate}
1136: The number \(\phi(y,n)\) is chosen so that
1137: \(y\times\mu(\phi(y,n))\leq \frac{1}{16}\) because \(\frac{1}{16}\)
1138: is the shortest distance between the bounds of the intervals
1139: for {\tt CLC} and {\tt C}, {\tt RLC} and {\tt R}, or {\tt LRC} and {\tt L}.
1140: Computing \(\phi(y,n)\) and \(\sum_{i=n}^{\phi(y,n)-1}a_i\)
1141: depends on the series being studied. Because recursive calls to
1142: \(f\) always have \(2y\) and \(\phi(y,n)\) as arguments, we can also
1143: assume
1144: that the invariant \(y\times\mu(n)<\frac{1}{8}\) is maintained through
1145: recursive calls.
1146: \subsection{Series with positive terms}
1147: When we know that the \(a_i\) terms are all positive, we do not need
1148: to use \(\frac{1}{16}\) to bound the infinite remainder of the series.
1149: The computation technique can be simplified.
1150:
1151: We first compute \(\phi(y,n)\) so that \(y\times\mu(\phi(y,n))
1152: \leq \frac{1}{8}\)
1153: and \(v=x+\sum_{i=n}^{\phi(y,n)-1}\).
1154: In what follows, let \(\rho\) be defined as
1155: \(y \times\sum_{i=\phi(y,n)}^\infty a_i\); we know \(|\rho|\leq \frac{1}{8}\).
1156: We perform the following case analysis:
1157: \begin{enumerate}
1158: \item if \(v\) has the form \({\tt R} v'\), we are sure that the
1159: result is larger than or equal to \(1/2\), the result is \({\tt
1160: R}(f(v',2y,\phi(y,n)))\).
1161: \item if \(v\) has the form \({\tt C} v'\) but not \({\tt CR} v'\),
1162: we can deduce \(v \in [\frac{1}{4},\frac{5}{8}]\) and
1163: \(v+\rho\in[\frac{1}{4},\frac{3}{4}]\), the result is
1164: \({\tt C}(f(v',2y,\phi(y,n)))\).
1165: \item if \(v\) has the form \({\tt L}v'\), but not
1166: \({\tt LR}v'\), we can deduce \(v\in [0,\frac{3}{8}]\) and
1167: \(v+\rho\in [0,\frac{1}{2}]\).
1168: The result is \({\tt L}(f(v',2y,\phi(y,n)))\).
1169: \item if \(v\) has the form \({\tt CR}v''\) or \({\tt LR}v''\), we can use
1170: the equivalences with \({\tt RL}v''\) and \({\tt CL}v''\),
1171: respectively, to switch to one of the previous cases.
1172: \end{enumerate}
1173: For positive series, there is also an invariant: \(y\times\mu(n)\) is
1174: always smaller than \(\frac{1}{4}\). This invariant plays a role
1175: in the correctness proofs.
1176: \subsection{Formal details of positive series}
1177: We programmed the general treatment of positive series in a
1178: higher-order function that is easy to re-use from one series to the
1179: other.
1180: \begin{verbatim}
1181: Definition series_body (A:Set)
1182: (f: stream idigit -> A -> stream idigit)
1183: (x: stream idigit) (a:A): stream idigit :=
1184: let (d,x') := v in
1185: match d with
1186: R => R::f v' a
1187: | L => match v' with R::v'' => C::f (L::v'') a | _ => L::f v' a end
1188: | C => match v' with R::v'' => R::f (L::v'') a | _ => C::f v' a end
1189: end.
1190: \end{verbatim}
1191: The type {\tt A} should make it possible to compute
1192: the values
1193: \(y\) and \(n\) used in our informal presentation. This will be made
1194: clearer in the next examples.
1195: \subsection{Application to computing $e$}
1196: The number \(e\) is defined by the formula
1197: \[e=\sum_{k=0}^\infty \frac{1}{k!}.\]
1198: Of course, this number is larger than 2, but we only want to compute
1199: its fractional part, so that we actually compute
1200: \(\sum_{k=2}^\infty \frac{1}{k!}\).
1201: The following properties are easy to obtain, by remembering that
1202: \(n!n^{k-n}<k!\) for every \(k \ge n\), therefore
1203: \[0 < \sum_{k=n}^{\infty} \frac{1}{k!} < \frac{1}{(n-1)!(n-1)}.\]
1204: For this series, we choose \(\mu(n)\) to be the value
1205: \(\frac{1}{(n-1)!(n-1)}\). As soon as
1206: \(2<n\), we have \(\mu(n+1)<\frac{\mu(n)}{2}\). This implies the
1207: following property:
1208: \[\forall n, y, 0 < y \wedge 2 < n \wedge y\times\mu(n) < \frac{1}{4}
1209: \Rightarrow \phi(y,n) \leq n+1.\]
1210: Thus, it is never necessary to absorb more than one term from the
1211: infinite sum into \(x\) at each co-recursive call.
1212:
1213: the type {\tt A} that appears in our use of {\tt series\_body} is a
1214: triple type. The triple given as argument has the form
1215: \((y,n,\theta)\), where \(\theta\) is the precomputed value
1216: \(\theta=(n-1)!\). This invariant is maintained through recursive calls
1217: so that factorials are not recomputed from scratch each time. Here the
1218: \(\mu\) function is given by the formula
1219: \[\mu(n)=\frac{1}{(n-1)!(n-1)}=\frac{1}{\theta\times(n-1)},\]
1220: and computing
1221: \(\phi(y,n)\) is easy, because we know that this value is always
1222: \(n\) or \(n+1\). To decide whether \(\phi(y,n)=n\),
1223: we simply need to compare
1224: \(y\times\frac{1}{\theta(n-1)}\) with \(\frac{1}{8}\),
1225: in other words to compare \(8y\) with \(\mu'=\frac{1}{\mu}=\theta(n-1)\).
1226: In the following code, {\tt rat\_to\_stream} builds the infinite sequence
1227: of digits for a rational number given by its numerator and denominator.
1228: \begin{verbatim}
1229: CoFixpoint e_series (x:stream idigit)(s :Z*Z*Z) :stream idigit :=
1230: let (aux, theta) := s in let (y, n) := aux in let mu' := theta*(n-1) in
1231: let (v, phi, theta') :=
1232: if Z_le_gt_dec (8*y) mu' then
1233: mk_triple x n theta
1234: else
1235: let theta' := mu'+theta in
1236: mk_triple (x+(rat_to_stream y theta'))(n+1) theta' in
1237: series_body _ e_series v (2*y, phi, theta').
1238: \end{verbatim}
1239:
1240: To express that this function computes correctly the series, we
1241: rely on a predicate {\tt infinite\_sum} which takes a function \(f\)
1242: from {\tt Z} to {\tt R} and a value \(v\) in {\tt R} as arguments
1243: and means {\em \(\sum_{i=0}^\infty f(i)\) converges and the limit is \(v\).}
1244: The correctness statement has the following shape:
1245:
1246: \begin{verbatim}
1247: Theorem e_correct1 :
1248: forall v vr r y n,
1249: 4 * y <= fact(n-1) * (n-1) -> 2 <= n -> 1 <= y ->
1250: represents v vr ->
1251: infinite_sum (fun i => 1/IZR(fact (i+n))) r ->
1252: vr + (IZR y)*r <= 1 ->
1253: represents (e_series v (y, n, fact(n-1))) (vr+(IZR y)*r).
1254: \end{verbatim}
1255: This statement is obfuscated by the simultaneous use of two
1256: types of numbers and the function {\tt IZR} is the natural injection
1257: of integers into the type of real numbers.
1258: In this statement the formula \verb+fact(n-1)*(n-1)+ represents the
1259: inverse of \(\mu(n)\) and the formula
1260: \verb"4 * y <= fact(n-1) * (n-1)"
1261: corresponds to the invariant of the series.
1262: Note that this theorem
1263: expresses that the series is correctly computed only if the series
1264: really converges to a value that is smaller than or equal to 1. The
1265: proof that the series converges has to be done independently.
1266:
1267:
1268: We initialize the recursive computation with \(x=\frac{1}{2}\),
1269: \(y=1\) and \(n=3\), so that the invariant on \(y\times\mu(n)\) is
1270: satisfied.
1271: \begin{verbatim}
1272: Definition number_e_minus2: stream idigit :=
1273: e_series (rat_to_stream 1 2+rat_to_stream 1 6) (1, 4, 6).
1274: \end{verbatim}
1275: The correctness theorem then makes it possible to obtain the
1276: following statement:
1277: \begin{verbatim}
1278: Theorem e_correct :
1279: infinite_sum (fun i => 1/IZR(fact(i+2)))(real_value number_e_minus2).
1280: \end{verbatim}
1281: This statement really means \(\sum_{i=2}^\infty \frac{1}{i!}={\tt number\_e\_minus2} \).
1282:
1283: The value {\tt number\_e\_minus2} can then be used to construct
1284: rational approximations of \(e-2\), using the {\tt bounds} function.
1285: Actually, given \(n\)
1286: we compute \((a,b,k)\) so that
1287: \[\frac{a}{2^k} \leq e - 2 \leq \frac{b}{2^k}\qquad \frac{b}{2^k} -
1288: \frac{a}{2^k} = \frac{1}{2^n}.\]
1289: For \(n=320\), this computation takes approximately a minute with the
1290: standard version of
1291: \coq{}\footnote{Coq version {\tt 8.0pl2}, Intel Pentium(R) M 1700Mhz.}.
1292: These functions can be used in proof procedures
1293: to compute approximations
1294: of \(e\).
1295: The code can also be extracted both to Ocaml and to Haskell. Running
1296: the Ocaml extracted code, we
1297: can compute 2000 redundant digits of \(e-2\) in about a minute.
1298: \subsection{Multiplication as a special case of series}
1299: When \(u\) is the infinite sequence \(d_1d_2\dots\) and then \(uu'\)
1300: is a series:
1301: \[uu'=\sum_{i=1}^{\infty}\frac{\alpha(d_i)u'}{2^i}.\]
1302: This is a series where all terms are positive. Moreover, two
1303: simplifications can be made with respect to the general approach.
1304: First, while \(y\) is multiplied by 2 at every recursive call, \(a_i\)
1305: contains a divisor that is also multiplied by \(2\), so that the two
1306: multiplications by 2 cancel out. Second, it is reasonable to simply
1307: consume one element from the infinite sum at each recursive call, without
1308: scrutinizing the value of \(u'\). If this approach is
1309: followed, the argument \(y\) is not necessary anymore: only the digits
1310: \(d_i\) and \(u'\) are needed. We can re-use the general function
1311: {\tt series\_body} in the following manner:
1312: \begin{alltt}
1313: Definition sum_mult_d (d:idigit) (u v:stream idigit) :=
1314: match d with L => u | C => u+L::L::v | R => u+L::v end.
1315:
1316: CoFixpoint mult_a (x:stream idigit)(p:stream idigit*stream idigit)
1317: : stream idigit :=
1318: let (u,v) := p in
1319: match u with d::w => series_body _ mult_a (sum_mult_d d x v)(w,v) end.
1320: \end{alltt}
1321: The function {\tt mult\_a \(x\) \((u,u')\)} computes \(x+uu'\) only when
1322: \(uu' < \frac{1}{4}\) (here again, we see the invariant of the general
1323: approach). To obtain multiplication for the general case, we divide
1324: the second operand by \(4\) before the multiplication and we multiply
1325: the result by \(4\).
1326: Here is a naive implementation:
1327: \begin{verbatim}
1328: Definition mult (x y:stream idigit): stream idigit :=
1329: mult2(mult2(mult_a zero (x,L::L::y))).
1330: \end{verbatim}
1331: The following theorem can then proved and verified formally:
1332: \begin{verbatim}
1333: mult_correct
1334: : forall (x y: stream idigit) (vx vy: Rdefinitions.R),
1335: represents x vx -> represents y vy -> represents (x*y)(vx*vy)
1336: \end{verbatim}
1337: In this statement the notation {\tt x * y} represents our
1338: multiplication as an operation on infinite digit streams, while the
1339: notation
1340: {\tt vx * vy} represents the multiplication of real numbers, as they
1341: are axiomatized in the {\coq} system.
1342:
1343: It turns out
1344: our approach of multiplication, based on series, yields an
1345: implementation of multiplication that is very close to the
1346: implementation in \cite{ciaffaglione.00}.
1347:
1348: We can also try this multiplication directly inside \coq{}, for
1349: instance, we can compute \((e-2)^2\). With the current standard
1350: version of {\coq} no effort is made to
1351: exploit possible sharing in the lazy computation of values, so that
1352: the same value may be computed several times. For this reason, we
1353: cannot compute this number to a high precision as easily as for
1354: \(e-2\). For example, our few experiments showed that it takes
1355: approximately 10 seconds to compute an approximation with an accuracy
1356: of \(\frac{1}{2^{30}}\) digits and a minute
1357: to compute the approximation with an accuracy of \(\frac{1}{2^{50}}\).
1358:
1359: \section{Conclusion}
1360: The work described in this paper is available on the Internet at the
1361: following address:
1362: \begin{verbatim}
1363: http://hal.inria.fr/inria-00001171
1364: \end{verbatim}
1365:
1366: This is both an extension and a departure
1367: from the work of Ciaffaglione and di~Gianantonio. We chose to work
1368: with an extra digit that is interpreted as \(\frac{1}{2}\) instead of
1369: \(-1\). We believe algorithms are easier to design in this approach
1370: and easier to prove correct, but this approach is less well adapted to
1371: expanding to the full real line.
1372:
1373: We believe the choice to rely on an existing axiomatization of real numbers
1374: was instrumental in making the proofs in this experiment quicker to
1375: obtain. In particular, we relied on a collection of automatic decision
1376: procedures for equalities between polynomials and sets of in-equalities
1377: between affine formulas. This axiomatization relies on classical mathematics,
1378: and we don't know in which respect the decision procedures rely on these
1379: these classical axioms and in which respect they could be re-implemented
1380: in constructive mathematics. Admittedly, we only provide algorithms to
1381: compute representations of real values that are constructively definable.
1382: We believe that our experiment should be reproducible in the context of
1383: constructive mathematics, but it concentrated on the presentation of real
1384: numbers that provided the most complete theory of functions. The question
1385: of constructive or non-constructive mathematics was secondary in this
1386: experiment.
1387:
1388: It is characteristic that the definition of series appears to be more
1389: basic than multiplication, but this is simply due to the fact that
1390: the digit-based representation of numbers already is naturally interpretable
1391: as a series and this structure is preserved by multiplication thanks to
1392: distributivity.
1393:
1394: Now that we have a multiplication for our representation of real
1395: numbers, we can consider the task of implementing other functions,
1396: like division and analytic functions. For division, we expect
1397: to use a method of range reduction: to compute \(\frac{x}{y}\) we
1398: should compute \(\frac{x}{2^ky}\) or \(\frac{x}{y}-k\) where \(k\)
1399: should be chosen so that the result is inside \([0,1]\) but finding
1400: the right value for \(k\) is only possible when we have a constructive
1401: way to prove that \(y\) is non zero.
1402:
1403: An alternative approach to division is provided if we generalize our
1404: approach to affine formulas to consider M{\"o}bius transforms (already
1405: studied in \cite{edalat.98}):
1406: \[(x,y)\mapsto \frac{axy + bx + cy +d}{exy+fx+gy+h}.\]
1407: However, we suspect that the proofs of correctness for these
1408: transformations are less easy to automatize, because they do not rely
1409: only on affine formulas (which are easily treated with the
1410: Fourier-Motzkin decision procedure.
1411:
1412: One of the interesting features of this experiment is that some series
1413: can be computed directly inside the theorem prover. This is an important
1414: feature, if a proof requires that we produce an accurate approximation of
1415: a series value.
1416:
1417: Concerning the computation of mathematical constants, we already have all the
1418: ingredients to compute \(\pi\) using a Machin formula (we used
1419: the formula \(\frac{\pi}{4}=\arctan(\frac{1}{2})+\arctan(\frac{1}{3})\) which
1420: can easily be proved and computed as the sum of two series).
1421:
1422: Several questions will be studied in the future. First, the choice of
1423: a digit set is arbitrary. We already experimented we a digit set that
1424: contains only two digits, corresponding to intervals \([0,\frac{2}{3}]\)
1425: and \([\frac{1}{3},1]\); although some functions seem to be simpler (because
1426: there are less cases to consider, for instance when considering affine
1427: formulas) other problems arise because equalities between patterns do not
1428: exist for short patterns (thus we cannot as easily mimic the equality
1429: \({\tt CL} = {\tt LR}\)). di~Gianantonio also studied a two-digit
1430: representation and he proposes to work with
1431: intervals whose length is based on the golden number
1432: \cite{diGianantonioGolden96}. However, the price
1433: to pay is that we now need to solve a polynomial system of degree 2 to
1434: determine whether a given value belongs to one of the basic intervals, again
1435: formal proofs in this setting are made more complex because we are not
1436: in the real of affine formulas anymore.
1437:
1438: In the long run, we wish to choose digit sets that are closer to the
1439: bound integers that are usually handled in computers, so that regular
1440: integer addition, subtraction, multiplication, and comparison or even
1441: bitwise operations can be used to establish the basic
1442: relations between various digits.
1443:
1444: The second important question is related to the efficiency of co-recursive
1445: computation inside the theorem prover. While recent evolutions of the \coq{}
1446: system brought drastic improvements in the computation of recursive functions,
1447: it is not certain that the co-recursive question is as well treated. In
1448: particular, lazy computation is needed to achieve reasonable speeds, while
1449: the current version of {\coq} may only implement call-by-name. This
1450: question is particularly difficult because the reduction mechanism also needs
1451: to retain the property of strong normalization for non-closed terms.
1452:
1453: Eventually, we hope to achieve the development of a reasonably efficient
1454: and formally verified library for mathematical computation. We believe this
1455: will be a stepping stone for more ambitious projects like the Flyspeck
1456: project\cite{Hales00,hales-flyspeck}.
1457:
1458: \bibliographystyle{apalike}
1459: \bibliography{a,aspecific}
1460: \end{document}
1461:
1462: % LocalWords: Coq Mhz Ocaml mult Motzkin Machin vn vd bn bd dx repr
1463: % LocalWords: dy bius axy cy exy fx gy ab'c a'bc abc a'b'c bc b'c axbyc caseR
1464: % LocalWords: caseL caseC pos Hc af RLL CRL LRR CLL CRR CLR LRL RLR CLC RLC uu
1465: % LocalWords: LRC vx vy ky aspecific Ciaffaglione di Gianantonio archimedian
1466: % LocalWords: CoRN Edalat Niqui Gianantonio's Miculan RL nat Rdefinitions ds
1467: % LocalWords: fourier idigit CoInductive LLL RRR si un IZR CoFixpoint bool
1468: % LocalWords: cauchy
1469: