7  IEEE-Compliant Square Root

Most of the results listed in Chapters 1, 4, and 6 are propositions pertaining to real variables, which are formalized by ACL2 events in which these variables are restricted to the rational domain. Many of the lemmas of this chapter similarly apply to arbitrary real numbers, but in light of its focus, these results are formulated to correspond more closely with their formal versions. Apart from the informal discussion below, the lemmas themselves contain no references to the real numbers or the square root function.

Establishing IEEE compliance of a floating-point square root module entails proving that the final value $ r$ computed for a given radicand $ x$, rounding mode $ {\cal R}$, and precision $ n$ satisfies

$\displaystyle r = {\cal R}(\sqrt{x}, n).$ (7.1)

We would like to formulate a proposition of rational arithmetic that is transparently equivalent to (7.1). This requirement is satisfied by the following criterion: For all positive rational numbers $ \ell$ and $ h$,

$\displaystyle \ell^2 \leq x \leq h^2 \Rightarrow {\cal R}(\ell, n) \leq r \leq {\cal R}(h, n).$ (7.2)

Obviously, the monotonicity of rounding (Lemma 6.5.11) ensures that (7.1) implies (7.2). On the other hand, suppose that (7.2) holds. According to Lemma 6.5.16, either $ \sqrt{x}$ is $ (n+1)$-exact (and, in particular, rational) or for some $ \epsilon > 0$, $ {\cal R}(y, n) = {\cal R}(\sqrt{x}, n)$ for all $ y$ satisfying $ \vert y - \sqrt{x}\vert < \epsilon$. In either case, there exist $ \ell \in \mathbb{Q}$ and $ h \in \mathbb{Q}$ such that $ \ell \leq \sqrt{x} \leq h$ and $ {\cal R}(\ell, n) = {\cal R}(\sqrt{x}, n) = {\cal R}(h, n)$. Since $ \ell^2 \leq x \leq h^2$,

$\displaystyle {\cal R}(\sqrt{x}, n) = {\cal R}(\ell, n) \leq r \leq {\cal R}(h, n) = {\cal R}(\sqrt{x}, n)

and hence $ r = {\cal R}(\sqrt{x}, n)$.

We would also like to prove formally that (7.2) is satisfied by the value $ r$ computed by any module of interest. For this purpose, it will be useful to have a function that computes, for given $ x$ and $ n$, a rational number $ q$ that satisfies

$\displaystyle {\cal R}(q, n) = {\cal R}(\sqrt{x}, n).$ (7.3)

We shall define a conceptually simple (albeit computationally horrendous) rational function qsqrt that serves this need. The definition is motivated by Lemma 6.5.17, which guarantees that if

$\displaystyle \mathit{qsqrt}(x, k) = \mathit{RTO}(\sqrt{x}, k),$ (7.4)

where $ k \geq n+2$, then (7.3) holds for $ q = \mathit{qsqrt}(x, k)$. Of course, (7.4) will not be our formal definition of qsqrt, nor shall we prove any instance of (7.3). However, our definition will be motivated by this observation, and we shall prove the following (Lemma 7.3.5):

If $ k \geq n+2$, then for all positive rationals $ \ell$ and $ h$ and positive integers $ k$ and $ n$,

$\displaystyle \ell^2 \leq x \leq h^2$    and $\displaystyle k \geq n+2\Rightarrow {\cal R}(\ell, n) \leq {\cal R}(\mathit{qsqrt}(x, k)) \leq {\cal R}(h, n).$ (7.5)

Thus, in order to prove that a computed value $ r$ satisfies (7.2), it suffices to show that $ r = \mathit{qsqrt}(x, k))$ for some $ k \geq n+2$.

Among various other properties of qsqrt that are derived in this chapter is one that warrants some motivation. In practice, a typical implementation of a subtractive square root algorithm produces a final truncated approximation $ q$ of $ \sqrt{x}$ and a remainder that provides a comparison between $ q^2$ and $ x$. A final rounded result $ r$ is derived from this approximation in accordance with a given rounding mode $ {\cal R}$ and precision $ n$. In order to apply (7.5), we would like to show that $ r = {\cal R}(\mathit{qsqrt}(x,k)$ for some appropriate $ k$. This may be done by invoking Lemma 6.5.20 with $ q$ and $ \mathit{qsqrt}(x,k)$ substituted for $ x$ and $ z$, respectively. But this requires showing that $ q = \mathit{RTZ}(\mathit{qsqrt}(x,k))$ and determining whether $ q = \mathit{qsqrt}(x, k)$. Thus, we require a means of converting inequalities relating $ q^2$ and $ x$ to inequalities relating $ q$ and $ \mathit{qsqrt}(x,k)$. This is achieved by the following result (Lemma 7.3.6):

If $ x$ and $ q$ are positive rationals and $ q$ is $ (n-1)$-exact, then

$\displaystyle q^2 < x \Leftrightarrow q < \mathit{qsqrt}(x, n)


$\displaystyle q^2 > x \Leftrightarrow q > \mathit{qsqrt}(x, n).

David Russinoff 2017-08-01