Given's Rotation SVD example, simplified

Average Error: 15.2 → 0.0

Time: 28.8s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\mathsf{hypot}\left(1, x\right) \le 1.000024004203487:\\ \;\;\;\;\mathsf{fma}\left(\frac{69}{1024}, \left(\left(x \cdot x\right) \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot x\right), \mathsf{fma}\left(x \cdot x, \frac{1}{8}, \frac{-11}{128} \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1 - \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}} \cdot \left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}{\mathsf{fma}\left(\sqrt{\sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}} + 1}, \sqrt{\sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}} + 1}, \frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}\\ \end{array}\]

C

double f(double x) {
        double r5794336 = 1.0;
        double r5794337 = 0.5;
        double r5794338 = x;
        double r5794339 = hypot(r5794336, r5794338);
        double r5794340 = r5794336 / r5794339;
        double r5794341 = r5794336 + r5794340;
        double r5794342 = r5794337 * r5794341;
        double r5794343 = sqrt(r5794342);
        double r5794344 = r5794336 - r5794343;
        return r5794344;
}

↓

double f(double x) {
        double r5794345 = 1.0;
        double r5794346 = x;
        double r5794347 = hypot(r5794345, r5794346);
        double r5794348 = 1.000024004203487;
        bool r5794349 = r5794347 <= r5794348;
        double r5794350 = 0.0673828125;
        double r5794351 = r5794346 * r5794346;
        double r5794352 = r5794351 * r5794346;
        double r5794353 = r5794352 * r5794352;
        double r5794354 = 0.125;
        double r5794355 = -0.0859375;
        double r5794356 = r5794351 * r5794351;
        double r5794357 = r5794355 * r5794356;
        double r5794358 = fma(r5794351, r5794354, r5794357);
        double r5794359 = fma(r5794350, r5794353, r5794358);
        double r5794360 = 0.5;
        double r5794361 = r5794360 / r5794347;
        double r5794362 = r5794360 + r5794361;
        double r5794363 = sqrt(r5794362);
        double r5794364 = r5794363 * r5794362;
        double r5794365 = r5794345 - r5794364;
        double r5794366 = r5794363 + r5794345;
        double r5794367 = sqrt(r5794366);
        double r5794368 = fma(r5794367, r5794367, r5794362);
        double r5794369 = r5794365 / r5794368;
        double r5794370 = r5794349 ? r5794359 : r5794369;
        return r5794370;
}

Error

Bits error versus x

Derivation

1. Split input into 2 regimes

2. if (hypot 1 x) < 1.000024004203487

   1. Initial program 29.7

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

   2. Simplified 29.7

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

   4. Applied flip3-- 29.7

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

   5. Simplified 29.7

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

   6. Simplified 29.7

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

   8. Applied add-cbrt-cube 29.7

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

   9. Applied add-cbrt-cube 29.7

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

   10. Applied cbrt-undiv 29.7

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

   11. Simplified 29.7

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

   12. Taylor expanded around 0 0.0

       \[\leadsto \color{blue}{\left(\frac{1}{8} \cdot {x}^{2} + \frac{69}{1024} \cdot {x}^{6}\right) - \frac{11}{128} \cdot {x}^{4}}\]

   13. Simplified 0.0

       \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{69}{1024}, \left(\left(x \cdot x\right) \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot x\right), \mathsf{fma}\left(x \cdot x, \frac{1}{8}, \frac{-11}{128} \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)}\]

   if 1.000024004203487 < (hypot 1 x)

   1. Initial program 1.0

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

   2. Simplified 1.0

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

   4. Applied flip3-- 1.6

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

   5. Simplified 1.0

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

   6. Simplified 0.1

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

   8. Applied add-sqr-sqrt 1.0

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

   9. Applied fma-def 0.1

      \[\leadsto \frac{1 - \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}} \cdot \left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}{\color{blue}{\mathsf{fma}\left(\sqrt{\sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}} + 1}, \sqrt{\sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}} + 1}, \frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{hypot}\left(1, x\right) \le 1.000024004203487:\\ \;\;\;\;\mathsf{fma}\left(\frac{69}{1024}, \left(\left(x \cdot x\right) \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot x\right), \mathsf{fma}\left(x \cdot x, \frac{1}{8}, \frac{-11}{128} \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1 - \sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}} \cdot \left(\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}{\mathsf{fma}\left(\sqrt{\sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}} + 1}, \sqrt{\sqrt{\frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}} + 1}, \frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right)}\\ \end{array}\]

Reproduce

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