Advertisement

Journal of Automated Reasoning

, Volume 62, Issue 2, pp 215–236 | Cite as

The Flow of ODEs: Formalization of Variational Equation and Poincaré Map

  • Fabian ImmlerEmail author
  • Christoph Traut
Article

Abstract

Formal analysis of ordinary differential equations (ODEs) and dynamical systems requires a solid formalization of the underlying theory. The formalization needs to be at the correct level of abstraction, in order to avoid drowning in tedious reasoning about technical details. The flow of an ODE, i.e., the solution depending on initial conditions, and a dedicated type of bounded linear functions yield suitable abstractions. The dedicated type integrates well with the type-class based analysis in Isabelle/HOL and we prove advanced properties of the flow, most notably, differentiable dependence on initial conditions via the variational equation. Moreover, we formalize the notion of first return or Poincaré map and prove its differentiability. We provide rigorous numerical algorithm to solve the variational equation and compute the Poincaré map.

Keywords

Isabelle/HOL Analysis Ordinary differential equation Dynamical system Poincaré map 

Notes

Acknowledgements

We would like to thank Professor Dr. Martin Brokate for supervising part of this work as an “interdisciplinary project”. Johannes Hölzl’s suggestions related to filters were very helpful. We would also like to thank the anonymous reviewers for all their suggestions and comments. Part of this work was supported by DFG RTG 1480 and DFG NI 491/16-1.

References

  1. 1.
    Boldo, S., Clément, F., Faissole, F., Martin, V., Mayero, M.: A Coq formal proof of the Lax–Milgram theorem. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, ACM, pp. 79–89 (2017)Google Scholar
  2. 2.
    Boldo, S., Clément, F., Filliâtre, J.C., Mayero, M., Melquiond, G., Weis, P.: Wave equation numerical resolution: a comprehensive mechanized proof of a C program. J. Autom. Reason. 50(4), 423–456 (2013).  https://doi.org/10.1007/s10817-012-9255-4 MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2015).  https://doi.org/10.1007/s11786-014-0181-1 MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7), 1196–1233 (2016).  https://doi.org/10.1017/S0960129514000437 MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Fleuriot, J.D., Paulson, L.C.: Mechanizing nonstandard real analysis. LMS J. Comput. Math. 3, 140–190 (2000).  https://doi.org/10.1112/S1461157000000267 MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Gouezel, S.: Ergodic theory. Archive of formal proofs. Formal Proof Development. http://isa-afp.org/entries/Ergodic_Theory.shtml (2015)
  7. 7.
    Gouezel, S.: Lp spaces. Archive of formal proofs. Formal Proof Development. http://isa-afp.org/entries/Lp.shtml (2016)
  8. 8.
    Haftmann, F.: Code generation from specifications in higher-order logic. Dissertation, Technische Universität München, München (2009)Google Scholar
  9. 9.
    Harrison, J.: A HOL theory of Euclidean space. In: J. Hurd, T. Melham (eds.) 18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs, LNCS, vol. 3603, pp. 114–129 (2005)Google Scholar
  10. 10.
    Harrison, J.: The HOL light theory of Euclidean space. J. Autom. Reason. 50(2), 173–190 (2013).  https://doi.org/10.1007/s10817-012-9250-9 MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Hirsch, M.W., Smale, S., Devaney, R.L.: Differential Equations, Dynamical Systems, and an Introduction to Chaos. Elsevier, New York (2013)zbMATHGoogle Scholar
  12. 12.
    Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: International Conference on Interactive Theorem Proving, Springer, pp. 279–294 (2013)Google Scholar
  13. 13.
    Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: International Conference on Certified Programs and Proofs, Springer, pp. 131–146 (2013)Google Scholar
  14. 14.
    Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: Badger, J., Rozier, K. (eds.) NASA Formal Methods, LNCS, vol. 8430, pp. 113–127. Springer, Berlin (2014)CrossRefGoogle Scholar
  15. 15.
    Immler, F.: A verified algorithm for geometric zonotope/hyperplane intersection. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP ’15, ACM, New York, NY, USA, pp. 129–136 (2015)Google Scholar
  16. 16.
    Immler, F.: Verified reachability analysis of continuous systems. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, vol. 9035, pp. 37–51. Springer, Berlin (2015).  https://doi.org/10.1007/978-3-662-46681-0_3 Google Scholar
  17. 17.
    Immler, F., Hölzl, J.: Numerical analysis of ordinary differential equations in Isabelle/HOL. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving, LNCS, vol. 7406, pp. 377–392. Springer, Berlin (2012)CrossRefGoogle Scholar
  18. 18.
    Immler, F., Hölzl, J.: Ordinary differential equations. Archive of Formal Proofs. Formal Proof Development (2017). http://isa-afp.org/entries/Ordinary_Differential_Equations.html
  19. 19.
    Immler, F., Traut, C.: The flow of ODEs. In: International Conference on Interactive Theorem Proving, Springer, pp. 184–199 (2016)Google Scholar
  20. 20.
    Lelay, C., Melquiond, G.: Différentiabilité et intégrabilité en Coq. application à la formule de d’Alembert. In: JFLA—Journées Francophone des Langages Applicatifs, 2012. Carnac, France (2012). https://hal.inria.fr/hal-00642206
  21. 21.
    Maggesi, M.: A formalization of metric spaces in HOL light. J. Autom. Reason. (2017). 10.1007/s10817-017-9412-xGoogle Scholar
  22. 22.
    Makarov, E., Spitters, B.: The Picard algorithm for ordinary differential equations in Coq. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving, LNCS, vol. 7998, pp. 463–468. Springer, Berlin (2013)CrossRefGoogle Scholar
  23. 23.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002)CrossRefzbMATHGoogle Scholar
  24. 24.
    Perko, L.: Differential Equations and Dynamical Systems. Springer, Berlin (2001).  https://doi.org/10.1007/978-1-4613-0003-8 CrossRefzbMATHGoogle Scholar
  25. 25.
    Robinson, C.: Dynamical Systems, Stability, Symbolic Dynamics, and Chaos. CRC Press, Boca Raton (1999).  https://doi.org/10.1007/978-1-4613-0003-8
  26. 26.
    Tucker, W.: A rigorous ODE solver and Smale’s 14th problem. Found. Comput. Math. 2(1), 53–117 (2002)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer Science+Business Media B.V., part of Springer Nature 2018

Authors and Affiliations

  1. 1.Institut für InformatikTechnische Universität MünchenGarchingGermany

Personalised recommendations