Given's Rotation SVD example, simplified

Average Error: 15.5 → 0.0

Time: 1.6m

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}\;x \le -0.01161705812947232:\\ \;\;\;\;\frac{\mathsf{fma}\left(1, \frac{1}{8}, \left(\frac{\sqrt{\frac{1}{8}}}{\mathsf{hypot}\left(1, x\right) \cdot \mathsf{hypot}\left(1, x\right)} \cdot \left(-\frac{\sqrt{\frac{1}{8}}}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)}{\sqrt{1 + \sqrt{\frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)} + \frac{1}{2}}} \cdot \left(\left(\frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)} \cdot \frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)} \cdot \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) + \frac{1}{4}\right)} \cdot \frac{1}{\sqrt{1 + \sqrt{\frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)} + \frac{1}{2}}}}\\ \mathbf{elif}\;x \le 0.01069117617427654:\\ \;\;\;\;\mathsf{fma}\left(\left(x \cdot x\right), \left(\mathsf{fma}\left(\frac{69}{1024}, \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right), \frac{1}{8}\right)\right), \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \frac{-11}{128}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{fma}\left(1, \frac{1}{8}, \left(\frac{\sqrt{\frac{1}{8}}}{\mathsf{hypot}\left(1, x\right) \cdot \mathsf{hypot}\left(1, x\right)} \cdot \left(-\frac{\sqrt{\frac{1}{8}}}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)}{\sqrt{1 + \sqrt{\frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)} + \frac{1}{2}}} \cdot \left(\left(\frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)} \cdot \frac{1}{2} + \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)} \cdot \frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)}\right) + \frac{1}{4}\right)} \cdot \frac{1}{\sqrt{1 + \sqrt{\frac{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)} + \frac{1}{2}}}}\\ \end{array}\]

C

double f(double x) {
        double r41626579 = 1.0;
        double r41626580 = 0.5;
        double r41626581 = x;
        double r41626582 = hypot(r41626579, r41626581);
        double r41626583 = r41626579 / r41626582;
        double r41626584 = r41626579 + r41626583;
        double r41626585 = r41626580 * r41626584;
        double r41626586 = sqrt(r41626585);
        double r41626587 = r41626579 - r41626586;
        return r41626587;
}

↓

double f(double x) {
        double r41626588 = x;
        double r41626589 = -0.01161705812947232;
        bool r41626590 = r41626588 <= r41626589;
        double r41626591 = 1.0;
        double r41626592 = 0.125;
        double r41626593 = sqrt(r41626592);
        double r41626594 = hypot(r41626591, r41626588);
        double r41626595 = r41626594 * r41626594;
        double r41626596 = r41626593 / r41626595;
        double r41626597 = r41626593 / r41626594;
        double r41626598 = -r41626597;
        double r41626599 = r41626596 * r41626598;
        double r41626600 = fma(r41626591, r41626592, r41626599);
        double r41626601 = 0.5;
        double r41626602 = r41626601 / r41626594;
        double r41626603 = r41626602 + r41626601;
        double r41626604 = sqrt(r41626603);
        double r41626605 = r41626591 + r41626604;
        double r41626606 = sqrt(r41626605);
        double r41626607 = r41626602 * r41626601;
        double r41626608 = r41626602 * r41626602;
        double r41626609 = r41626607 + r41626608;
        double r41626610 = 0.25;
        double r41626611 = r41626609 + r41626610;
        double r41626612 = r41626606 * r41626611;
        double r41626613 = r41626600 / r41626612;
        double r41626614 = r41626591 / r41626606;
        double r41626615 = r41626613 * r41626614;
        double r41626616 = 0.01069117617427654;
        bool r41626617 = r41626588 <= r41626616;
        double r41626618 = r41626588 * r41626588;
        double r41626619 = 0.0673828125;
        double r41626620 = r41626618 * r41626618;
        double r41626621 = fma(r41626619, r41626620, r41626592);
        double r41626622 = -0.0859375;
        double r41626623 = r41626620 * r41626622;
        double r41626624 = fma(r41626618, r41626621, r41626623);
        double r41626625 = r41626617 ? r41626624 : r41626615;
        double r41626626 = r41626590 ? r41626615 : r41626625;
        return r41626626;
}

Error

Bits error versus x

Derivation

1. Split input into 2 regimes

2. if x < -0.01161705812947232 or 0.01069117617427654 < 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{\frac{1}{2}}{\mathsf{hypot}\left(1, x\right)} + \frac{1}{2}}}\]
   3. Using strategy rm

   4. Applied flip-- 1.0

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

   6. Applied add-sqr-sqrt 1.6

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

   7. Applied *-un-lft-identity 1.6

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

   8. Applied times-frac 1.0

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

   9. Simplified 0.1

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

   11. Applied flip3-- 0.1

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

   12. Applied associate-/l/ 0.1

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

   13. Simplified 0.1

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

   15. Applied add-sqr-sqrt 0.1

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

   16. Applied times-frac 0.1

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

   17. Applied *-un-lft-identity 0.1

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

   18. Applied prod-diff 0.1

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

   19. Simplified 0.1

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

   if -0.01161705812947232 < x < 0.01069117617427654

   1. Initial program 30.6

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

   2. Simplified 30.6

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

   3. 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}}\]

   4. Simplified 0.0

      \[\leadsto \color{blue}{\mathsf{fma}\left(\left(x \cdot x\right), \left(\mathsf{fma}\left(\frac{69}{1024}, \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right), \frac{1}{8}\right)\right), \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \frac{-11}{128}\right)\right)}\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.0

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

Reproduce

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