Rigorous error analysis of numerical algorithms via symbolic computations (Q674759)

When performing a numerical calculation on a computer, we want to obtain an exact estimate of the total error of the obtained result. This error may be estimated by the sum of the truncation error of the used numerical method (e.g. the approximation of a given function by a polynomial) and the rounding error produced during the calculation process, dependent on the used machine arithmetic. The main result of the paper is a theorem, giving foundations to a technique providing rigorous a priori bounds for the rounding error obtained when we compute a polynomial expression (approximating a calculated function) in a floating point arithmetic. This arithmetic decides on both the precision of the representation of input data and the precision of results of arithmetic operations. When the way of the evaluation of the polynomial expression is uniquely determined (e.g. its algorithm is described by the configuration of parentheses in the expression), it is possible to calculate rigorous rounding error bounds using the symbolic calculus. Such a technique is an alternative to the commonly used calculations of error bounds in the interval arithmetic. The technique was invented to perform the computer-assisted proof of chaos in the Lorenz equation; this application of the approach is presented in the paper as an example implemented in MATHEMATICA, using the fourth-order Runge-Kutta method. The program in MATHEMATICA, calculating error bounds for this example is displayed in the Appendix..