High-level proofs of mathematical programs using automatic differentiation, simplification, and some common sense

ABSTRACT

One problem in applying elementary methods to prove correctness of interesting scientific programs is the large discrepancy in level of discourse between low-level proof methods and the logic of scientific calculation, especially that used in a complex numerical program. The justification of an algorithm typically relies on algebra or analysis, but the correctness of the program requires that the arithmetic expressions are written correctly and that iterations converge to correct values in spite of truncation of infinite processes or series and the commission of numerical roundoff errors. We hope to help bridge this gap by showing how we can, in some cases, state a high-level requirement and by using a computer algebra system (CAS) demonstrate that a program satisfies that requirement. A CAS can contribute program manipulation, partial evaluation, simplification or other algorithmic methods. A novelty here is that we add to the usual list of techniques automatic differentiation, a method already widely used in optimization contexts where algorithms are differentiated. We sketch a proof of a numerical program to compute sine, and display a related approach to a version of a Bessel function algorithm for J0(x) based on a recurrence.

REFERENCES

• 1: Milton Abramowitz, Handbook of Mathematical Functions, With Formulas, Graphs, and Mathematical Tables,, Dover Publications, Incorporated, 1974
• 2: A Collection of Automatic Differentiation Tools. http://www-unix.mcs.anl.gov/autodiff/AD_Tools/
• 3: Michael Beeler , R. W Gosper , Rich Schroeppel, HAKMEM, Massachusetts Institute of Technology, Cambridge, MA, 1972
• 4: A. Bundy. "A Survey of Automated Deduction". Lecture Notes in Computer Science volume 1600, Springer-Verlag, 1999.
• 5: N. de Bruijn. A survey of the project AUTOMATH, in J. Seldin and J. Hindley, eds, `To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism', Academic Press, 1980,pp. 579---606.
• 6: G. Dowek, Felty A., Herbelin H., Huet G., Murthy C., Parent C., Paulin-Mohring C. and Werner B. {1993}, "The Coq proof assistant user's guide," Rapport Techniques 154, INRIA, Rocquencourt, France. Version 5.8.
• 7: John Harrison, Formal Verification of Floating Point Trigonometric Functions, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.217-233, November 01-03, 2000
• 8: John McCarthy, Recursive functions of symbolic expressions and their computation by machine, Part I, Communications of the ACM, v.3 n.4, p.184-195, April 1960 [doi>10.1145/367177.367199]
• 9: R. J. Fateman, Series solutions of algebraic and differential equations: a comparison of linear and quadratic algebraic convergence, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation, p.11-16, July 17-19, 1989, Portland, Oregon, United States [doi>10.1145/74540.74543]
• 10: R. Fateman."Compiling functional pipe/stream abstractions into conventional programs: Software Pipelines," on-line notes.
• 11: R. Fateman."Programs for evaluating polynomials," on-line notes.
• 12: Michael B. Monagan , Walter M. Neuenschwander, GRADIENT: algorithmic differentiation in Maple, Proceedings of the 1993 international symposium on Symbolic and algebraic computation, p.68-76, July 06-08, 1993, Kiev, Ukraine [doi>10.1145/164081.164095]
• 13: Ronitt Rubinfeld , Madhu Sudan, Robust Characterizations of Polynomials withApplications to Program Testing, SIAM Journal on Computing, v.25 n.2, p.252-271, February 1996 [doi>10.1137/S0097539793255151]
• 14: Benjamin Price Shults , Larry Hines , Robert Boyer, Discoveries and experiments in the automation of mathematical reasoning, 1997
• 15: Ian Sommerville, Software engineering (6th ed.), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2001
• 16: Wen-Tsun Wu, Mathematics Mechanization: Mechanical Geometry Theorem-Proving, Mechanical Geometry Problem-Solving, and Polynomial Equations-Solving, Kluwer Academic Publishers, Norwell, MA, 2001
• 17: F. Wiedijk, "Conditional Computing (what proof checking needs from computer algebra)" on-line notes. http://www.cs.kun.nl/˜freek/notes/.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.1 Expressions and Their Representation
          Subjects: Simplification of expressions

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program verification

General Terms:
Algorithms, Design, Languages, Theory

Keywords:
Bessel, differentiation, proof, recurrence, sine