This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Verified Real Number Calculations: A Library for Interval Arithmetic
February 2009 (vol. 58 no. 2)
pp. 226-237
Marc Daumas, ELIAUS, UPVD, Perpignan
David Lester, University of Manchester, Manchester
Céar Muñoz, National Institute of Aerospace, Hampton
Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or proof assistant in a convenient and highly automated as well as interactive way. First, we formally establish upper and lower bounds for elementary functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations take place in an algebraic setting. In order to reduce the dependency effect of interval arithmetic, we integrate two techniques: interval splitting and Taylor series expansions. This pragmatic approach has been developed, and formally verified, in a theorem prover. The formal development also includes a set of customizable strategies to automate proofs involving explicit calculations over real numbers. Our ultimate goal is to provide guaranteed proofs of numerical properties with minimal human theorem-prover interaction.

[1] Information Management and Technology Division, Patriot Missile Defense: Software Problem Led to System Failure at Dhahran, Saudi Arabia, US General Accounting Office, Report B-247094, http://www.fas.org/spp/starwars/gaoim92026.htm , 1992.
[2] J.-L. Lions et al., “Ariane 5 Flight 501 Failure Report by the Inquiry Board,” technical report, European Space Agency, http://ravel. esrin.esa.it/docsesa-x-1819eng.pdf , 1996.
[3] D. Gage and J. McCormick, “We Did Nothing Wrong,” Baseline, vol. 1, no. 28, pp. 32-58, http://common.ziffdavisinternet.com/download/ 0/2529Baseline0304-DissectionNEW.pdf , 2004.
[4] J. Harrison, Theorem Proving with the Real Numbers. Springer-Verlag, 1998.
[5] J. Fleuriot and L. Paulson, “Mechanizing Nonstandard Real Analysis,” LMS J. Computation and Math., vol. 3, pp. 140-190, http://www.lms.ac.uk/jcm/3lms1999-027/, 2000.
[6] R. Gamboa, “Mechanically Verifying Real-Valued Algorithms in ACL2,” PhD dissertation, Univ. of Texas at Austin, ftp://ftp.cs.utexas.edu/pub/boyer/dissgamboa.pdf , 1999.
[7] M. Mayero, “Formalisation et Automatisation de Preuves en Analyse Réelle et Numérique,” PhD dissertation, Université Pierre et Marie Curie, http://www.pps.jussieu.fr/~mayero/specif these-mayero.ps, 2001.
[8] H. Gottliebsen, “Automated Theorem Proving for Mathematics: Real Analysis in PVS,” PhD dissertation, Univ. of St. Andrews, http://www.dcs.qmul.ac.uk/~hagothesis.ps.gz , 2001.
[9] C. Muñoz, V. Carreño, G. Dowek, and R. Butler, “Formal Verification of Conflict Detection Algorithms,” Int'l J. Software Tools for Technology Transfer, vol. 4, no. 3, pp. 371-380, http://dx.doi.org/10.1007s10009-002-0084-3 , 2003.
[10] M. Daumas, G. Melquiond, and C. Muñoz, “Guaranteed Proofs Using Interval Arithmetic,” Proc. 17th IEEE Symp. Computer Arithmetic (ARITH '05), P. Montuschi and E. Schwarz, eds., pp.188-195, http://hal.archives-ouvertes.frhal-00164621 , 2005.
[11] C. Muñoz and D. Lester, “Real Number Calculations and Theorem Proving,” Proc. 18th Int'l Conf. Theorem Proving in Higher Order Logics (TPHOLs '05), pp. 239-254, http://dx.doi.org/10.100711541868_13, 2005.
[12] S. Owre, J.M. Rushby, and N. Shankar, “PVS: A Prototype Verification System,” Proc. 11th Int'l Conf. Automated Deduction (CADE '92), D. Kapur, ed., pp. 748-752, http://pvs.csl.sri.com/papers/cade92-pvs cade92-pvs.ps, 1992.
[13] M. Abramowitz and I.A. Stegun, eds., Handbook of Mathematical Functions with Formulas, Graphs, and Mathematical Tables. Dover Publications, 1972.
[14] J.-M. Muller, Elementary Functions, Algorithms and Implementation. Birkhaüser, http://www.springer.com/west/home/birkhauser computer+science?SGWID=4-40353-22-72377986-0 , 2006.
[15] Mathematics by Experiment: Plausible Reasoning in the 21st Century, J.Borwein and D.H. Bailey, eds. A.K. Peters, 2003.
[16] A. Neumaier, Interval Methods for Systems of Equations. Cambridge Univ. Press, 1990.
[17] L. Jaulin, M. Kieffer, O. Didrit, and E. Walter, Applied Interval Analysis. Springer, http://www.springeronline.com/sgw/cda/frontpage 0, 10735, 5-40106-22-2093571-0, 00.html , 2001.
[18] Rigorous Global Search: Continuous Problems, R.B. Kearfott, ed. Kluwer Academic Publishers, 1996.
[19] A. Yakovlev, “Classification Approach to Programming of Localizational (Interval) Computations,” Interval Computations, vol. 1, no. 1, pp. 61-84, 1992.
[20] J. Sawada, “Formal Verification of Divide and Square Root Algorithms Using Series Calculation,” Proc. Third Int'l Workshop ACL2 Theorem Prover and Its Applications (ACL2 '02), pp. 31-49, 2002.
[21] C. Muñoz, “Batch Proving and Proof Scripting in PVS,” Report NIA report no. 2007-03, NASA/CR-2007-214546, NIA-NASA Langley, Nat'l Inst. Aerospace, Hampton, Va., Feb. 2007.
[22] R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J.V. Tassel, “Experience with Embedding Hardware Description Languages in HOL,” Proc. IFIP TC10/WG 10.2 Int'l Conf. Theorem Provers in Circuit Design (TPCD '92), pp. 129-156, 1992.
[23] J. Harrison, “Metatheory and Reflection in Theorem Proving: A Survey and Critique,” Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, U.K., 1995.
[24] S. Boutin, “Using Reflection to Build Efficient and Certified Decision Procedures,” Proc. Third Int'l Symp. Theoretical Aspects of Computer Software (TACS '97), pp. 515-529, 1997.
[25] F.W. von Henke, S. Pfab, H. Pfeifer, and H. Rueß, “Case Studies in Meta-Level Theorem Proving,” Proc. 11th Int'l Conf. Theorem Proving in Higher Order Logics (TPHOLs '98), J. Grundy and M.Newey, eds., pp. 461-478, Sept. 1998.
[26] N. Shankar, “Efficiently Executing PVS,” Computer Science Laboratory, SRI Int'l, Menlo Park, CA, project report, http://www.csl.sri.com/shankarPVSeval.ps.gz , Nov. 1999.
[27] C. Muñoz, “Rapid Prototyping in PVS,” Report NIA Report 2003-03, NASA/CR-2003-212418, NIA-NASA Langley, Nat'l Inst. Aerospace, Hampton, Va., May 2003.
[28] P. Markstein, IA-64 and Elementary Functions: Speed and Precision. Prentice Hall, 2000.
[29] P. Gowland and D. Lester, “A Survey of Exact Arithmetic Implementations,” Proc. Fourth Int'l Workshop Computability and Complexity in Analysis (CCA '00), pp. 30-47, http://www.link. springer.de/link/service/ series/0558/bibs/206420640030.htm, 2000.
[30] V. Ménissier-Morain, “Arbitrary Precision Real Arithmetic: Designand Algorithms,” J. Logic and Algebraic Programming, vol. 64, no. 1, pp. 13-39, http://dx.doi.org/10.1016j.jlap.2004.07. 003 , 2005.
[31] G. Huet, G. Kahn, and C. Paulin-Mohring, The Coq Proof Assistant: A Tutorial: Version 8.0, ftp://ftp.inria.fr/INRIA/coq/current/doc Tutorial.pdf.gz, 2004.
[32] A. Ciaffaglione and P. Di Gianantonio, “A Certified, Corecursive Implementation of Exact Real Numbers,” Theoretical Computer Science, vol. 351, no. 1, pp. 39-51, http://dx.doi.org/10.1016j.tcs.2005.09.061 , 2006.
[33] J. Hughes and M. Niqui, “Admissible Digit Sets,” Theoretical Computer Science, vol. 351, no. 1, pp. 61-73, http://dx.doi.org/10.1016j.tcs.2005.09.059 , 2006.
[34] Y. Bertot, “Affine Functions and Series with Co-Inductive Real Numbers,” Math. Structures in Computer Science, vol. 17, no. 1, pp.37-63, http://dx.doi.org/10.1017S0960129506005809 , 2007.
[35] B. Dutertre, “Elements of Mathematical Analysis in PVS,” Proc. Ninth Int'l Conf. Theorem Proving in Higher Order Logics (TPHOLs'96), J. von Wright, J. Grundy, and J. Harrison, eds., pp.141-156, http://www.sdl.sri.com/paperstphol96/, Aug. 1996.
[36] M. Daumas and G. Melquiond, “Generating Formally Certified Bounds on Values and Round-Off Errors,” Real Numbers and Computers, pp. 55-70, http://hal.inria.frinria- 00070739, 2004.
[37] R. Zumkeller, “Formal Global Optimisation with Taylor Models,” Proc. Third Int'l Joint Conf. Automated Reasoning (IJCAR '06), U. Furbach and N. Shankar, eds., pp. 408-422, http://dx.doi.org/10.100711814771_35, 2006.
[38] S. Boldo and C. Muñoz, “Provably Faithful Evaluation of Polynomials,” Proc. 21st ACM Symp. Applied Computing (SAC'06), pp.1328-1332, http://doi.acm.org/10.11451141277.1141586 , 2006.
[39] D. Lester and P. Gowland, “Using PVS to Validate the Algorithms of an Exact Arithmetic,” Theoretical Computer Science, vol. 291, no. 2, pp. 203-218, Nov. 2002.
[40] K. Makino and M. Berz, “Taylor Models and Other Validated Functional Inclusion Methods,” Int'l J. Pure and Applied Math., vol. 4, no. 4, pp. 379-456, http://bt.pa.msu.edu/pub/papers/TMIJPAM03 TMIJPAM03.pdf, 2003.
[41] F. Cháves and M. Daumas, “A Library to Taylor Models for PVS Automatic Proof Checker,” Proc. NSF Workshop Reliable Eng. Computing (REC '06), pp. 39-52, http://www.gtsav.gatech.edu/workshop/rec06/ papersChaves_paper.pdf, 2006.
[42] F. Cháves, M. Daumas, C. Muñoz, and N. Revol, “Automatic Strategies to Evaluate Formulas on Taylor Models and Generate Proofs in PVS,” Proc. Sixth Int'l Congress on Industrial and Applied Math. (ICIAM '07), http:/www.iciam07.ch/, 2007.

Index Terms:
Real number calculations, interval arithmetic, proof checking, theorem proving.
Citation:
Marc Daumas, David Lester, Céar Muñoz, "Verified Real Number Calculations: A Library for Interval Arithmetic," IEEE Transactions on Computers, vol. 58, no. 2, pp. 226-237, Feb. 2009, doi:10.1109/TC.2008.213
Usage of this product signifies your acceptance of the Terms of Use.