Using Real Quantifer Elimination for Synthesizing Optimal Numerical Algorithms
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. We will also present how our approach can be used to syntesize optimal numerical algorithms for other important functions which occur in hardware implementation, e.g. reciprocal (multiplicative inverse), reciprocal square root. The work is partly joined with Hoon Hong, NCSU, Raleigh, USA.