Automatic reasoning about numerical stability of rational expressions

ABSTRACT

While numerical (e.g. Fortran) code generation from computer algebra is nowadays relatively easy to do, the expressions as they are produced via computer algebra typically benefit from non-trivial reformulation for efficiency and numerical stability. To assist in automatic “expert reformulation”, we desire good automated tools to assess the stability of a particular form of an expression. In this paper, we discuss an approach to proofs of numerical stability (with respect to roundoff error) of rational expressions. The proof technique is based upon the ability to propagate properties such as sign, exact representability, or a certain kind of numerical stability, to floating point results from properties of their antecedents. The qualitative approach to numerical stability (inspired by [12]) lends itself to implementation as a backwards-chaining theorem prover. While it is not a replacement for alternative forms of stability analysis, it can sometimes discover stability and explain it straightforwardly.

REFERENCES

• 1: AMERICAN NATIONAL STANDARDS INSTI- TUTE/THE INSTITUTE OF ELECTRICAL AND ELECTRONICS ENGINEERS, INC., IEEE Standard for Binary Floating-Point Arithmetic, New York, 1985. ANSI/IEEE Std 754-1985.
• 2: ----, IEEE Standard for Radiz-Independeni Floating-Point Arithmetic, New York, 1987. ANSI/IEEE Std 854-1987.
• 3: W. BLEDSOE, Non-resolution theorem proving, Artificial Intelligence, 9 (1977).
• 4: B. C~{^R, K. OBDDES, O. GONNET, M. MONAGAN, AND S. WATT, Maple Reference Manual, 5th edition, Waterloo, Ontario, Canada, 1988.
• 5: C. T. FIKE, Computer Evaluation of Mathematical Functions, Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 1968.
• 6: Barbara L. Gates, A numerical code generation facility for REDUCE, Proceedings of the fifth ACM symposium on Symbolic and algebraic computation, p.94-99, July 21-23, 1986, Waterloo, Ontario, Canada [doi>10.1145/32439.32459]
• 7: T. HULL, The use of controlled precision, in The Relationship between numerical computation and programming languages, J. Reid, ed., North-Holland, 1982, pp. 71-84.
• 8: Ben J. A. Hulshof , J. A. van Hulzen, Automatic Error Cumulation Control, Proceedings of the International Symposium on Symbolic and Algebraic Computation, p.260-271, July 09-11, 1984
• 9: U W Kulisch , W L Miranker, The arithmetic of the digital computer: A new approach, SIAM Review, v.28 n.1, p.1-40, March 1986 [doi>10.1137/1028001]
• 10: Douglas H. Lanam, An algebraic front-end for the production and use of numeric programs, Proceedings of the fourth ACM symposium on Symbolic and algebraic computation, p.223-227, August 05-07, 1981, Snowbird, Utah, United States [doi>10.1145/800206.806400]
• 11: J. L. LAiR. SON AND A. H. SAMEH, Algorithms for roundoff error analysis - a relalive error approach, Computing, 24 (1980), pp. 275- 297.
• 12: C. MESZTENYI AND C. WITZGALI,, Stable Evaluation of Polynomials, Journal of Research of the National Bureau of Standards - B. Mathematics and Mathematical Physics, 71B (1967), pp. ll-l?.
• 13: W. MILLEa AND C. WRATHALL, Software for Roundoff Analysis of Matrix Algorithms, Academic Press, Inc., New York, 1980.
• 14: M. MUTRm, B. CHAR, AND R. BAa- TELS, Expression Optimization using High- Level Knowledge, tech. rep., University of Waterloo, Waterloo, Ontario, CANADA N2L 3G I, i987. Research Report CS-87-09.
• 15: M. P. W. MUTRIE, P~. H. BARTELS, AND B. W. C~AR, Floating-point error analysis using symbolic algebraic computation, tech. rep., University of Waterloo, Department of Computer Science, 1987. Research Report CS-87-08. Presented at the Conference on Computer~ and Mathematics, Stanford University, Stanford, California, July, 1986.
• 16: Edward W. Ng, Symbolic-Numeric Interface: a review (in absentia), Proceedings of the International Symposiumon on Symbolic and Algebraic Computation, p.330-345, June 01, 1979
• 17: E. SACKS, Automatic qualitative analysis of ordinary differential equations using piecewise linear approximations, PhD thesis, Massachusetts Institute of Technology, 1988. Available as Laboratory for Computer Science technical report MIT/LCS/TR-416.
• 18: S. STEINBERG AND P. ROACHE, Using Vaxima to Write Fortran Code, in Proceedings of the 1984 Macsyma User's Conference, V. E. Golden, ed., General Electric, Schenectady, New York, July 1984, pp. 1-22.
• 19: David R. Stoutemyer, Automatic Error Analysis Using Computer Algebraic Manipulation, ACM Transactions on Mathematical Software (TOMS), v.3 n.1, p.26-43, March 1977 [doi>10.1145/355719.355721]
• 20: James H. Wilkinson, Rounding Errors in Algebraic Processes, Dover Publications, Incorporated, 1994
• 21: Stephen Wolfram, Mathematica: a system for doing mathematics by computer, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Code generation

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.0 General
          Subjects: Computer arithmetic

General Terms:
Algorithms, Theory