Semi-automatic analysis of algorithm complexity (Case study: Square-root computation)

We report on our on-going efforts to apply real quantifier elimination to the (semi-)automatic complexity analysis of 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 √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. In this paper, the complexity analysis amounts to find the smallest maximum number of loop iterations of the algorithm. Hence, the algorithm must be correct, terminating and optimal. It can be formulated as a quantifier elimination problem over real numbers. Hence, in principle, the complexity analysis can be carried out automatically. However, the computational requirement is huge, making the automatic analysis 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 compute semi-automatically the complexity of a class of optimal contracting maps.