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

详细信息    查看全文

• 作者：Mădălina Eraşcu^a ; ^{merascu@info.uvt.ro" class="auth_mail" title="E-mail the corresponding author} ; Hoon Hong^b ; ^{hong@ncsu.edu" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Synthesis ; Optimal quadratically convergent algorithm ; Square root ; Real quantifier elimination
• 刊名：Journal of Symbolic Computation
• 出版年：2016
• 出版时间：July-August 2016
• 年：2016
• 卷：75
• 期：Complete
• 页码：110-126
• 全文大小：382 K

文摘

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 ε  , find a real interval such that it contains class="mathmlsrc">title="View the MathML source" class="mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S0747717115001091&_mathId=si1.gif&_user=111111111&_pii=S0747717115001091&_rdoc=1&_issn=07477171&md5=20e503933310ad8016ec8779d4ff5bb6">class="imgLazyJSB inlineImage" height="15" width="21" alt="View the MathML source" style="margin-top: -5px; vertical-align: middle" title="View the MathML source" src="/sd/grey_pxl.gif" data-inlimgeid="1-s2.0-S0747717115001091-si1.gif">class="mathContainer hidden">class="mathCode">$\sqrt{x}$ 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 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.