View source for Validated numerics

'''Validated numerics''', or '''rigorous computation''', '''verified computation''', '''reliable computation''', '''numerical verification''' ({{lang-de|
Zuverlässiges Rechnen}}) is numerics including mathematically strict error (rounding error, truncation error, discretization error) evaluation, and it is one field of [[Numerical analysis|numerical analysis]]. For computation, [[Interval arithmetic|interval arithmetic]] is used, and all results are represented by intervals. Validated numerics were used by Warwick Tucker in order to solve the 14th of [[Smale's problems]],<ref name="Tucker_1999"/> and today it is recognized as a powerful tool for the study of dynamical systems.<ref name="Kokubu"/>

==Importance==
Computation without verification may cause unfortunate results. Below are some examples.

===Rump's example===
In the 1980s, Rump made an example.<ref name="Rump_1988"/><ref name="Loh_2002"/> 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.

===Phantom solution===
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.<ref name="Breuer_2001"/> This result to the study conflicted to the theoretical study by Gidas–Ni–Nirenberg which claimed that there is no asymmetric solution.<ref name="Gidas_1979"/> 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.

===Accidents caused by numerical errors===
The following examples are known as accidents caused by numerical errors:
* Failure of intercepting missiles in the Gulf War (1991)<ref name="Arnold"/>
* Failure of the [[Engineering:Ariane 5|Ariane 5]] rocket (1996)<ref name="Ariane"/>
* Mistakes in election result totalization<ref name="Makeup"/>

==Main topics==
The study of validated numerics is divided into the following fields:
{{columns-list|colwidth=22em|
* Verification in [[Numerical linear algebra|numerical linear algebra]]
** Validating numerical solutions of a given system of linear equations<ref>Yamamoto, T. (1984). Error bounds for approximate solutions of systems of equations. Japan Journal of Applied Mathematics, 1(1), 157.</ref><ref>Oishi, S., & Rump, S. M. (2002). Fast verification of solutions of matrix equations. Numerische Mathematik, 90(4), 755-773.</ref>
** Validating numerically obtained eigenvalues<ref>Yamamoto, T. (1980). Error bounds for computed eigenvalues and eigenvectors. Numerische Mathematik, 34(2), 189-199.</ref><ref>Yamamoto, T. (1982). Error bounds for computed eigenvalues and eigenvectors. II. Numerische Mathematik, 40(2), 201-206.</ref><ref>Mayer, G. (1994). Result verification for eigenvectors and eigenvalues. Topics in Validated Computations, Elsevier, Amsterdam, 209-276.</ref>
** Rigorously computing [[Determinant|determinant]]s<ref>Ogita, T. (2008). Verified Numerical Computation of Matrix Determinant. SCAN’2008 El Paso, Texas September 29–October 3, 2008, 86.</ref>
** Validating numerical solutions of matrix equations<ref>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.</ref><ref>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.</ref><ref>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.</ref><ref>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</ref><ref>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.</ref><ref>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.</ref><ref>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.</ref>
* Verification of [[Special functions|special functions]]:
** [[Gamma function]]<ref name="Rump_2014"/><ref name="Yamanaka_2015"/>
** Elliptic functions<ref name="Johansson_2019_1"/>
** Hypergeometric functions<ref name="Johansson_2019_2"/>
** [[Hurwitz zeta function]]<ref name="Johansson_2015"/>
** [[Bessel function]]
** [[Matrix function]]<ref>Miyajima, S. (2018). Fast verified computation for the matrix principal pth root. :en:Journal of Computational and Applied Mathematics, 330, 276-288.</ref><ref>Miyajima, S. (2019). Verified computation for the matrix principal logarithm. Linear Algebra and its Applications, 569, 38-61.</ref><ref>Miyajima, S. (2019). Verified computation of the matrix exponential. Advances in Computational Mathematics, 45(1), 137-152.</ref>
* Verification of numerical quadrature<ref name="Johansson_2017"/><ref name="Johansson_2018_1"/><ref name="Johansson_2018_2"/>
* Verification of nonlinear equations (The [[Kantorovich theorem]],<ref name="zeidler"/> Krawczyk method, interval Newton method, and the Durand–Kerner–Aberth method are studied.)
* Verification for solutions of ODEs, PDEs<ref name="nakao"/> (For PDEs, knowledge of [[Functional analysis|functional analysis]] are used.<ref name="zeidler"/>)
* Verification of [[Linear programming|linear programming]]<ref name="Oishi_2009"/>
* Verification of [[Computational geometry|computational geometry]]
* Verification at high-performance computing environment
}}

==Tools==
{{columns-list|colwidth=22em|
* [https://www.tuhh.de/ti3/rump/intlab/ INTLAB] Library made by [[Software:MATLAB|MATLAB]]/[[Software:GNU Octave|GNU Octave]]
* [http://verifiedby.me/kv/index-e.html kv] Library made by [[C++]]. This library can obtain multiple precision outputs by using [[Software:GNU MPFR|GNU MPFR]].
** {{GitHub|mskashi/kv}}
* [http://arblib.org/ Arb] Library made by [[C (programming language)|C]]. It is capable to rigorously compute various [[Special functions|special functions]].
** {{GitHub|fredrik-johansson/arb}}
* [http://capd.ii.uj.edu.pl/ CAPD] A collection of flexible C++ modules which are mainly designed to computation of homology of sets, maps and validated numerics for dynamical systems.
* {{GitHub|JuliaIntervals}} (Library made by [[Julia (programming language)|Julia]])
* [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].
** {{GitHub|safe_numerics}}
}}

==See also==
{{columns-list|colwidth=22em|
* [[Computer-assisted proof]]
* [[Interval arithmetic]]
* [[Affine arithmetic]]
* [[Software:INTLAB|INTLAB]] (Interval Laboratory)
* [[Automatic differentiation]]
* wikibooks:Numerical calculations and rigorous mathematics
* [[Kantorovich theorem]]
* [[Gershgorin circle theorem]]
* Ulrich W. Kulisch
}}

==References==
{{Reflist|refs=
<ref name="Tucker_1999">Tucker, Warwick. (1999). "The Lorenz attractor exists." ''Comptes Rendus de l'Académie des Sciences-Series I-Mathematics'', 328(12), 1197–1202.</ref>
<ref name="Kokubu">Zin Arai, Hiroshi Kokubu, Paweãl Pilarczyk. [https://www.math.kyoto-u.ac.jp/~kokubu/preprints/rigdynam.pdf Recent Development In Rigorous Computational Methods In Dynamical Systems].</ref>
<ref name="Rump_1988">Rump, Siegfried M. (1988). "Algorithms for verified inclusions: Theory and practice." In ''Reliability in computing'' (pp. 109–126). Academic Press.</ref>
<ref name="Loh_2002">Loh, Eugene; Walster, G. William (2002). Rump's example revisited. Reliable Computing, 8(3), 245-248.</ref>
<ref name="Breuer_2001">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.</ref>
<ref name="Gidas_1979">Gidas, B.; Ni, Wei-Ming; Nirenberg, Louis (1979). "Symmetry and related properties via the maximum principle." ''Communications in Mathematical Physics'', 68(3), 209–243.</ref>
<ref name="Arnold">{{Cite web|url=http://www-users.math.umn.edu/~arnold//disasters/patriot.html|title = The Patriot Missile Failure}}</ref>
<ref name="Ariane">ARIANE 5 Flight 501 Failure, http://sunnyday.mit.edu/nasa-class/Ariane5-report.html</ref>
<ref name="Makeup">[http://catless.ncl.ac.uk/Risks/13.37.html#subj4 Rounding error changes Parliament makeup]</ref>
<ref name="Rump_2014">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.</ref>
<ref name="Yamanaka_2015">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.</ref>
<ref name="Johansson_2019_1">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.</ref>
<ref name="Oishi_2009">Oishi, Shin’ichi; Tanabe, Kunio (2009). Numerical Inclusion of Optimum Point for Linear Programming. JSIAM Letters, 1, 5-8.</ref> 
<ref name="Johansson_2019_2">Johansson, Fredrik (2019). Computing Hypergeometric Functions Rigorously. ACM Transactions on Mathematical Software (TOMS), 45(3), 30.</ref>
<ref name="Johansson_2015">Johansson, Fredrik (2015). Rigorous high-precision computation of the Hurwitz zeta function and its derivatives. Numerical Algorithms, 69(2), 253-270.</ref>
<ref name="Johansson_2017">Johansson, Fredrik (2017). Arb: efficient arbitrary-precision midpoint-radius interval arithmetic. IEEE Transactions on Computers, 66(8), 1281-1292.</ref>
<ref name="Johansson_2018_1">Johansson, Fredrik (2018, July). Numerical integration in arbitrary-precision ball arithmetic. In International Congress on Mathematical Software (pp. 255-263). Springer, Cham.</ref>
<ref name="Johansson_2018_2">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.</ref>
<ref name="zeidler">[[Biography:Eberhard Zeidler (mathematician)|Eberhard Zeidler]], Nonlinear Functional Analysis and Its Applications I-V. Springer Science & Business Media.</ref>
<ref name="nakao">Mitsuhiro T. Nakao, Michael Plum, Yoshitaka Watanabe (2019) Numerical Verification Methods and Computer-Assisted Proofs for Partial Differential Equations (Springer Series in Computational Mathematics).</ref>
}}

==Further reading==
* Tucker, Warwick (2011). Validated Numerics: A Short Introduction to Rigorous Computations. Princeton University Press.
* Moore, Ramon Edgar, Kearfott, R. Baker., Cloud, Michael J. (2009). Introduction to Interval Analysis. Society for Industrial and Applied Mathematics.
* Rump, Siegfried M. (2010). Verification methods: Rigorous results using floating-point arithmetic. [[Acta Numerica]], 19, 287–449.

==External links==
* [http://www2.math.uu.se/~warwick/main/papers/ECM04Tucker.pdf Validated Numerics for Pedestrians]
* [https://interval.louisiana.edu/reliable-computing-journal/ Reliable Computing], 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.

{{Numerical PDE}}
{{Industrial and applied mathematics}}

[[Category:Numerical analysis]]
[[Category:Computational science]]

{{Sourceattribution|Validated numerics}}