×

The world’s shortest correct exact real arithmetic program? (English) Zbl 1386.68150

The difference between double precision floating point and exact real number computation is well described on the fourth page of the paper. When computing sin(1e200*pi), the former results in a value near 1, whereas the latter gives correctly the exact result of 0. Exact real number arithmetic is difficult, algorithms are often more subtle than their traditional counterparts and not always studied to the same extent.
The application of formal methods in exact real number computation puts the reliability of these algorithms on a new level. In this paper the author presents what is supposed to be the world’s shortest correct exact real arithmetic program. Correct means here concretely that the program is verified using the PVS system. The choice of system is discussed comparing it to Coq and Isabelle/HOL. PVS is used mainly since it contains libraries related to the work and since it is a non-constructive system. In further sections the representation of exact real numbers is presented, then issues are discussed of how to compute sin, cos, and log as Taylor series (after the functions are transformed so that the arguments are moved into an area where these series converge fast). The PVS proof consists of 500 theorems and over 60000 lines of code. The appendix contains in three pages the verified Haskell program.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
65G20 Algorithms with automatic result verification
68N18 Functional programming and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] J.-C. Bajard, M. Ercegovac, L. Imbert, F. Rico, Fast evaluation of elementary functions with combined shift-and-add and polynomial methods, in: RNC 4, 2000, pp. 75-87.; J.-C. Bajard, M. Ercegovac, L. Imbert, F. Rico, Fast evaluation of elementary functions with combined shift-and-add and polynomial methods, in: RNC 4, 2000, pp. 75-87.
[2] Barthe, G.; Courtieu, P., Efficient reasoning about executable specifications in Coq, (TPHOLs 2002. TPHOLs 2002, LNCS, vol. 2410 (2002), Springer-Verlag), 31-46 · Zbl 1013.68539
[3] Bauer, A.; Kavkler, I., Implementing real numbers with RZ, Electronic Notes in Theoretical Computer Science, 202, 365-384 (2008) · Zbl 1262.03076
[4] Coq Development Team, The Coq proof assistant reference manual version 8.0, Technical report, INRIA, April 2004, http://coq.inria.fr/doc/main.html; Coq Development Team, The Coq proof assistant reference manual version 8.0, Technical report, INRIA, April 2004, http://coq.inria.fr/doc/main.html
[5] M. Daumas, G. Melquiond, C. Muñoz, Guaranteed proofs using interval arithmetic, in: ARITH 17, 2005, pp. 188-195.; M. Daumas, G. Melquiond, C. Muñoz, Guaranteed proofs using interval arithmetic, in: ARITH 17, 2005, pp. 188-195.
[6] Gowland, P.; Lester, D., A survey of exact arithmetic implementations, (Proceedings of the 4th International Workshop. Proceedings of the 4th International Workshop, CCA 2000 (2000), Springer-Verlag) · Zbl 0985.65043
[7] D. Lester, Using PVS to validate the inverse trigonometric functions of an exact arithmetic, in: Proceedings of the Seminar on Numerical Software with Result Verification, Dagstuhl, Germany, 2003, pp. 259-273,.; D. Lester, Using PVS to validate the inverse trigonometric functions of an exact arithmetic, in: Proceedings of the Seminar on Numerical Software with Result Verification, Dagstuhl, Germany, 2003, pp. 259-273,. · Zbl 1126.68351
[8] Lester, D.; Gowland, G., Using PVS to validate the algorithms of an exact arithmetic, Theoretical Computer Science, 291, 203-218 (2003) · Zbl 1064.68005
[9] V. Ménissier, Arithmétique Exacte, PhD thesis, Université Pierre et Marie Curie, Paris, December 1994.; V. Ménissier, Arithmétique Exacte, PhD thesis, Université Pierre et Marie Curie, Paris, December 1994.
[10] Muller, J.-M., Elementary Functions (1997), Birkhauser
[11] N. Muller, The iRRAM: Exact arithmetic in C++, CCA2000, 2000, pp. 222-252.; N. Muller, The iRRAM: Exact arithmetic in C++, CCA2000, 2000, pp. 222-252. · Zbl 0985.65523
[12] C. Muñoz, D. Lester, Real number calculations and theorem proving, in: TPHOLs 18, 2005, pp. 239-254.; C. Muñoz, D. Lester, Real number calculations and theorem proving, in: TPHOLs 18, 2005, pp. 239-254.
[13] M. Niqui, Formalising exact arithmetic, PhD thesis, Nijmegen University, 2004.; M. Niqui, Formalising exact arithmetic, PhD thesis, Nijmegen University, 2004. · Zbl 1113.68404
[14] Owre, S.; Rushby, J. M.; Shankar, N., PVS: A prototype verification system, (CADE 11. CADE 11, LNAI, vol. 607 (1992), Springer-Verlag), 748-752
[15] Paulson, L. C., Isabelle: A Generic Theorem Prover, LNCS, vol. 828 (1994) · Zbl 0825.68059
[16] Pour-El, M. B.; Richards, J. I., Computability in Analysis and Physics (1989), Springer-Verlag · Zbl 0678.03027
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.