Synthesis of optimal numerical algorithms using real quantifier elimination (case study: square root computation)

ABSTRACT

We report on on-going efforts to apply real quantifier elimination to the synthesis of optimal numerical algorithms. In particular, we describe a case study on the square root problem: given a real number x and an error bound ε, find a real interval such that it contains [EQUATION] and its width is less than or equal to ε.

A typical numerical algorithm starts with an initial interval and repeatedly updates it by applying a "refinement map" on it until it becomes narrow enough. Thus the synthesis amounts to finding a refinement map that ensures the correctness and optimality of the resulting algorithm.

This problem can be formulated as a real quantifier elimination. Hence, in principle, the synthesis can be carried out automatically. However, the computational requirement is huge, making the automatic synthesis practically impossible with the current general real quantifier elimination software.

We overcame the difficulty by (1) carefully reducing a complicated quantified formula into several simpler ones and (2) automatically eliminating the quantifiers from the resulting ones using the state of the art quantifier elimination software.

As the result, we were able to synthesize semi-automatically, under mild assumptions, a class of optimal maps, which are significantly better than the well known hand-crafted Secant-Newton map. Interestingly, the optimal synthesized maps are not contracting as one would naturally expect.

References

1. B. Akbarpour and L. C. Paulson. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. J. Autom. Reasoning, 44(3):175--205, 2010.
2. G. Alefeld and J. Herzberger. Introduction to Interval Computations. Academic Press, Inc., New York, NY, 1983.
3. H. Anai and V. Weispfenning. Set Computations Using Real Quantifier Elimination. In HSCC, pages 63--76, 2001.
4. D. S. Arnon. A Cluster-based Cylindrical Algebraic Decomposition Algorithm. J. Symb. Comput., 5(1-2):189--212, 1988.
5. S. Basu, R. Pollack, and M.-F. Roy. On the Combinatorial and Algebraic Complexity of Quantifier Elimination. J. ACM, 43(6):1002--1045, 1996.
6. N. Beebe. Accurate Square Root Computation. Technical report, Center for Scientific Computing, Department of Mathematics, University of Utah, 1991.
7. R. Bradford, J. H. Davenport, M. England, S. McCallum, and D. Wilson. Cylindrical Algebraic Decompositions for Boolean Combinations. In ISSAC, pages 125--132, 2013.
8. C. W. Brown. Improved Projection for Cylindrical Algebraic Decomposition. J. Symb. Comput., 32(5):447--465, 2001.
9. C. W. Brown. Simple CAD Construction and Its Applications. J. Symb. Comput., 31(5):521--547, 2001.
10. C. W. Brown. QEPCAD-B: A Program for Computing with Semi-algebraic Sets using CADs. SIGSAM Bulletin, 37(4):97--108, 2003.
11. C. W. Brown. Fast Simplifications for Tarski Formulas based on Monomial Inequalities. J. Symb. Comput., 47(7):859--882, 2012.
12. C. W. Brown. Constructing a Single Open Cell in a Cylindrical Algebraic Decomposition. In ISSAC, pages 133--140, 2013.
13. B. Caviness and J. Johnson, editors. Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and monographs in symbolic computation, Springer, 1998.
14. W. Cody and W. Waite. Software Manual for the Elementary Functions. Prentice-Hall, Englewood Cliffs, NJ, 1980.
15. G. E. Collins. Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition. In Automata Theory and Formal Languages, 1975.
16. G. E. Collins and H. Hong. Cylindrical Algebraic Decomposition for Quantifier Elimination. J. Symb. Comput., 12(3):299--328, 1991.
17. A. Dolzmann, A. Seidl, and T. Sturm. Efficient Projection Orders for CAD. In ISSAC, pages 111--118, 2004.
18. A. Dolzmann and T. Sturm. REDLOG: Computer Algebra Meets Computer Logic. SIGSAM Bulletin (ACM Special Interest Group on Symbolic and Algebraic Manipulation), 31(2):2--9, 1997.
19. M. Erascu and H. Hong. The Secant-Newton Map is Optimal Among Contracting Quadratic Maps for Square Root Computation. Journal of Reliable Computing, 18:73--81, 2013.
20. D. Fowler and E. Robson. Square Root Approximations in Old Babylonian Mathematics: YBC 7289 in Context. Historia Mathematica, 25(4):366--378, 1998.
21. D. Grigoriev. Complexity of Deciding Tarski Algebra. J. Symb. Comput., 5(1-2):65--108, 1988.
22. J. F. Hart, E. W. Cheney, C. L. Lawson, H. J. Maehly, C. K. Mesztenyi, J. R. Rice, H. C. Thacher Jr., and C. Witzgall. Computer Approximations. John Wiley, 1968. Reprinted, E. Krieger Publishing Company (1978).
23. H. Hong. An Improvement of the Projection Operator in Cylindrical Algebraic Decomposition. In ISSAC, pages 261--264, 1990.
24. H. Hong. Simple Solution Formula Construction in Cylindrical Algebraic Decomposition Based Quantifier Elimination. In ISSAC, pages 177--188, 1992.
25. H. Hong. Special Issue Editorial: Computational Quantifier Elimination. The Computer Journal, 1993.
26. H. Hong and M. S. E. Din. Variant Quantifier Elimination. J. Symb. Comput., 47(7):883--901, 2012.
27. R. Liska and S. Steinberg. Applying Quantifier Elimination to Stability Analysis of Difference Schemes. Comput. J., 36(5):497--503, 1993.
28. S. McCallum. An Improved Projection Operation for Cylindrical Algebraic Decomposition of Three-Dimensional Space. J. Symb. Comput., 5(1-2):141--161, 1988.
29. S. McCallum. On Projection in CAD-based Quantifier Elimination with Equational Constraint. In ISSAC, pages 145--149, 1999.
30. S. McCallum. On Propagation of Equational Constraints in CAD-based Quantifier Elimination. In ISSAC, pages 223--231, 2001.
31. J. R. Meggitt. Pseudo Division and Pseudo Multiplication Processes. IBM Journal of Research and Development, 6(2):210--226, 1962.
32. R. E. Moore. Interval Analysis. Prentice-Hall, Englewood Cliffs, NJ, 1966.
33. R. E. Moore, R. B. Kearfott, and M. J. Cloud. Introduction to Interval Analysis. Society for Industrial and Applied Mathematics, Philadelphia, PA, 2009.
34. J. Renegar. On the Computational Complexity and Geometry of the First-Order Theory of the Reals. J. Symb. Comput., 13(3):255--352, 1992.
35. N. Revol. Interval Newton Iteration in Multiple Precision for the Univariate Case. Numerical Algorithms, 34(2-4):417--426, 2003.
36. A. Strzebonski. Cylindrical Algebraic Decomposition using Validated Numerics. J. Symb. Comput., 41(9):1021--1038, 2006.
37. A. Strzeboski. Cylindrical Decomposition for Systems Transcendental in the First Variable. J. Symb. Comput., 46(11):1284--1290, 2011.
38. A. Tarski. A Decision Method for Elementary Algebra and Geometry. Bulletin of the American Mathematical Society, 1951.
39. J. H. Wensley. A Class of Non-Analytical Iterative Processes. The Computer Journal, 1(4):163--167, 1959.
40. I. Wolfram Research. Mathematica Edition: Version 8.0. Wolfram Research, Inc., 2010.

Index Terms

• Applied computing

  • Physical sciences and engineering

    • Mathematics and statistics

• Computing methodologies

  • Symbolic and algebraic manipulation

    • Computer algebra systems

• Mathematics of computing

  • Mathematical analysis

    • Mathematical optimization

    • Numerical analysis

• Theory of computation

  • Design and analysis of algorithms

    • Mathematical optimization