Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)

摘要

If we know that x~(1/2) lies in [L,U], can we produce a better bounding interval? The obvious answer is the Secant-Newton map, replacing [L,U] by [L_s,U_s]:[L+x-L~2/L+U,U+x-U~2/2U]. 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 [L_2,U_2]:[L+x-q_L/l_L,U+x-q_u/l_u]. where the q_X are homogeneous quadratics in L,U and the l_X are homogeneous linears. This form is dimensionally consistent. Hence we wish to minimize the Lipschitz constant E:=sup0＜L≤x~(1/2)≤U;L≠U U_2-L_2/U-L subject to various quantified constraints, where the minimum is taken over the coefficients of the q_X and l_X, ten variables in all. For example, the correctness constraint is (∨)_0＜L≤x~(1/2)≤U L, U, x : O＜ L_2 ≤x~(1/2)≤U_2. 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 , and we have 13 (ten coefficients, x,L,U).