Hostname: page-component-745bb68f8f-v2bm5 Total loading time: 0 Render date: 2025-01-24T06:37:15.288Z Has data issue: false hasContentIssue false
  • English
  • Français

Formal proofs for theoretical properties of Newton's method

Published online by Cambridge University Press:  01 July 2011

IOANA PAŞCA
IOANA PAŞCA*
Affiliation:
INRIA Sophia Antipolis, 2004 route des Lucioles – BP 93, 06902 Sophia Antipolis Cedex, France Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We discuss a formal development for the certification of Newton's method. We address several issues encountered in the formal study of numerical algorithms: developing the necessary libraries for our proofs, adapting paper proofs to suit the features of a proof assistant and designing new proofs based on the existing ones to deal with optimisations of the method. We start from Kantorovitch's Theorem, which gives the convergence of Newton's method in the case of a system of equations. To formalise this proof inside the proof assistant Coq, we first need to code the necessary concepts from multivariate analysis. We also prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. This proof is based on Kantorovitch's Theorem, but is an original result. An algorithm including rounding is a more accurate model for computations with Newton's method in practice.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 21 , Special Issue 4: Interactive Theorem Proving and the Formalisation of Mathematics , August 2011 , pp. 683 - 714
Copyright
Copyright © Cambridge University Press 2011

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

Bertot, Y. and Castéran, P. (2004) Interactive Theorem Proving and Program Development, Coq'Art: the Calculus of Inductive Constructions, Springer-Verlag.CrossRefGoogle Scholar
Bertot, Y., Gonthier, G., Biha, S. O. and Paşca, I. (2008) Canonical Big Operators. In: Mohamed, O. A., Muñoz, C. and Tahar, S. (eds.) Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008). Springer-Verlag Lecture Notes in Computer Science 517086–101.Google Scholar
Biha, S. O. (2008) Formalisation des mathématiques: une preuve du théorème de Cayley-Hamilton. In: Journées Francophones des Langages Applicatifs 1–14.Google Scholar
Coq development team (2009) The Coq Proof Assistant Reference Manual, version 8.2.Google Scholar
Cowles, J., Gamboa, R. and Van Baalen, J. V. (2003) Using ACL2 Arrays to Formalize Matrix Algebra. In: Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003).Google Scholar
Delahaye, D. and Mayero, M. (2005) Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System. In: Proceedings of Calculemus 2005. Electronic Notes in Theoretical Computer Science 151 (1)57–73.CrossRefGoogle Scholar
Duerte, B. (1996) Elements of Mathematical Analysis in PVS. In: von Wright, J., Grundy, J. and Harrison, J. (eds.) Proceedings of the Ninth International Conference on Theorem Proving in Higher-Order Logics (TPHOL '96). Springer-Verlag Lecture Notes in Computer Science 1125141–156.Google Scholar
Démidovitch, B. and Maron, I. (1979) Éléments de calcul numérique, Mir – Moscou.Google Scholar
Fleuriot, J. D. (2000) On the mechanization of real analysis in Isabelle/HOL. 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 1869146–162.Google Scholar
Gamboa, R. and Kaufmann, M. (2001) Nonstandard Analysis in ACL2. Journal of automated reasoning 27 (4)323–428.CrossRefGoogle Scholar
Garillot, F., Gonthier, G., Mahboubi, A. and Rideau, L. (2009) Packaging mathematical structures. In: Nipkow, T. and Urban, C. (eds.) Proceedings Theorem Proving in Higher Order Logics. Springer-Verlag Lecture Notes in Computer Science 5674327–342.CrossRefGoogle Scholar
Gonthier, G. and Mahboubi, A. (2008) A small scale reflection extension for the Coq system. INRIA Technical report. (Available at http://hal.inria.fr/inria-00258384.)Google Scholar
Harrison, J. (1998) Theorem Proving with the Real Numbers, Distinguished Dissertations, Springer-Verlag.Google Scholar
Harrison, J. (2005) A HOL Theory of Euclidian Space. In: Hurd, J. and Melham, T. F. (eds.) Proceedings: Theorem Proving in Higher Order Logics. Springer-Verlag Lecture Notes in Computer Science 3603114–129.CrossRefGoogle Scholar
Harrison, J. and Théry, L. (1998) A Skeptic's Approach to Combining HOL and Maple. J. Autom. Reasoning 21 (3)279–294, 1998.CrossRefGoogle Scholar
Julien, N. (2008) Certified exact real arithmetic using co-induction in arbitrary integer base. In: Garrigue, J. and Hermenegildo, M. (eds.) Functional and Logic Programming Symposium (FLOPS). 4989 48–63.CrossRefGoogle Scholar
Julien, N. and Pasca, I. (2009) Formal Verification of Exact Computations Using Newton's Method. In: Nipkow, T. and Urban, C. (eds.) Proceedings Theorem Proving in Higher Order Logics. Springer-Verlag Lecture Notes in Computer Science 5674408–423.Google Scholar
Lester, D. R. (2008) Real Number Calculations and Theorem Proving. In: Mohamed, O. A., Muñoz, C. and Tahar, S. (eds.) Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008). Springer-Verlag Lecture Notes in Computer Science 5170215–229.Google Scholar
Mayero, M. (2001) Formalisation et automatisation de preuves en analyses reelle et numerique, Ph.D. thesis, Université de Paris VI.Google Scholar
Obua, S. (2005) Proving bounds for real linear programs in isabelle/hol. In: Hurd, J. and Melham, T. F. (eds.) Proceedings: Theorem Proving in Higher Order Logics. Springer-Verlag Lecture Notes in Computer Science 3603227–244.CrossRefGoogle Scholar
O'Connor, R. (2008) Certified Exact Transcendental Real Number Computation in Coq. In: Mohamed, O. A., Muñoz, C. and Tahar, S. (eds.) Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008). Springer-Verlag Lecture Notes in Computer Science 5170246–261.Google Scholar
Paşca, I. (2008) A Formal Verification for Kantorovitch's Theorem. In: Journées Francophones des Langages Applicatifs 15–29.Google Scholar