Document Open Access Logo

A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations

Authors Sewon Park , Holger Thies

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.30.pdf
  • Filesize: 0.81 MB
  • 19 pages

Document Identifiers

Author Details

Sewon Park
  • Graduate School of Informatics, Kyoto University, Japan
Holger Thies
  • Graduate School of Human and Environmental Studies, Kyoto University, Japan

Funding

  • Park, Sewon: has been supported by JSPS KAKENHI (Grant-in-Aid for JSPS Fellows) JP22F22071 as a JSPS International Research Fellow.
  • Thies, Holger: Supported by JSPS KAKENHI Grant Numbers JP20K19744, JP23H03346 and JP24K20735.

Cite AsGet BibTex

Sewon Park and Holger Thies. A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.30

Abstract

In exact real computation real numbers are manipulated exactly without round-off errors, making it well-suited for high precision verified computation. In recent work we propose an axiomatic formalization of exact real computation in the Coq theorem prover. The formalization admits an extended extraction mechanism that lets us extract computational content from constructive parts of proofs to efficient programs built on top of AERN, a Haskell library for exact real computation. Many processes in science and engineering are modeled by ordinary differential equations (ODEs), and often safety-critical applications depend on computing their solutions correctly. The primary goal of the current work is to extend our framework to spaces of functions and to support computation of solutions to ODEs and other essential operators. In numerical mathematics, the most common way to represent continuous functions is to use polynomial approximations. This can be modeled by so-called Taylor models, that encode a function as a polynomial and a rigorous error-bound over some domain. We define types of classical functions that do not hold any computational content and formalize Taylor models to computationally approximate those classical functions. Classical functions are defined in a way to admit classical principles in their constructions and verification. We define various basic operations on Taylor models and verify their correctness based on the classical functions that they approximate. We then shift our interest to analytic functions as a generalization of Taylor models where polynomials are replaced by infinite power series. We use the formalization to develop a theory of non-linear polynomial ODEs. From the proofs we can extract certified exact real computation programs that compute solutions of ODEs on some time interval up to any precision.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Exact real computation
  • Taylor models
  • Analytic functions
  • Computable analysis
  • Program extraction

Metrics

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

Supplementary Materials

