zbMATH — the first resource for mathematics

Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation). (English) Zbl 1335.68300
Summary: We report on our 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 \(\varepsilon\), find a real interval such that it contains \(\sqrt{x}\) and its width is less than or equal to \(\varepsilon\).
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 an optimal quadratically convergent map, which is better than the well known hand-crafted Secant-Newton map. Interestingly, the optimal synthesized map is not contracting as one would naturally expect.

68W30 Symbolic computation and algebraic computation
03C10 Quantifier elimination, model completeness, and related topics
65G40 General methods in interval analysis
Full Text: DOI
[1] Akbarpour, B.; Paulson, L. C., Metitarski: an automatic theorem prover for real-valued special functions, J. Autom. Reason., 44, 3, 175-205, (2010) · Zbl 1215.68206
[2] Alefeld, G.; Herzberger, J., Introduction to interval computations, (1983), Academic Press, Inc. New York, NY
[3] Anai, H.; Weispfenning, V., Set computations using real quantifier elimination, (HSCC, (2001)), 63-76 · Zbl 0991.93008
[4] Arnon, D. S., A cluster-based cylindrical algebraic decomposition algorithm, J. Symb. Comput., 5, 1-2, 189-212, (1988) · Zbl 0648.68056
[5] Basu, S.; Pollack, R.; Roy, M.-F., On the combinatorial and algebraic complexity of quantifier elimination, J. ACM, 43, 6, 1002-1045, (1996) · Zbl 0885.68070
[6] Beebe, N., Accurate square root computation, (1991), Center for Scientific Computing, Department of Mathematics, University of Utah
[7] Bradford, R.; Davenport, J. H.; England, M.; McCallum, S.; Wilson, D., Cylindrical algebraic decompositions for Boolean combinations, (ISSAC, (2013)), 125-132 · Zbl 1359.68327
[8] Brown, C. W., Improved projection for cylindrical algebraic decomposition, J. Symb. Comput., 32, 5, 447-465, (2001) · Zbl 0981.68186
[9] Brown, C. W., Simple CAD construction and its applications, J. Symb. Comput., 31, 5, 521-547, (2001) · Zbl 0976.65023
[10] Brown, C. W., QEPCAD-B: a program for computing with semi-algebraic sets using cads, SIGSAM Bull., 37, 4, 97-108, (2003) · Zbl 1083.68148
[11] Brown, C. W., Fast simplifications for Tarski formulas based on monomial inequalities, J. Symb. Comput., 47, 7, 859-882, (2012) · Zbl 1262.68189
[12] Brown, C. W., Constructing a single open cell in a cylindrical algebraic decomposition, (ISSAC, (2013)), 133-140 · Zbl 1360.68924
[13] (Caviness, B.; Johnson, J., Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts Monogr. Symbolic Comput, (1998), Springer)
[14] Cody, W.; Waite, W., Software manual for the elementary functions, (1980), Prentice Hall Englewood Cliffs, NJ · Zbl 0468.68036
[15] Collins, G. E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (Automata Theory and Formal Languages, (1975)) · Zbl 0318.02051
[16] Collins, G. E.; Hong, H., Cylindrical algebraic decomposition for quantifier elimination, J. Symb. Comput., 12, 3, 299-328, (1991) · Zbl 0754.68063
[17] Dolzmann, A.; Seidl, A.; Sturm, T., Efficient projection orders for CAD, (ISSAC, (2004)), 111-118 · Zbl 1134.68575
[18] Dolzmann, A.; Sturm, T., REDLOG: computer algebra meets computer logic, SIGSAM Bull., 31, 2, 2-9, (1997)
[19] Erascu, M.; Hong, H., The secant-Newton map is optimal among contracting quadratic maps for square root computation, J. Reliab. Comput., 18, 73-81, (2013)
[20] Erascu, M.; Hong, H., Synthesis of optimal numerical algorithms using real quantifier elimination (case study: square root computation), (ISSAC, (2014)), 162-169 · Zbl 1325.68276
[21] Fowler, D.; Robson, E., Square root approximations in old Babylonian mathematics: YBC 7289 in context, Hist. Math., 25, 4, 366-378, (1998) · Zbl 0917.01005
[22] Grigoriev, D., Complexity of deciding Tarski algebra, J. Symb. Comput., 5, 1-2, 65-108, (1988) · Zbl 0689.03021
[23] Hart, J. F.; Cheney, E. W.; Lawson, C. L.; Maehly, H. J.; Mesztenyi, C. K.; Rice, J. R.; Thacher, H. C.; Witzgall, C., Computer approximations, (1968), John Wiley, Reprinted, E. Krieger Publishing Company, 1978 · Zbl 0174.20402
[24] Hong, H., An improvement of the projection operator in cylindrical algebraic decomposition, (ISSAC, (1990)), 261-264
[25] Hong, H., Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination, (ISSAC, (1992)), 177-188 · Zbl 0919.03029
[26] Hong, H., Special issue editorial: computational quantifier elimination, Comput. J, (1993)
[27] Hong, H.; Din, M. S.E., Variant quantifier elimination, J. Symb. Comput., 47, 7, 883-901, (2012) · Zbl 1238.14001
[28] Liska, R.; Steinberg, S., Applying quantifier elimination to stability analysis of difference schemes, Comput. J., 36, 5, 497-503, (1993) · Zbl 0780.68075
[29] McCallum, S., An improved projection operation for cylindrical algebraic decomposition of three-dimensional space, J. Symb. Comput., 5, 1-2, 141-161, (1988) · Zbl 0648.68054
[30] McCallum, S., On projection in CAD-based quantifier elimination with equational constraint, (ISSAC, (1999)), 145-149
[31] McCallum, S., On propagation of equational constraints in CAD-based quantifier elimination, (ISSAC, (2001)), 223-231 · Zbl 1356.68287
[32] Meggitt, J. R., Pseudo division and pseudo multiplication processes, IBM J. Res. Dev., 6, 2, 210-226, (1962) · Zbl 0201.48709
[33] Moore, R. E., Interval analysis, (1966), Prentice Hall Englewood Cliffs, NJ · Zbl 0176.13301
[34] Moore, R. E.; Kearfott, R. B.; Cloud, M. J., Introduction to interval analysis, (2009), Society for Industrial and Applied Mathematics Philadelphia, PA · Zbl 1168.65002
[35] Renegar, J., On the computational complexity and geometry of the first-order theory of the reals, J. Symb. Comput., 13, 3, 255-352, (1992) · Zbl 0798.68073
[36] Revol, N., Interval Newton iteration in multiple precision for the univariate case, Numer. Algorithms, 34, 2-4, 417-426, (2003) · Zbl 1035.65051
[37] Strzebonski, A., Cylindrical algebraic decomposition using validated numerics, J. Symb. Comput., 41, 9, 1021-1038, (2006) · Zbl 1124.68123
[38] Strzeboski, A., Cylindrical decomposition for systems transcendental in the first variable, J. Symb. Comput., 46, 11, 1284-1290, (2011) · Zbl 1236.14053
[39] Tarski, A., A decision method for elementary algebra and geometry, Bull. Am. Math. Soc, (1951) · Zbl 0044.25102
[40] Wolfram Research, I., Mathematica edition: version 8.0, (2010), Wolfram Research, Inc
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.