7.3  IEEE-Rounded Square Root

The desired function qsqrt is a simple generalization of rto-sqrt to arbitrary positive rationals:

Definition 7.3.1   (qsqrt) Let $ x \in \mathbb{Q}$ and $ n \in \mathbb{N}$ with $ x>0$ and $ n > 0$. Let $ e = \left\lfloor \frac{\mathit{expo}(x)}{2} \right\rfloor + 1$. then

$\displaystyle \mathit{qsqrt}(x, n) = 2^e\mathit{rto\mbox{-}sqrt}(2^{-2e}x, n).
$

Notation: $ \mathit{qsqrt}(x, n)$ is abbreviated as $ \sqrt[(n)]{x}$.

  (qsqrt-expo) Let $ x \in \mathbb{Q}$, $ x>0$, $ e = \left\lfloor \frac{\mathit{expo}(x)}{2} \right\rfloor + 1$, and $ x' = 2^{-2e}x$. Then $ \frac{1}{4} \leq x' < 1$.

PROOF: Since

$\displaystyle \frac{\mathit{expo}(x)}{2} - 1 < \left\lfloor \frac{\mathit{expo}(x)}{2} \right\rfloor \leq \frac{\mathit{expo}(x)}{2},
$

we have

$\displaystyle \mathit{expo}(x) < 2\left\lfloor \frac{\mathit{expo}(x)}{2} \right\rfloor + 2 = 2e
$

and

$\displaystyle \mathit{expo}(x) \geq 2\left\lfloor \frac{\mathit{expo}(x)}{2} \right\rfloor = 2e-2.
$

By Lemma 4.1.14, $ -2 \leq \mathit{expo}(x') < 0$ and the lemma follows. 

  (qsqrt-rto-sqrt) Let $ x \in \mathbb{Q}$ and $ n \in \mathbb{N}$. If $ x \geq \frac{1}{4}$ and $ n > 0$, then

$\displaystyle \sqrt[(n)]{x} = \mathit{rto\mbox{-}sqrt}(x,n).
$

PROOF: Since $ \mathit{expo}(x) \in \{-2,-1\}$, $ \left\lfloor \frac{\mathit{expo}(x)}{2} \right\rfloor = -1$ and $ e = 0$

  (qsqrt-shift) Let $ x \in \mathbb{Q}$ and $ n \in \mathbb{N}$ with $ x>0$ and $ n > 0$. For all $ k \in \mathbb{N}$,

$\displaystyle \sqrt[(2^{2k})]{x} = 2^k \sqrt[(n)]{x}.
$

PROOF: Let $ x' = 2^{2k}x$ and

$\displaystyle e' = \left\lfloor \frac{\mathit{expo}(x')}{2} + 1
= \right\rfloor \left\lfloor \frac{\mathit{expo}(x)}{2} + k \right\rfloor + 1
= e + k.
$

Then
$\displaystyle \sqrt[(n)]{x}$ $\displaystyle =$ $\displaystyle 2^{e'}\mathit{rto\mbox{-}sqrt}(2^{-2e'}x', n)$  
  $\displaystyle =$ $\displaystyle 2^{e+k}\mathit{rto\mbox{-}sqrt}(2^{-2(e+k)}2^{2k}x, n)$  
  $\displaystyle =$ $\displaystyle 2^{k}\left(2^e\mathit{rto\mbox{-}sqrt}(2^{2e}x, n)\right)$  
  $\displaystyle =$ $\displaystyle 2^k \sqrt[(n)]{x}. $  

  (rnd-qsqrt-equal) Let $ x \in \mathbb{Q}$, $ k \in \mathbb{N}$, $ m_1 \in \mathbb{N}$, and $ n_2 \in \mathbb{N}$ with $ x>0$ and $ 2 < k+2 \leq m \leq n$ and let $ {\cal R}$ be a common rounding mode. Then

