How to Develop and Utilize Numerical Algorithms with Automatic Result Verification?

Abstract

Advances in computer technology axe now so profound that the arithmetic capability and repertoire of computers can and should be expanded. The quality of the elementary floating-point operations should be extended to the most frequent numerical data types or mathematical spaces of computation (vectors, matrices, complex numbers and intervals over these types). A VLSI coprocessor chip with integrated PCI-interface has been developed which provides these operations. The expanded capability is gained at modest hardware cost and does not implicate a performance penalty. Language and programming support (the -XSC languages) are available. There, the chip’s functionality is directly coupled to the operator symbols for the corresponding data types. By operator overloading a long real arithmetic (array of reals) and long interval arithmetic as well as automatic differentiation arithmetic become part of the runtime system of the compiler. I. e. derivatives, Taylor-coefficients, gradients, Jacobian and Hessian matrices or enclosures of these are directly computed out of the expression by a simple type change of the operands. Techniques are now available so that with this expanded capability, the computer itself can be used to appraise the quality and the reliability of the computed results over a wide range of applications. Program packages for many standard problems of Numerical Analysis have been developed where the computer itself verifies the correctness of the computed result and proves existence and uniqueness of the solution within the computed bounds.

Many applications require that rigorous mathematics can be done with the computer using floating-point. As an example, this is essential in simulation runs (fusion reactor) or mathematical modeling where the user has to distinguish between computational artifacts and genuine reactions of the model. The model can only be developed systematically if errors entering into the computation can be essentially excluded. Automatic result verification re-integrates digital computing into real mathematics.