Document Open Access Logo

A Certificate-Based Approach to Formally Verified Approximations

Authors Florent Bréhard, Assia Mahboubi, Damien Pous

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.8.pdf
  • Filesize: 0.54 MB
  • 19 pages

Document Identifiers

Author Details

Florent Bréhard
  • Plume and AriC teams, LIP, ENS de Lyon, Université de Lyon, Lyon, France
  • MAC team, LAAS-CNRS, Université de Toulouse, CNRS, Toulouse, France
Assia Mahboubi
  • Gallinette team, LS2N, INRIA, Université de Nantes, Nantes, France
Damien Pous
  • Plume team, LIP, CNRS, ENS de Lyon, Université de Lyon, Lyon, France

Funding

This work has been funded by the European Research Council (ERC) under the European Union’s Horizon 2020 programme (CoVeCe, grant agreement No 678157), and was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR). This work was supported in part by the project FastRelax ANR-14-CE25-0018-01.

Cite AsGet BibTex

Florent Bréhard, Assia Mahboubi, and Damien Pous. A Certificate-Based Approach to Formally Verified Approximations. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.8

Abstract

We present a library to verify rigorous approximations of univariate functions on real numbers, with the Coq proof assistant. Based on interval arithmetic, this library also implements a technique of validation a posteriori based on the Banach fixed-point theorem. We illustrate this technique on the case of operations of division and square root. This library features a collection of abstract structures that organise the specfication of rigorous approximations, and modularise the related proofs. Finally, we provide an implementation of verified Chebyshev approximations, and we discuss a few examples of computations.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • approximation theory
  • Chebyshev polynomials
  • Banach fixed-point theorem
  • interval arithmetic
  • Coq

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Henk Barendregt and Erik Barendsen. Autarkic Computations in Formal Proofs. Journal of Automated Reasoning, 28(3):321-336, April 2002. Google Scholar
  2. Alexandre Benoit, Mioara Joldeş, and Marc Mezzarobba. Rigorous uniform approximation of D-finite functions using Chebyshev expansions. Math. Comp., 86(305):1303-1341, 2017. URL: https://doi.org/10.1090/mcom/3135.
  3. Vasile Berinde. Iterative approximation of fixed points, volume 1912 of Lecture Notes in Mathematics. Springer, Berlin, 2007. Google Scholar
  4. Martin Berz and Kyoko Makino. Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliable Computing, 4(4):361-369, 1998. Google Scholar
  5. Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formal proof of the Lax-Milgram theorem. In 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Paris, France, January 2017. URL: https://doi.org/10.1145/3018610.3018625.
  6. Sylvie Boldo and Guillaume Melquiond. Verifying Floating-point Algorithms with the Coq System. Elsevier, 2017. Google Scholar
  7. Nicolas Bourbaki. General Topology. Springer, 1995. Original French edition published by MASSON, Paris, 1971. URL: https://doi.org/10.1007/978-3-642-61701-0.
  8. Florent Bréhard, Nicolas Brisebarre, and Mioara Joldes. Validated and numerically efficient Chebyshev spectral methods for linear ordinary differential equations. ACM Transactions on Mathematical Software, 2018. Google Scholar
  9. Florent Bréhard, Nicolas Brisebarre, Mioara Joldes, and Warwick Tucker. A New Lower Bound on the Hilbert Number for Quartic Systems, 2019. URL: http://www.jncf2019.uvsq.fr/program/abs-brehard.pdf.
  10. Nicolas Brisebarre and Mioara Joldeş. Chebyshev interpolation polynomial-based tools for rigorous computing. In Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, pages 147-154. ACM, 2010. Google Scholar
  11. Florent Bréhard, Assia Mahboubi, and Damien Pous. Web appendix to the present paper. URL: https://gitlab.inria.fr/amahboub/approx-models.
  12. Florent Bréhard, Assia Mahboubi, and Damien Pous. A certificate-based approach to formally verified approximations, 2019. Version with appendix. URL: https://hal.archives-ouvertes.fr/hal-02088529.
  13. Olga Caprotti and Martijn Oostdijk. Formal and Efficient Primality Proofs by Use of Computer Algebra Oracles. J. Symb. Comput., 32(1/2):55-70, 2001. Google Scholar
  14. Colin Christopher. Estimating limit cycle bifurcations from centers. In Differential equations with symbolic computation, Trends Math., pages 23-35. Birkhäuser, Basel, 2005. URL: https://doi.org/10.1007/3-7643-7429-2_2.
  15. Tobin A Driscoll, Nicholas Hale, and Lloyd N Trefethen. Chebfun guide, 2014. Google Scholar
  16. L. Fox and I. B. Parker. Chebyshev polynomials in numerical analysis. Oxford University Press, London-New York-Toronto, Ont., 1968. Google Scholar
  17. Benjamin Grégoire and Assia Mahboubi. Proving Equalities in a Commutative Ring Done Right in Coq. In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pages 98-113. Springer, 2005. URL: https://doi.org/10.1007/11541868_7.
  18. Benjamin Grégoire and Laurent Théry. A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. In Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of Lecture Notes in Computer Science, pages 423-437. Springer, 2006. Google Scholar
  19. Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, and Roland Zumkeller. A formal proof of the Kepler conjecture. CoRR, abs/1501.02155, 2015. URL: http://arxiv.org/abs/1501.02155,
  20. John Harrison and Laurent Théry. A Skeptic’s Approach to Combining HOL and Maple. J. Autom. Reasoning, 21(3):279-294, 1998. Google Scholar
  21. Johannes Hölzl, Fabian Immler, and Brian Huffman. Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, pages 279-294, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  22. Allan Hungria, Jean-Philippe Lessard, and Jason D. Mireles James. Rigorous numerics for analytic solutions of differential equations: the radii polynomial approach. Math. Comp., 85(299):1427-1459, 2016. Google Scholar
  23. Fabian Immler. A verified ODE solver and the Lorenz attractor. Journal of automated reasoning, pages 1-39, 2018. Google Scholar
  24. Fredrik Johansson. Arb: efficient arbitrary-precision midpoint-radius interval arithmetic. IEEE Transactions on Computers, 66(8):1281-1292, 2017. Google Scholar
  25. Tomas Johnson. A quartic system with twenty-six limit cycles. Exp. Math., 20(3):323-328, 2011. URL: https://doi.org/10.1080/10586458.2011.565252.
  26. Mioara Joldeş. https://tel.archives-ouvertes.fr/tel-00657843. PhD thesis, École normale supérieure de Lyon - Université de Lyon, Lyon, France, 2011.
  27. Edgar W Kaucher and Willard L Miranker. Self-validating numerics for function space problems: Computation with guarantees for differential and integral equations, volume 9. Elsevier, 1984. Google Scholar
  28. Rudi Klatte, Ulrich Kulisch, Andreas Wiethoff, and Michael Rauch. C-XSC: A C++ class library for extended scientific computing. Springer Science & Business Media, 2012. Google Scholar
  29. Jean-Philippe Lessard and Christian Reinhardt. Rigorous numerics for nonlinear differential equations using Chebyshev series. SIAM J. Numer. Anal., 52(1):1-22, 2014. Google Scholar
  30. Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Journal of Automated Reasoning, 62(2):281-300, February 2019. URL: https://doi.org/10.1007/s10817-018-9463-7.
  31. Érik Martin-Dorel and Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. Journal of Automated Reasoning, 57(3):187-217, October 2016. URL: https://doi.org/10.1007/s10817-015-9350-4.
  32. Guillaume Melquiond. Proving bounds on real-valued functions with computations. In International Joint Conference on Automated Reasoning, pages 2-17. Springer, 2008. Google Scholar
  33. Ramon E. Moore. Interval Analysis. Prentice-Hall, 1966. Google Scholar
  34. Nathalie Revol and Fabrice Rouillier. Motivations for an arbitrary precision interval arithmetic and the MPFI library. Reliable computing, 11(4):275-290, 2005. Google Scholar
  35. Siegfried M Rump. INTLAB—interval laboratory. In Developments in reliable computing, pages 77-104. Springer, 1999. Google Scholar
  36. Lloyd Nicholas Trefethen. Approximation Theory and Approximation Practice. SIAM, 2013. See URL: http://www.chebfun.org/ATAP/.
  37. Warwick Tucker. A rigorous ODE solver and Smale’s 14th problem. Found. Comput. Math., 2(1):53-117, 2002. URL: http://www.math.cornell.edu/~warwick/main/rodes/JFoCM.pdf.
  38. Warwick Tucker. Validated numerics: a short introduction to rigorous computations. Princeton University Press, 2011. Google Scholar
  39. Jan Bouwe Van Den Berg and Jean-Philippe Lessard. Chaotic braided solutions via rigorous numerics: Chaos in the Swift-Hohenberg equation. SIAM Journal on Applied Dynamical Systems, 7(3):988-1031, 2008. Google Scholar
  40. Nobito Yamamoto. A numerical verification method for solutions of boundary value problems with local uniqueness by Banach’s fixed-point theorem. SIAM J. Numer. Anal., 35(5):2004-2013, 1998. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact