Computing Reviews

Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)
Eraşcu M., Hong H. Journal of Symbolic Computation75(C):110-126,2016.Type:Article
Date Reviewed: 07/25/16

If we know that lies in [L,U], can we produce a better bounding interval? The obvious answer is the Secant-Newton map, replacing [L,U] by

This is guaranteed to halve the interval (and generally does better). Is there a better algorithm?

The authors, not unnaturally, restrict their search to algorithms of the form

where the qX are homogeneous quadratics in L,U and the lX are homogeneous linears. This form is dimensionally consistent. Hence we wish to minimize the Lipschitz constant

subject to various quantified constraints, where the minimum is taken over the coefficients of the qX and lX, ten variables in all. For example, the correctness constraint is In principle this is a problem over the theory of real closed fields, and soluble since [1,4]. In practice, such methods as are implemented are doubly exponential in the number of variables [2], and we have 13 (ten coefficients, x,L,U).

The bulk of this paper is devoted to showing how the authors solve this problem by carefully dividing the formula, judiciously instantiating some of the quantified variables, imposing an additional constraint K on the coefficients of the lX, and then solving the resulting simpler problems with Mathematica and/or QEPCAD-B. The detailed proofs take 8.5 pages, excluding the Mathematica and QEPCAD logs, which are provided on a website.

Having done this, they prove that the best you can do is guarantee to quarter the interval, and they prove that this is achieved:

This result is surprising, as the authors had previously proved [3] that the Secant-Newton map was optimal among contracting maps, that is, those with . In fact, their map is only left contracting; that is, we have LL* but not necessarily U*U. This may well, as the authors speculate, explain why this new map has not been previously discovered. In fact, Ls=L* and the difference in the upper bounds can be more clearly seen in the formulation

which also shows that the two iterations have the same cost.

It is easy to argue that the Lipschitz constant only captures the worst-case behavior. What happens in typical cases? The authors have indeed considered this question, and their figure 2 shows that the new formula typically requires half as many iterations as the Secant-Newton map. They conjecture that the new map is always better, but this is left as an open problem, as is the question of whether one can do without the constraint K.


1)

Collins, G. E. Quantifier elimination for real closed fields by cylindrical algebraicdecomposition. In Automata theory and formal languages (LNCS 33). Springer, 1975, 134–183.


2)

Tarski, A. A decision method for elementary algebra and geometry (2nd ed.). University of California Press, Berkeley, CA, 1951.


3)

Davenport, J. H.; Heintz, J. Real quantifier elimination is doubly exponential. Journal of Symbolic Computation 5, (1988), 29–35.


4)

Erascu, M.; Hong, H. The Secant-Newton map is optimal among contracting quadratic maps forsquare root computation. Journal of Reliable Computing 18, (2013), 73–81.

Reviewer:  J. H. Davenport Review #: CR144626 (1611-0832)

Reproduction in whole or in part without permission is prohibited.   Copyright 2024 ComputingReviews.com™
Terms of Use
| Privacy Policy