Abstract
Solutions to differential equations, which are used to model physical systems, are computed numerically by solving a set of discretized equations. This set of discretized equations is reduced to a large linear system, whose solution is typically found using an iterative solver. We start with an initial guess, \(x_0\), and iterate the algorithm to obtain a sequence of solution vectors, \(x_k\), which are approximations to the exact solution of the linear system, x. The iterative algorithm is said to converge to x, in the field of reals, if and only if \(x_k\) converges to x in the limit of \(k \rightarrow \infty \).
In this paper, we formally prove the asymptotic convergence of a particular class of iterative methods called the stationary iterative methods, in the Coq theorem prover. We formalize the necessary and sufficient conditions required for the iterative convergence, and extend this result to two classical iterative methods: the Gauss–Seidel method and the Jacobi method. For the Gauss–Seidel method, we also formalize a set of easily testable conditions for iterative convergence, called the Reich theorem, for a particular matrix structure, and apply this on a model problem of the one-dimensional heat equation. We also apply the main theorem of iterative convergence to prove convergence of the Jacobi method on the model problem.
M. Tekriwal—Currently affiliated with the Lawrence Livermore National Laboratory, USA.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Our Coq formalization is available at https://github.com/mohittkr/iterative_convergence.git.
- 2.
The theory about complex modulus and norms has been added in most recent developments of MathComp after our discussion with the developers. We were pointed to the development of matrix norms in the CoqQ project (https://github.com/coq-quantum/CoqQ/blob/main/src/mxnorm.v), which was done concurrently with our development.
References
Bagnara, R.: A unified proof for the convergence of Jacobi and Gauss-Seidel methods. SIAM Rev. 37(1), 93–97 (1995)
Boldo, S., Clément, F., Filliâtre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Formal proof of a wave equation resolution scheme: the method error. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 147–162. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_12
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)
Boldo, S., Clément, F., Filliâtre, J.C., Mayero, M., Melquiond, G., Weis, P.: Trusting computations: a mechanized proof from partial differential equations to actual program. Comput. Math. Appl. 68(3), 325–352 (2014)
Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2015)
Cano, G., Dénès, M.: Matrices à blocs et en forme canonique. In: JFLA – Journées francophones des langages applicatifs (2013). https://hal.inria.fr/hal-00779376
Cohen, C.: Construction of real algebraic numbers in Coq. In: Interactive Theorem Proving (2012). https://hal.inria.fr/hal-00671809
Deniz, E., Rashid, A., Hasan, O., Tahar, S.: On the formalization of the heat conduction problem in HOL. In: Buzzard, K., Kutsia, T. (eds.) CICM 2022. LNCS, vol. 13467, pp. 21–37. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-16681-5_2
Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327–342. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_23
Hindmarsh, A.C.: Odepack, a systematized collection of ode solvers. Sci. Comput. 55–64 (1983)
Hindmarsh, A.C., et al.: SUNDIALS: suite of nonlinear and differential/algebraic equation solvers. ACM Trans. Math. Softw. (TOMS) 31(3), 363–396 (2005)
Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 113–127. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06200-6_9
Immler, F., Hölzl, J.: Numerical analysis of ordinary differential equations in Isabelle/HOL. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 377–392. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_26
Immler, F., Traut, C.: The flow of ODEs. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 184–199. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43144-4_12
Immler, F., Traut, C.: The flow of ODEs: formalization of variational equation and Poincaré map. J. Autom. Reason. 62(2), 215–236 (2019)
Lancaster, P., Tismenetsky, M.: The Theory of Matrices: With Applications. Elsevier (1985)
Mahboubi, A., Cohen, C.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logical Methods Comput. Sci. 8 (2012)
Pasca, I.: Formal verification for numerical methods. Ph.D. thesis, Université Nice Sophia Antipolis (2010)
Prussing, J.E.: The principal minor test for semidefinite matrices. J. Guid. Control. Dyn. 9(1), 121–122 (1986)
Reich, E.: On the convergence of the classical iterative method of solving linear simultaneous equations. Ann. Math. Stat. 20(3), 448–451 (1949)
Saad, Y.: Iterative Methods for Sparse Linear Systems, 2nd edn. Society for Industrial and Applied Mathematics (SIAM), Philadelphia (2003)
Tekriwal, M., Appel, A.W., Kellison, A.E., Bindel, D., Jeannin, J.B.: Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method. In: Dubois, C., Kerber, M. (eds.) CICM 2023. LNCS, vol. 14101, pp. 206–221. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-42753-4_14
Tekriwal, M., Duraisamy, K., Jeannin, J.-B.: A formal proof of the lax equivalence theorem for finite difference schemes. In: Dutle, A., Moscato, M.M., Titolo, L., Muñoz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 322–339. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-76384-8_20
Tekriwal, M., Miller, J., Jeannin, J.B.: Formalization of asymptotic convergence for stationary iterative methods (extended version) (2022). https://arxiv.org/abs/2202.05587
Thiemann, R.: A Perron-Frobenius theorem for deciding matrix growth. J. Logical Algebraic Methods Program. 123, 100699 (2021)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Tekriwal, M., Miller, J., Jeannin, JB. (2024). Formalization of Asymptotic Convergence for Stationary Iterative Methods. In: Benz, N., Gopinath, D., Shi, N. (eds) NASA Formal Methods. NFM 2024. Lecture Notes in Computer Science, vol 14627. Springer, Cham. https://doi.org/10.1007/978-3-031-60698-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-031-60698-4_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-60697-7
Online ISBN: 978-3-031-60698-4
eBook Packages: Computer ScienceComputer Science (R0)