$\displaystyle {\cal R}(\sqrt[(m)]{x} = {\cal R}(\sqrt[(n)]{x}).
$

PROOF: Let $ e = \left\lfloor \frac{\mathit{expo}(x)}{2} \right\rfloor + 1$. By Definition 7.3.1 and Lemmas 7.2.5 and 6.4.3,

$\displaystyle {\cal R}(\sqrt[(m)]{x},k)$ $\displaystyle =$ $\displaystyle {\cal R}(2^e\mathit{rto\mbox{-}sqrt}(2^{-2e}x,m),k)$  
  $\displaystyle =$ $\displaystyle 2^e{\cal R}(\mathit{rto\mbox{-}sqrt}(2^{-2e}x,m),k)$  
  $\displaystyle =$ $\displaystyle 2^e{\cal R}(\mathit{rto\mbox{-}sqrt}(2^{-2e}x,n),k)$  
  $\displaystyle =$ $\displaystyle {\cal R}(2^e\mathit{rto\mbox{-}sqrt}(2^{-2e}x,n),k)$  
  $\displaystyle =$ $\displaystyle {\cal R}(\sqrt[(n)]{x},k). $  

The next two lemmas establish the properties of qsqrt discussed at the beginning of this chapter.

  (qsqrt-lower, qsqrt-upper) Let $ x \in \mathbb{Q}$, $ \ell \in \mathbb{Q}$, $ h \in \mathbb{Q}$ $ n \in \mathbb{N}$, and $ k \in \mathbb{N}$. Assume that $ x>0$ $ h>0$, $ n > 0$, $ k \geq n+2$, and $ \ell^2 \leq x \leq h^2$. Let $ {\cal R}$ be a common rounding mode. Then

$\displaystyle {\cal R}(\ell, n) \leq {\cal R}(\sqrt[(k)]{x}, n) \leq {\cal R}(h, n).
$

PROOF: Let Let $ e = \left\lfloor \frac{\mathit{expo}(x)}{2} \right\rfloor + 1$, $ x' = 2^{-2e}x$, $ \ell' = 2^{-e}\ell$, and $ h' = 2^{-e}h$. By Lemmas 7.3.1 and 7.2.5,

$\displaystyle \mathit{rto}(\ell', k) \leq \mathit{rto\mbox{-}sqrt}(x', k) \leq \mathit{rto}(h', k),
$

or

$\displaystyle \mathit{rto}(2^{-k}\ell, k) \leq 2^{-k}\sqrt[(k)]{x} \leq \mathit{rto}(2^{-k}h, k).
$

By Lemma 6.4.3,

$\displaystyle \mathit{rto}(\ell, k) \leq \sqrt[(k)]{x} \leq \mathit{rto}(h, k),
$

and by Lemma 6.5.17,

$\displaystyle {\cal R}(\ell, n) = {\cal R}(\mathit{rto}(\ell, k), n) \leq {\cal R}(\sqrt[(k)]{x}, n)
\leq {\cal R}(\mathit{rto}(h, k), n) = {\cal R}(h, n). $

  (exactp-cmp-qsqrt) Let $ x \in \mathbb{Q}$, $ q \in \mathbb{Q}$, and $ n \in \mathbb{N}$. Assume that $ x>0$, $ q>0$, $ n>1$, and q is $ (n-1$)-exact. Then

(a) $ q^2 < x \Leftrightarrow q < \sqrt[(n)]{x}$;

(b) $ q^2 > x \Leftrightarrow q > \sqrt[(n)]{x}$;

(c) $ q^2 = x \Leftrightarrow q = \sqrt[(n)]{x}$.

PROOF: Let $ e = \left\lfloor \frac{\mathit{expo}(x)}{2} \right\rfloor + 1$, $ x' = 2^{-2e}x$, and $ q' = 2^{-e}q$. Then $ \frac{1}{4} \leq x' < 1$ and $ \sqrt[(n)]{x} = 2^e\mathit{rto\mbox{-}sqrt}(x', n)$. By Lemma 7.2.6,

$\displaystyle q^2 < x$ $\displaystyle \Leftrightarrow$ $\displaystyle q'^2 < x'$  
  $\displaystyle \Leftrightarrow$ $\displaystyle q' < \mathit{rto\mbox{-}sqrt}(x', n)$  
  $\displaystyle \Leftrightarrow$ $\displaystyle 2^{-e}q < 2^{-e}\sqrt[(n)]{x}$  
  $\displaystyle \Leftrightarrow$ $\displaystyle q < \sqrt[(n)]{x}.$  

The proof of (b) is similar, and (c) follows. 


  (qsqrt-sqrt) Let $ x \in \mathbb{Q}$ and $ n \in \mathbb{N}$ with $ x>0$ and $ n>1$. If $ \sqrt[(n)]{x}$ is $ (n-1)$-exact, then $ (\sqrt[(n)]{x})^2 = x$.

PROOF: Instantiate Lemma 7.3.6 with $ q = \sqrt[(n)]{x})$

  (qsqrt-exact-equal) Let $ x \in \mathbb{Q}$, $ k \in \mathbb{N}$, $ n \in \mathbb{N}$, and $ m \in \mathbb{N}$ with $ x>0$, $ k>1$, $ n>k$, and $ m > k$. If $ \sqrt[(n)]{x}$ is $ (n-1)$-exact, then $ \sqrt[(m)]{x} = \sqrt[(n)]{x}$.

PROOF: By Corollary 7.3.7, $ (\sqrt[(n)]{x})^2 = x$. The corollary again follows from Lemma 7.3.6


Lemma 7.3.6 is also critical in the detection of floating-point precision exceptions. As described more fully in Sections 8.4, 9.5, and 10.3, this exception is signaled when an instruction returns a rounded result $ r$ that differs from the precise mathematical value $ u$ of an operation. But in the case of the square root, the ACL2 formalization compares $ r$ to $ \sqrt[(p+2)]{x}$ rather than $ u = \sqrt{x}$, where $ p$ is the target precision. This is justified by (c) above, from which it follows that $ r = \sqrt{x}$ iff $ r = \sqrt[(p+2)]{x}$.

David Russinoff 2017-08-01