Given's Rotation SVD example, simplified

Average Error: 15.6 → 15.2

Time: 1.3m

Precision: 64

Math

\[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]

↓

\[\sqrt{\frac{1 \cdot \left(1 \cdot 1\right) - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)}{\mathsf{fma}\left(1, 1, \mathsf{fma}\left(1, \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)}} \cdot \sqrt{\frac{1 \cdot \left(1 \cdot 1\right) - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)}{\mathsf{fma}\left(1, 1, \mathsf{fma}\left(1, \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)}}\]

C

double f(double x) {
        double r11917391 = 1.0;
        double r11917392 = 0.5;
        double r11917393 = x;
        double r11917394 = hypot(r11917391, r11917393);
        double r11917395 = r11917391 / r11917394;
        double r11917396 = r11917391 + r11917395;
        double r11917397 = r11917392 * r11917396;
        double r11917398 = sqrt(r11917397);
        double r11917399 = r11917391 - r11917398;
        return r11917399;
}

↓

double f(double x) {
        double r11917400 = 1.0;
        double r11917401 = r11917400 * r11917400;
        double r11917402 = r11917400 * r11917401;
        double r11917403 = 0.5;
        double r11917404 = x;
        double r11917405 = hypot(r11917400, r11917404);
        double r11917406 = r11917400 / r11917405;
        double r11917407 = r11917400 + r11917406;
        double r11917408 = r11917403 * r11917407;
        double r11917409 = sqrt(r11917408);
        double r11917410 = r11917409 * r11917408;
        double r11917411 = r11917402 - r11917410;
        double r11917412 = fma(r11917400, r11917409, r11917408);
        double r11917413 = fma(r11917400, r11917400, r11917412);
        double r11917414 = r11917411 / r11917413;
        double r11917415 = sqrt(r11917414);
        double r11917416 = r11917415 * r11917415;
        return r11917416;
}

Error

Bits error versus x

Derivation

1. Initial program 15.6

   \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
2. Using strategy rm

3. Applied flip3-- 15.9

   \[\leadsto \color{blue}{\frac{{1}^{3} - {\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}{1 \cdot 1 + \left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1 \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}}\]

4. Simplified 15.6

   \[\leadsto \frac{\color{blue}{1 \cdot \left(1 \cdot 1\right) - \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}{1 \cdot 1 + \left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1 \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}\]

5. Simplified 15.2

   \[\leadsto \frac{1 \cdot \left(1 \cdot 1\right) - \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}{\color{blue}{\mathsf{fma}\left(1, 1, \mathsf{fma}\left(1, \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)}}\]
6. Using strategy rm

7. Applied add-sqr-sqrt 15.2

   \[\leadsto \color{blue}{\sqrt{\frac{1 \cdot \left(1 \cdot 1\right) - \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}{\mathsf{fma}\left(1, 1, \mathsf{fma}\left(1, \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)}} \cdot \sqrt{\frac{1 \cdot \left(1 \cdot 1\right) - \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}{\mathsf{fma}\left(1, 1, \mathsf{fma}\left(1, \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)}}}\]

8. Final simplification 15.2

   \[\leadsto \sqrt{\frac{1 \cdot \left(1 \cdot 1\right) - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)}{\mathsf{fma}\left(1, 1, \mathsf{fma}\left(1, \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)}} \cdot \sqrt{\frac{1 \cdot \left(1 \cdot 1\right) - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)}{\mathsf{fma}\left(1, 1, \mathsf{fma}\left(1, \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)}}\]

Reproduce

herbie shell --seed 2019172 +o rules:numerics
(FPCore (x)
  :name "Given's Rotation SVD example, simplified"
  (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))