Hostname: page-component-cc8bf7c57-n7qbj Total loading time: 0 Render date: 2024-12-11T23:07:12.846Z Has data issue: false hasContentIssue false
  • English
  • Français

Affine functions and series with co-inductive real numbers

Published online by Cambridge University Press:  01 February 2007

YVES BERTOT
YVES BERTOT*
Affiliation:
INRIA, Sophia Antipolis, France Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We extend the work of A. Ciaffaglione and P. di Gianantonio on the mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits implemented as a co-inductive type. Four aspects are studied. The first concerns the proof that digit streams correspond to axiomatised real numbers when they are already present in the proof system. The second re-visits the definition of an addition function, looking at techniques to let the proof search engine perform the effective construction of an algorithm that is correct by construction. The third concerns the definition of a function to compute affine formulas with positive rational coefficients. This is an example where we need to combine co-recursion and recursion. Finally, the fourth aspect concerns the definition of a function to compute series, with an application on the series that is used to compute Euler's number e. All these experiments should be reproducible in any proof system that supports co-inductive types, co-recursion and general forms of terminating recursion; we used the COQ system (Dowek et al. 1993; Bertot and Castéran 2004; Giménez 1994).

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 17 , Issue 1 , February 2007 , pp. 37 - 63
Copyright
Copyright © Cambridge University Press 2007

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Bauer, A., Escardó, M. and Simpson, A. (2002) Comparing functional paradigms for exact real-number computation. In: Automata, languages and programming. Springer-Verlag Lecture Notes in Computer Science 2380489–500.Google Scholar
Bertot, Y. (2005) Filters on coinductive streams, an application to Eratosthenes' sieve. In: Urzyczyn, P. (ed.) Typed Lambda Calculi and Applications, TLCA 2005, Springer-Verlag 102–115.CrossRefGoogle Scholar
Bertot, Y. and Castéran, P. (2004) Interactive Theorem Proving and Program Development, Coq'Art: the Calculus of Inductive Constructions, Springer-Verlag.CrossRefGoogle Scholar
Boehm, H.-J., Cartwright, R., Riggle, M. and O'Donnell, M. J. (1986) Exact real arithmetic: A case study in higher order programming. In: LISP and Functional Programming 162–173.Google Scholar
Boldo, S. (2004) Preuves formelles en arithmétiques à virgule flottante, Ph.D. thesis, École Normale Sup'erieure de Lyon.Google Scholar
Boldo, S., Daumas, M., Moreau-Finot, C. and Théry, L. (2002) Computer validated proofs of a toolset for adaptable arithmetic. Submitted to Journal of the ACM.Google Scholar
Boutin, S. (1997) Using reflection to build efficient and certified decision procedures. In: Abadi, M. and Ito, T. (eds.) TACS'97. Springer-Verlag Lecture Notes in Computer Science 1281.Google Scholar
Ciaffaglione, A. and di Gianantonio, P. (2000) A coinductive approach to real numbers. In: Coquand, T., Dybjer, P., Nordström, B. and Smith, J. (eds.) Types 1999 Workshop, Lökeberg, Sweden. Springer-Verlag Lecture Notes in Computer Science 1956114–130.Google Scholar
Coquand, T. (1993) Infinite objects in Type Theory. In: Barendregt, H. and Nipkow, T. (eds.) Types for Proofs and Programs. Springer-Verlag Lecture Notes in Computer Science 80662–78.Google Scholar
Cruz-Filipe, L., Geuvers, H. and Wiedijk, F. (2004) C-corn, the constructive coq repository at nijmegen. In: Asperti, A., Bancerek, G. and Trybulec, A. (eds.) MKM. Springer-Verlag Lecture Notes in Computer Science 311988–103.Google Scholar
Daumas, M., Rideau, L. and Théry, L. (2001) A generic library of floating-point numbers and its application to exact computing. In: Boulton, R. J. and Jackson, P. B. (eds.) Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001. Springer-Verlag Lecture Notes in Computer Science 2152169–184.CrossRefGoogle Scholar
Delahaye, D. and Mayero, M. (2001) Field: une procédure de décision pour les nombres réels en coq. In: Proceedings of JFLA'2001, INRIA.Google Scholar
di Gianantonio, P. (1996) A golden ration notation for the real numbers. Technical Report CS-R9602, CWI, Amsterdam.Google Scholar
di Gianantonio, P. and Miculan, M. (2003) A unifying approach to recursive and co-recursive definitions. In: Geuvers, H. and Wiedijk, F. (eds.) Types for Proofs and Programs. Springer-Verlag Lecture Notes in Computer Science 2646148–161.CrossRefGoogle Scholar
Dowek, G., Felty, A., Herbelin, H., Huet, G., Murthy, C., Parent, C., Paulin-Mohring, C. and Werner, B. (1993) The Coq Proof Assistant User's Guide, Version 5.8, INRIA.Google Scholar
Edalat, A. and Potts, P. J. (1998) A new representation for exact real numbers. In: Brookes, S. and Mislove, M. (eds.) Electronic Notes in Theoretical Computer Science 6.Google Scholar
Gibbons, J. (2004) Streaming representation-changers. In: Kozen, D. and Shankland, C. (eds.) MPC. Springer-Verlag Lecture Notes in Computer Science 3125142–168.Google Scholar
Giménez, E. (1994) Codifying guarded definitions with recursive schemes. In: Dybjer, P., Nordström, B. and Smith, J. (eds.) Types for proofs and Programs. Springer-Verlag Lecture Notes in Computer Science 99639–59.Google Scholar
Gosper, R. W. (1972) HAKMEM, Item 101 B. MIT AI Laboratory Memo No.239. Available at http://www.inwap.com/pdp10/hbaker/hakmem/cf.html#item101b.Google Scholar
Hales, T. C. (2000) Cannonballs and honeycombs. Notices of the AMS 47 (4)440–449.Google Scholar
Hales, T. (2004) The flyspeck project fact sheet. Available at http://www.math.pitt.edu/~thales/flyspeck/index.htmlGoogle Scholar
Hanrot, G., Lefèvre, V., Pélissier, P. and Zimmermann, P. (2000) The mpfr library. Available at http://www.mpfr.org.Google Scholar
Harrison, J. (1996) Hol light: A tutorial introduction. In: Srivas, M. K. and Camilleri, A. J. (eds.) FMCAD. Springer-Verlag Lecture Notes in Computer Science 1166265–269.Google Scholar
Harrison, J. (1998) Theorem Proving with the Real Numbers, Springer-Verlag.CrossRefGoogle Scholar
Harrison, J. (2000) Formal verification of IA-64 division algorithms. In: Harrison, J. and Aagaard, M. (eds.) Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000. Springer-Verlag Lecture Notes in Computer Science 1869234–251.Google Scholar
IEEE (1987) IEEE standard for binary floating-point arithmetic. SIGPLAN Notices 22 (2)9–25.Google Scholar
Lambov, B. (2005) Reallib: an efficient implementation of exact real arithmetic. In: Grubba, T., Hertling, P., Tsuiki, H. and Weihrauch, K. (eds.) CCA 2005 – Second International Conference on Computability and Complexity in Analysis, August 25–29, 2005, Kyoto, Japan. Informatik Berichte 326-7/2005, Fern Universität Hagen, Germany 169–175.Google Scholar
Mahboubi, A. (2007) Implementing the Cylindrical Algebraic Decomposition inside the Coq system. Mathematical Structures in Computer Science, this issue.CrossRefGoogle Scholar
Mahboubi, A. and Pottier, L. (2002) Élimination des quantificateurs sur les réels en Coq. In: Journées Francophones des Langages Applicatifs, Anglet.Google Scholar
Mayero, M. (2001) Formalisation et automatisation de preuves en analyses réelle et numérique, Ph.D. thesis, Université Paris VI.Google Scholar
McLaughlin, S. and Harrison, J. (2005) A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) CADE-20: 20th International Conference on Automated Deduction, proceedings. Springer-Verlag Lecture Notes in Computer Science 3632295–314.CrossRefGoogle Scholar
Ménissier-Morain, V. (1994) Arithmétique exacte, conception, algorithmique et performances d'une implémentation informatique en précision arbitraire, Thèse, Université Paris 7.Google Scholar
Ménissier-Morain, V. (1995) Conception et algorithmique d'une représentation d'arithmétique réelle en précision arbitraire. In: Proceedings of the first conference on real numbers and computers.Google Scholar
Muller, J.-M. (1997) Elementary Functions, Algorithms and implementation, Birkhauser.CrossRefGoogle Scholar
Müller, N. T. (2005) Implementing exact real numbers efficiently. In: Grubba, T., Hertling, P., Tsuiki, H. and Weihrauch, K. (eds.) CCA 2005 – Second International Conference on Computability and Complexity in Analysis, August 25–29, 2005, Kyoto, Japan. Informatik Berichte 326–7/2005, Fern Universität Hagen, Germany 378.Google Scholar
Niqui, M. (2004) Formalising Exact Arithmetic, Representations, Algorithms, and Proofs, Ph.D. thesis, University of Nijmegen, ISBN 90-9018333-7.Google Scholar
Nordström, B. (1988) Terminating general recursion. BIT 28 605–619.CrossRefGoogle Scholar
Paulin-Mohring, C. (1993) Inductive Definitions in the System Coq – Rules and Properties. In: Bezem, M. and Groote, J.-F. (eds.) Proceedings of the conference Typed Lambda Calculi and Applications. Springer-Verlag Lecture Notes in Computer Science 664. (Also LIP research report 92-49.)Google Scholar
Russinoff, D. M. (1999) A Mechanically Checked Proof of IEEE Compliance of the AMD K5 Floating-Point Square Root Microcode. Formal Methods in System Design 14 (1)75–125.CrossRefGoogle Scholar
Vuillemin, J. E. (1990) Exact real computer arithmetic with continued fractions. IEEE Transactions on Computers 39 (8)1087–1105.CrossRefGoogle Scholar