References

  1. Reynald Affeldt, Yves Bertot, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Pierre Roux, Kazuhiko Sakaguchi, Zachary Stone, Pierre-Yves Strub, et al. Mathcomp-analysis: Mathematical components compliant analysis library, 2022. Google Scholar
  2. Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei Hsin Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel, editors, Hybrid Systems, pages 209-229, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg. Google Scholar
  3. A. Balluchi, A. Casagrande, P. Collins, A. Ferrari, T. Villa, and A.L. Sangiovanni-Vincentelli. Ariadne: a Framework for Reachability Analysis of Hybrid Automata. In Proc. 17th Int. Symp. on Mathematical Theory of Networks and Systems, Kyoto, 2006. Google Scholar
  4. Errett Bishop and Douglas Bridges. Constructive analysis, volume 279. Springer Science & Business Media, 2012. Google Scholar
  5. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Mathematics in Computer Science, 9(1):41-62, 2015. URL: https://doi.org/10.1007/s11786-014-0181-1.
  6. Franz Brauße, Pieter Collins, and Martin Ziegler. Computer science for continuous data. In François Boulier, Matthew England, Timur M. Sadykov, and Evgenii V. Vorozhtsov, editors, Computer Algebra in Scientific Computing, pages 62-82, Cham, 2022. Springer International Publishing. Google Scholar
  7. Franz Brauße, Margarita Korovina, and Norbert Müller. Using taylor models in exact real arithmetic. In Revised Selected Papers of the 6th International Conference on Mathematical Aspects of Computer and Information Sciences - Volume 9582, MACIS 2015, pages 474-488, Berlin, Heidelberg, 2015. Springer-Verlag. URL: https://doi.org/10.1007/978-3-319-32859-1_41.
  8. Franz Brauße, Margarita Korovina, and Norbert Th Müller. Towards using exact real arithmetic for initial value problems. In Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers 10, pages 61-74. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41579-6_6.
  9. Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. Flow*: An analyzer for non-linear hybrid systems. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, pages 258-263, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  10. George F Corliss and Robert Rihm. Validating an a priori enclosure using high-order taylor series. Mathematical Research, 90:228-238, 1996. Google Scholar
  11. Luís Cruz-Filipe, Herman Geuvers, and Freek Wiedijk. C-CoRN, the constructive Coq repository at Nijmegen. In International Conference on Mathematical Knowledge Management, pages 88-103. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27818-4_7.
  12. Laurent Doyen, Goran Frehse, George J. Pappas, and André Platzer. Verification of Hybrid Systems, pages 1047-1110. Springer International Publishing, Cham, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_30.
  13. Fabian Immler. A Verified ODE Solver and Smale’s 14th Problem (Ein Verifizierter GDGL-Löser und Smales 14. Problem). PhD thesis, Technical University of Munich, Germany, 2018. URL: https://mediatum.ub.tum.de/1422071.
  14. Fabian Immler. A verified ODE solver and the lorenz attractor. J. Autom. Reason., 61(1-4):73-111, 2018. URL: https://doi.org/10.1007/S10817-017-9448-Y.
  15. Manuel Kauers. D-finite Functions, volume 30. Springer Nature, 2023. Google Scholar
  16. Akitoshi Kawamura, Florian Steinberg, and Holger Thies. Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving. In International Workshop on Logic, Language, Information, and Computation, pages 223-236. Springer, 2018. URL: https://doi.org/10.1007/978-3-662-57669-4_13.
  17. Michal Konečný, Sewon Park, and Holger Thies. Axiomatic reals and certified efficient exact real computation. In International Workshop on Logic, Language, Information, and Computation, pages 252-268. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-88853-4_16.
  18. Michal Konečný, Sewon Park, and Holger Thies. Certified computation of nondeterministic limits. In NASA Formal Methods Symposium, pages 771-789. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-06773-0_41.
  19. Michal Konečný, Sewon Park, and Holger Thies. Extracting efficient exact real number computation from proofs in constructive type theory. arXiv preprint arXiv:2202.00891, 2022. Google Scholar
  20. Michal Konečný, Sewon Park, and Holger Thies. cAERN: Axiomatic Reals and Certified Efficient Exact Real Computation. https://github.com/holgerthies/coq-aern, 2024.
  21. Michal Konečný, Sewon Park, and Holger Thies. Formalizing Hyperspaces for Extracting Efficient Exact Real Computation. In Jérôme Leroux, Sylvain Lombardy, and David Peleg, editors, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023), volume 272 of Leibniz International Proceedings in Informatics (LIPIcs), pages 59:1-59:16, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2023.59.
  22. Michal Konečný. aern2-real: A Haskell library for exact real number computation. https://hackage.haskell.org/package/aern2-real, 2021.
  23. Soonho Kong, Sicun Gao, Wei Chen, and Edmund Clarke. dreach: δ-reachability analysis for hybrid systems. In Christel Baier and Cesare Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 200-205, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. Google Scholar
  24. Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote. Formally verified approximations of definite integrals. J. Autom. Reason., 62(2):281-300, 2019. URL: https://doi.org/10.1007/S10817-018-9463-7.
  25. Evgeny Makarov and Bas Spitters. The picard algorithm for ordinary differential equations in coq. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, pages 463-468, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-39634-2_34.
  26. Kyoko Makino and Martin Berz. Efficient control of the dependency problem based on taylor model methods. Reliable Computing, 5(1):3-12, 1999. URL: https://doi.org/10.1023/A:1026485406803.
  27. Kyoko Makino and Martin Berz. Taylor models and other validated functional inclusion methods. International Journal of Pure and Applied Mathematics, 6:239-316, 2003. Google Scholar
  28. Érik Martin-Dorel, Laurence Rideau, Laurent Théry, Micaela Mayero, and Ioana Pasca. Certified, efficient and sharp univariate taylor models in coq. In Proceedings of the 2013 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC '13, pages 193-200, USA, 2013. IEEE Computer Society. URL: https://doi.org/10.1109/SYNASC.2013.33.
  29. Norbert Th Müller. Constructive aspects of analytic functions. In Proc. Workshop on Computability and Complexity in Analysis, volume 190, pages 105-114, 1995. Google Scholar
  30. Norbert Th Müller. The iRRAM: Exact arithmetic in C++. In International Workshop on Computability and Complexity in Analysis, pages 222-252. Springer, 2000. URL: https://doi.org/10.1007/3-540-45335-0_14.
  31. Nedialko S Nedialkov. Interval tools for odes and daes. In 12th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN 2006), pages 4-4. IEEE, 2006. Google Scholar
  32. Sewon Park, Franz Brauße, Pieter Collins, SunYoung Kim, Michal Konečný, Gyesik Lee, Norbert Müller, Eike Neumann, Norbert Preining, and Martin Ziegler. Semantics, specification logic, and hoare logic of exact real computation, 2024. URL: https://arxiv.org/abs/1608.05787.
  33. Arno Pauly and Florian Steinberg. Comparing representations for function spaces in computable analysis. Theory Comput. Syst., 62(3):557-582, 2018. URL: https://doi.org/10.1007/S00224-016-9745-6.
  34. Svetlana Selivanova, Florian Steinberg, Holger Thies, and Martin Ziegler. Exact real computation of solution operators for linear analytic systems of partial differential equations. In Computer Algebra in Scientific Computing: 23rd International Workshop, CASC 2021, Sochi, Russia, September 13-17, 2021, Proceedings 23, pages 370-390. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-85165-1_21.
  35. Christoph Traut and Fabian Immler. Taylor models. Arch. Formal Proofs, 2018, 2018. URL: https://www.isa-afp.org/entries/Taylor_Models.html.
  36. K. Weihrauch. Computable analysis. Springer, Berlin, 2000. URL: https://doi.org/10.1007/978-3-642-56999-9.
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