Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Validated numerics
open-in-new
<h2 id="importance">Importance</h2> <p>Computation without verification may cause unfortunate results. Below are some examples. </p> <h3>Rump's example</h3> <p>In the 1980s, Rump made an example.<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a><a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a> He made a complicated function and tried to obtain its value. Single precision, double precision, extended precision results seemed to be correct, but its plus-minus sign was different from the true value. </p> <h3>Phantom solution</h3> <p>Breuer–Plum–McKenna used the spectrum method to solve the boundary value problem of the Emden equation, and reported that an asymmetric solution was obtained.<a class="footnote-ref" id="fnref:5" href="#fn:5"><sup>5</sup></a> This result to the study conflicted to the theoretical study by Gidas–Ni–Nirenberg which claimed that there is no asymmetric solution.<a class="footnote-ref" id="fnref:6" href="#fn:6"><sup>6</sup></a> The solution obtained by Breuer–Plum–McKenna was a phantom solution caused by discretization error. This is a rare case, but it tells us that when we want to strictly discuss differential equations, numerical solutions must be verified. </p> <h3>Accidents caused by numerical errors</h3> <p>The following examples are known as accidents caused by numerical errors: </p> <ul><li>Failure of intercepting missiles in the <a href="/facts/Gulf_War/6LdLnGdo">Gulf War</a> (1991)<a class="footnote-ref" id="fnref:7" href="#fn:7"><sup>7</sup></a></li> <li>Failure of the <a href="/facts/Ariane_5/H78wlLG4">Ariane 5</a> rocket (1996)<a class="footnote-ref" id="fnref:8" href="#fn:8"><sup>8</sup></a></li> <li>Mistakes in election result totalization<a class="footnote-ref" id="fnref:9" href="#fn:9"><sup>9</sup></a></li></ul> <h2 id="main-topics">Main topics</h2> <p>The study of validated numerics is divided into the following fields: </p> <ul><li>Verification in <a href="/facts/Numerical_linear_algebra/jnS6Tteb">numerical linear algebra</a> <ul><li>Validating numerical solutions of a given system of linear equations<a class="footnote-ref" id="fnref:10" href="#fn:10"><sup>10</sup></a><a class="footnote-ref" id="fnref:11" href="#fn:11"><sup>11</sup></a></li> <li>Validating numerically obtained eigenvalues<a class="footnote-ref" id="fnref:12" href="#fn:12"><sup>12</sup></a><a class="footnote-ref" id="fnref:13" href="#fn:13"><sup>13</sup></a><a class="footnote-ref" id="fnref:14" href="#fn:14"><sup>14</sup></a></li> <li>Rigorously computing <a href="/facts/Determinant/eGYqJ2TF">determinants</a><a class="footnote-ref" id="fnref:15" href="#fn:15"><sup>15</sup></a></li> <li>Validating numerical solutions of matrix equations<a class="footnote-ref" id="fnref:16" href="#fn:16"><sup>16</sup></a><a class="footnote-ref" id="fnref:17" href="#fn:17"><sup>17</sup></a><a class="footnote-ref" id="fnref:18" href="#fn:18"><sup>18</sup></a><a class="footnote-ref" id="fnref:19" href="#fn:19"><sup>19</sup></a><a class="footnote-ref" id="fnref:20" href="#fn:20"><sup>20</sup></a><a class="footnote-ref" id="fnref:21" href="#fn:21"><sup>21</sup></a><a class="footnote-ref" id="fnref:22" href="#fn:22"><sup>22</sup></a></li></ul></li> <li>Verification of <a href="/facts/Special_functions/JETSeucA">special functions</a>: <ul><li><a href="/facts/Gamma_function/SjGQcnyw">Gamma function</a><a class="footnote-ref" id="fnref:23" href="#fn:23"><sup>23</sup></a><a class="footnote-ref" id="fnref:24" href="#fn:24"><sup>24</sup></a></li> <li><a href="/facts/Elliptic_functions/mF03oI04">Elliptic functions</a><a class="footnote-ref" id="fnref:25" href="#fn:25"><sup>25</sup></a></li> <li><a href="/facts/Hypergeometric_functions/yTEC6NBJ">Hypergeometric functions</a><a class="footnote-ref" id="fnref:26" href="#fn:26"><sup>26</sup></a></li> <li><a href="/facts/Hurwitz_zeta_function/4EH7sKXB">Hurwitz zeta function</a><a class="footnote-ref" id="fnref:27" href="#fn:27"><sup>27</sup></a></li> <li><a href="/facts/Bessel_function/hSyvFPqC">Bessel function</a></li> <li><a href="/facts/Matrix_function/T2e9sFm9">Matrix function</a><a class="footnote-ref" id="fnref:28" href="#fn:28"><sup>28</sup></a><a class="footnote-ref" id="fnref:29" href="#fn:29"><sup>29</sup></a><a class="footnote-ref" id="fnref:30" href="#fn:30"><sup>30</sup></a></li></ul></li> <li>Verification of <a href="/facts/Numerical_quadrature/MwJnvcDV">numerical quadrature</a><a class="footnote-ref" id="fnref:31" href="#fn:31"><sup>31</sup></a><a class="footnote-ref" id="fnref:32" href="#fn:32"><sup>32</sup></a><a class="footnote-ref" id="fnref:33" href="#fn:33"><sup>33</sup></a></li> <li>Verification of nonlinear equations (The <a href="/facts/Kantorovich_theorem/Grtj9yBF">Kantorovich theorem</a>,<a class="footnote-ref" id="fnref:34" href="#fn:34"><sup>34</sup></a> Krawczyk method, interval Newton method, and the Durand–Kerner–Aberth method are studied.)</li> <li>Verification for solutions of ODEs, PDEs<a class="footnote-ref" id="fnref:35" href="#fn:35"><sup>35</sup></a> (For PDEs, knowledge of <a href="/facts/Functional_analysis/MIp233MT">functional analysis</a> are used.<a class="footnote-ref" id="fnref:36" href="#fn:36"><sup>36</sup></a>)</li> <li>Verification of <a href="/facts/Linear_programming/GduXFQxT">linear programming</a><a class="footnote-ref" id="fnref:37" href="#fn:37"><sup>37</sup></a></li> <li>Verification of <a href="/facts/Computational_geometry/eeaotQtl">computational geometry</a></li> <li>Verification at high-performance computing environment</li></ul> <p class="note">See also: <a href="/facts/Numerical_methods_for_ordinary_differential_equations/rbrYBco3">numerical methods for ordinary differential equations</a>, <a href="/facts/Numerical_linear_algebra/jnS6Tteb">numerical linear algebra</a>, <a href="/facts/Numerical_quadrature/MwJnvcDV">numerical quadrature</a>, and <a href="/facts/Computational_geometry/eeaotQtl">computational geometry</a></p> <h2 id="tools">Tools</h2> <ul><li><a href="https://www.tuhh.de/ti3/rump/intlab/">INTLAB</a> Library made by <a href="/facts/MATLAB/qPjLISCk">MATLAB</a>/<a href="/facts/GNU_Octave/vVVq5evM">GNU Octave</a></li> <li><a href="http://verifiedby.me/kv/index-e.html">kv</a> Library made by <a href="/facts/C%252B%252B/Et0F2qn9">C++</a>. This library can obtain multiple precision outputs by using <a href="/facts/GNU_MPFR/csBsCoTD">GNU MPFR</a>. <ul><li><a href="https://github.com/mskashi/kv">kv</a> on <a href="/facts/GitHub/n1hNCsc3">GitHub</a></li></ul></li> <li><a href="http://arblib.org/">Arb</a> Library made by <a href="/facts/C_(programming_language)/Ky2No763">C</a>. It is capable to rigorously compute various <a href="/facts/Special_functions/JETSeucA">special functions</a>. <ul><li><a href="https://github.com/fredrik-johansson/arb">arb</a> on <a href="/facts/GitHub/n1hNCsc3">GitHub</a></li></ul></li> <li><a href="http://capd.ii.uj.edu.pl/">CAPD</a> A collection of flexible C++ modules which are mainly designed to computation of homology of sets, maps and validated numerics for <a href="/facts/Dynamical_systems/782gREl5">dynamical systems</a>.</li> <li><a href="https://github.com/JuliaIntervals">JuliaIntervals</a> on <a href="/facts/GitHub/n1hNCsc3">GitHub</a> (Library made by <a href="/facts/Julia_(programming_language)/AoB0PJ9C">Julia</a>)</li> <li><a href="https://www.boost.org/doc/libs/develop/libs/safe_numerics/doc/html/index.html">Boost Safe Numerics - C++ header only library of validated replacements for all builtin integer types</a>. <ul><li><a href="https://github.com/safe_numerics">Safe numerics</a> on <a href="/facts/GitHub/n1hNCsc3">GitHub</a></li></ul></li></ul> <h2 id="see-also">See also</h2> <ul><li><a href="/facts/Computer-assisted_proof/Dnk4uESy">Computer-assisted proof</a></li> <li><a href="/facts/Interval_arithmetic/1ylnKraf">Interval arithmetic</a></li> <li><a href="/facts/Affine_arithmetic/rnXQVMX8">Affine arithmetic</a></li> <li><a href="/facts/INTLAB/cI4TAqYV">INTLAB</a> (Interval Laboratory)</li> <li><a href="/facts/Automatic_differentiation/dQcdhBAM">Automatic differentiation</a></li> <li>wikibooks:Numerical calculations and rigorous mathematics</li> <li><a href="/facts/Kantorovich_theorem/Grtj9yBF">Kantorovich theorem</a></li> <li><a href="/facts/Gershgorin_circle_theorem/tXde6pGo">Gershgorin circle theorem</a></li> <li><a href="/facts/Ulrich_W._Kulisch/aN6gMaU9">Ulrich W. Kulisch</a></li></ul> <h2 id="further-reading">Further reading</h2> <ul><li><a href="/facts/Warwick_Tucker/w47LIMUT">Tucker, Warwick</a> (2011). Validated Numerics: A Short Introduction to Rigorous Computations. <a href="/facts/Princeton_University_Press/kwvFlKEj">Princeton University Press</a>.</li> <li><a href="/facts/Ramon_Edgar_Moore/gJHDSXu2">Moore, Ramon Edgar</a>, Kearfott, R. Baker., Cloud, Michael J. (2009). Introduction to Interval Analysis. <a href="/facts/Society_for_Industrial_and_Applied_Mathematics/2HY4T5WY">Society for Industrial and Applied Mathematics</a>.</li> <li>Rump, Siegfried M. (2010). Verification methods: Rigorous results using floating-point arithmetic. <a href="/facts/Acta_Numerica/mN9tHCwY">Acta Numerica</a>, 19, 287–449.</li></ul> <h2 id="external-links">External links</h2> <ul><li><a href="http://www2.math.uu.se/~warwick/main/papers/ECM04Tucker.pdf">Validated Numerics for Pedestrians</a></li> <li><a href="https://interval.louisiana.edu/reliable-computing-journal/">Reliable Computing</a>, An open electronic journal devoted to numerical computations with guaranteed accuracy, bounding of ranges, mathematical proofs based on floating-point arithmetic, and other theory and applications of interval arithmetic and directed rounding.</li></ul> <h2 id="references">References</h2> <ol> <li id="fn:1"><p>Tucker, Warwick. (1999). "The Lorenz attractor exists." Comptes Rendus de l'Académie des Sciences-Series I-Mathematics, 328(12), 1197–1202. <a href="/wiki/Warwick_Tucker" target="_blank">/wiki/Warwick_Tucker</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li> <li id="fn:2"><p>Zin Arai, Hiroshi Kokubu, Paweãl Pilarczyk. Recent Development In Rigorous Computational Methods In Dynamical Systems. <a href="https://www.math.kyoto-u.ac.jp/~kokubu/preprints/rigdynam.pdf" target="_blank">https://www.math.kyoto-u.ac.jp/~kokubu/preprints/rigdynam.pdf</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li> <li id="fn:3"><p>Rump, Siegfried M. (1988). "Algorithms for verified inclusions: Theory and practice." In Reliability in computing (pp. 109–126). Academic Press. <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li> <li id="fn:4"><p>Loh, Eugene; Walster, G. William (2002). Rump's example revisited. Reliable Computing, 8(3), 245-248. <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li> <li id="fn:5"><p>Breuer, B.; Plum, Michael; McKenna, Patrick J. (2001). "Inclusions and existence proofs for solutions of a nonlinear boundary value problem by spectral numerical methods." In Topics in Numerical Analysis (pp. 61–77). Springer, Vienna. <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li> <li id="fn:6"><p>Gidas, B.; Ni, Wei-Ming; Nirenberg, Louis (1979). "Symmetry and related properties via the maximum principle." Communications in Mathematical Physics, 68(3), 209–243. <a href="/wiki/Louis_Nirenberg" target="_blank">/wiki/Louis_Nirenberg</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li> <li id="fn:7"><p>"The Patriot Missile Failure". <a href="http://www-users.math.umn.edu/~arnold//disasters/patriot.html" target="_blank">http://www-users.math.umn.edu/~arnold//disasters/patriot.html</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></p></li> <li id="fn:8"><p>ARIANE 5 Flight 501 Failure, http://sunnyday.mit.edu/nasa-class/Ariane5-report.html <a href="http://sunnyday.mit.edu/nasa-class/Ariane5-report.html" target="_blank">http://sunnyday.mit.edu/nasa-class/Ariane5-report.html</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></p></li> <li id="fn:9"><p>Rounding error changes Parliament makeup <a href="http://catless.ncl.ac.uk/Risks/13.37.html#subj4" target="_blank">http://catless.ncl.ac.uk/Risks/13.37.html#subj4</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></p></li> <li id="fn:10"><p>Yamamoto, T. (1984). Error bounds for approximate solutions of systems of equations. Japan Journal of Applied Mathematics, 1(1), 157. <a href="#fnref:10" class="footnote-back-ref">↩</a></p></li> <li id="fn:11"><p>Oishi, S., & Rump, S. M. (2002). Fast verification of solutions of matrix equations. Numerische Mathematik, 90(4), 755-773. <a href="#fnref:11" class="footnote-back-ref">↩</a></p></li> <li id="fn:12"><p>Yamamoto, T. (1980). Error bounds for computed eigenvalues and eigenvectors. Numerische Mathematik, 34(2), 189-199. <a href="#fnref:12" class="footnote-back-ref">↩</a></p></li> <li id="fn:13"><p>Yamamoto, T. (1982). Error bounds for computed eigenvalues and eigenvectors. II. Numerische Mathematik, 40(2), 201-206. <a href="#fnref:13" class="footnote-back-ref">↩</a></p></li> <li id="fn:14"><p>Mayer, G. (1994). Result verification for eigenvectors and eigenvalues. Topics in Validated Computations, Elsevier, Amsterdam, 209-276. <a href="#fnref:14" class="footnote-back-ref">↩</a></p></li> <li id="fn:15"><p>Ogita, T. (2008). Verified Numerical Computation of Matrix Determinant. SCAN’2008 El Paso, Texas September 29–October 3, 2008, 86. <a href="#fnref:15" class="footnote-back-ref">↩</a></p></li> <li id="fn:16"><p>Shinya Miyajima, Verified computation for the Hermitian positive definite solution of the conjugate discrete-time algebraic Riccati equation, Journal of Computational and Applied Mathematics, Volume 350, Pages 80-86, April 2019. <a href="#fnref:16" class="footnote-back-ref">↩</a></p></li> <li id="fn:17"><p>Shinya Miyajima, Fast verified computation for the minimal nonnegative solution of the nonsymmetric algebraic Riccati equation, Computational and Applied Mathematics, Volume 37, Issue 4, Pages 4599-4610, September 2018. <a href="#fnref:17" class="footnote-back-ref">↩</a></p></li> <li id="fn:18"><p>Shinya Miyajima, Fast verified computation for the solution of the T-congruence Sylvester equation, Japan Journal of Industrial and Applied Mathematics, Volume 35, Issue 2, Pages 541-551, July 2018. <a href="#fnref:18" class="footnote-back-ref">↩</a></p></li> <li id="fn:19"><p>Shinya Miyajima, Fast verified computation for the solvent of the quadratic matrix equation, The Electronic Journal of Linear Algebra, Volume 34, Pages 137-151, March 2018 <a href="#fnref:19" class="footnote-back-ref">↩</a></p></li> <li id="fn:20"><p>Shinya Miyajima, Fast verified computation for solutions of algebraic Riccati equations arising in transport theory, Numerical Linear Algebra with Applications, Volume 24, Issue 5, Pages 1-12, October 2017. <a href="#fnref:20" class="footnote-back-ref">↩</a></p></li> <li id="fn:21"><p>Shinya Miyajima, Fast verified computation for stabilizing solutions of discrete-time algebraic Riccati equations, Journal of Computational and Applied Mathematics, Volume 319, Pages 352-364, August 2017. <a href="#fnref:21" class="footnote-back-ref">↩</a></p></li> <li id="fn:22"><p>Shinya Miyajima, Fast verified computation for solutions of continuous-time algebraic Riccati equations, Japan Journal of Industrial and Applied Mathematics, Volume 32, Issue 2, Pages 529-544, July 2015. <a href="#fnref:22" class="footnote-back-ref">↩</a></p></li> <li id="fn:23"><p>Rump, Siegfried M. (2014). Verified sharp bounds for the real gamma function over the entire floating-point range. Nonlinear Theory and Its Applications, IEICE, 5(3), 339-348. <a href="#fnref:23" class="footnote-back-ref">↩</a></p></li> <li id="fn:24"><p>Yamanaka, Naoya; Okayama, Tomoaki; Oishi, Shin’ichi (2015, November). Verified Error Bounds for the Real Gamma Function Using Double Exponential Formula over Semi-infinite Interval. In International Conference on Mathematical Aspects of Computer and Information Sciences (pp. 224-228). Springer. <a href="#fnref:24" class="footnote-back-ref">↩</a></p></li> <li id="fn:25"><p>Johansson, Fredrik (2019). Numerical Evaluation of Elliptic Functions, Elliptic Integrals and Modular Forms. In Elliptic Integrals, Elliptic Functions and Modular Forms in Quantum Field Theory (pp. 269-293). Springer, Cham. <a href="#fnref:25" class="footnote-back-ref">↩</a></p></li> <li id="fn:26"><p>Johansson, Fredrik (2019). Computing Hypergeometric Functions Rigorously. ACM Transactions on Mathematical Software (TOMS), 45(3), 30. <a href="#fnref:26" class="footnote-back-ref">↩</a></p></li> <li id="fn:27"><p>Johansson, Fredrik (2015). Rigorous high-precision computation of the Hurwitz zeta function and its derivatives. Numerical Algorithms, 69(2), 253-270. <a href="#fnref:27" class="footnote-back-ref">↩</a></p></li> <li id="fn:28"><p>Miyajima, S. (2018). Fast verified computation for the matrix principal pth root. en:Journal of Computational and Applied Mathematics, 330, 276-288. <a href="/wiki/Journal_of_Computational_and_Applied_Mathematics" target="_blank">/wiki/Journal_of_Computational_and_Applied_Mathematics</a> <a href="#fnref:28" class="footnote-back-ref">↩</a></p></li> <li id="fn:29"><p>Miyajima, S. (2019). Verified computation for the matrix principal logarithm. Linear Algebra and its Applications, 569, 38-61. <a href="#fnref:29" class="footnote-back-ref">↩</a></p></li> <li id="fn:30"><p>Miyajima, S. (2019). Verified computation of the matrix exponential. Advances in Computational Mathematics, 45(1), 137-152. <a href="#fnref:30" class="footnote-back-ref">↩</a></p></li> <li id="fn:31"><p>Johansson, Fredrik (2017). Arb: efficient arbitrary-precision midpoint-radius interval arithmetic. IEEE Transactions on Computers, 66(8), 1281-1292. <a href="#fnref:31" class="footnote-back-ref">↩</a></p></li> <li id="fn:32"><p>Johansson, Fredrik (2018, July). Numerical integration in arbitrary-precision ball arithmetic. In International Congress on Mathematical Software (pp. 255-263). Springer, Cham. <a href="#fnref:32" class="footnote-back-ref">↩</a></p></li> <li id="fn:33"><p>Johansson, Fredrik; Mezzarobba, Marc (2018). Fast and Rigorous Arbitrary-Precision Computation of Gauss--Legendre Quadrature Nodes and Weights. SIAM Journal on Scientific Computing, 40(6), C726-C747. <a href="/wiki/SIAM_Journal_on_Scientific_Computing" target="_blank">/wiki/SIAM_Journal_on_Scientific_Computing</a> <a href="#fnref:33" class="footnote-back-ref">↩</a></p></li> <li id="fn:34"><p>Eberhard Zeidler, Nonlinear Functional Analysis and Its Applications I-V. Springer Science & Business Media. <a href="/wiki/Eberhard_Zeidler_(mathematician)" target="_blank">/wiki/Eberhard_Zeidler_(mathematician)</a> <a href="#fnref:34" class="footnote-back-ref">↩</a></p></li> <li id="fn:35"><p>Mitsuhiro T. Nakao, Michael Plum, Yoshitaka Watanabe (2019) Numerical Verification Methods and Computer-Assisted Proofs for Partial Differential Equations (Springer Series in Computational Mathematics). <a href="#fnref:35" class="footnote-back-ref">↩</a></p></li> <li id="fn:36"><p>Eberhard Zeidler, Nonlinear Functional Analysis and Its Applications I-V. Springer Science & Business Media. <a href="/wiki/Eberhard_Zeidler_(mathematician)" target="_blank">/wiki/Eberhard_Zeidler_(mathematician)</a> <a href="#fnref:36" class="footnote-back-ref">↩</a></p></li> <li id="fn:37"><p>Oishi, Shin’ichi; Tanabe, Kunio (2009). Numerical Inclusion of Optimum Point for Linear Programming. JSIAM Letters, 1, 5-8. <a href="#fnref:37" class="footnote-back-ref">↩</a></p></li> </ol>