Given's Rotation SVD example

Average Error: 13.5 → 13.8

Time: 44.4s

Precision: 64

\[10^{-150} \lt \left|x\right| \lt 10^{+150}\]

Math

\[\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}\]

↓

\[\sqrt{\frac{0.5 \cdot \left(0.5 \cdot 0.5\right) + \left(\left(0.5 \cdot \left(0.5 \cdot 0.5\right)\right) \cdot \left(\frac{x \cdot x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}} \cdot \frac{1}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}\right)\right) \cdot \frac{x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}}{0.5 \cdot 0.5 - \left(0.5 \cdot \frac{x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}\right) \cdot \left(0.5 - 0.5 \cdot \frac{x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}\right)}}\]

C

double f(double p, double x) {
        double r8494099 = 0.5;
        double r8494100 = 1.0;
        double r8494101 = x;
        double r8494102 = 4.0;
        double r8494103 = p;
        double r8494104 = r8494102 * r8494103;
        double r8494105 = r8494104 * r8494103;
        double r8494106 = r8494101 * r8494101;
        double r8494107 = r8494105 + r8494106;
        double r8494108 = sqrt(r8494107);
        double r8494109 = r8494101 / r8494108;
        double r8494110 = r8494100 + r8494109;
        double r8494111 = r8494099 * r8494110;
        double r8494112 = sqrt(r8494111);
        return r8494112;
}

↓

double f(double p, double x) {
        double r8494113 = 0.5;
        double r8494114 = r8494113 * r8494113;
        double r8494115 = r8494113 * r8494114;
        double r8494116 = x;
        double r8494117 = r8494116 * r8494116;
        double r8494118 = p;
        double r8494119 = 4.0;
        double r8494120 = r8494119 * r8494118;
        double r8494121 = r8494118 * r8494120;
        double r8494122 = r8494117 + r8494121;
        double r8494123 = sqrt(r8494122);
        double r8494124 = r8494117 / r8494123;
        double r8494125 = 1.0;
        double r8494126 = r8494125 / r8494123;
        double r8494127 = r8494124 * r8494126;
        double r8494128 = r8494115 * r8494127;
        double r8494129 = r8494116 / r8494123;
        double r8494130 = r8494128 * r8494129;
        double r8494131 = r8494115 + r8494130;
        double r8494132 = r8494113 * r8494129;
        double r8494133 = r8494113 - r8494132;
        double r8494134 = r8494132 * r8494133;
        double r8494135 = r8494114 - r8494134;
        double r8494136 = r8494131 / r8494135;
        double r8494137 = sqrt(r8494136);
        return r8494137;
}

Error

Bits error versus p

Bits error versus x

Target

Original	13.5
Target	13.5
Herbie	13.8

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

Derivation

1. Initial program 13.5

   \[\sqrt{0.5 \cdot \left(1 + \frac{x}{\sqrt{\left(4 \cdot p\right) \cdot p + x \cdot x}}\right)}\]

2. Simplified 13.5

   \[\leadsto \color{blue}{\sqrt{\frac{x}{\frac{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}{0.5}} + 0.5}}\]
3. Using strategy rm

4. Applied flip3-+ 13.5

   \[\leadsto \sqrt{\color{blue}{\frac{{\left(\frac{x}{\frac{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}{0.5}}\right)}^{3} + {0.5}^{3}}{\frac{x}{\frac{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}{0.5}} \cdot \frac{x}{\frac{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}{0.5}} + \left(0.5 \cdot 0.5 - \frac{x}{\frac{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}{0.5}} \cdot 0.5\right)}}}\]

5. Simplified 13.4

   \[\leadsto \sqrt{\frac{\color{blue}{0.5 \cdot \left(0.5 \cdot 0.5\right) + \left(\left(0.5 \cdot \left(0.5 \cdot 0.5\right)\right) \cdot \frac{x \cdot x}{x \cdot x + \left(p \cdot 4\right) \cdot p}\right) \cdot \frac{x}{\sqrt{x \cdot x + \left(p \cdot 4\right) \cdot p}}}}{\frac{x}{\frac{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}{0.5}} \cdot \frac{x}{\frac{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}{0.5}} + \left(0.5 \cdot 0.5 - \frac{x}{\frac{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}{0.5}} \cdot 0.5\right)}}\]

6. Simplified 13.4

   \[\leadsto \sqrt{\frac{0.5 \cdot \left(0.5 \cdot 0.5\right) + \left(\left(0.5 \cdot \left(0.5 \cdot 0.5\right)\right) \cdot \frac{x \cdot x}{x \cdot x + \left(p \cdot 4\right) \cdot p}\right) \cdot \frac{x}{\sqrt{x \cdot x + \left(p \cdot 4\right) \cdot p}}}{\color{blue}{0.5 \cdot 0.5 - \left(0.5 \cdot \frac{x}{\sqrt{x \cdot x + \left(p \cdot 4\right) \cdot p}}\right) \cdot \left(0.5 - 0.5 \cdot \frac{x}{\sqrt{x \cdot x + \left(p \cdot 4\right) \cdot p}}\right)}}}\]
7. Using strategy rm

8. Applied associate-/l* 13.6

   \[\leadsto \sqrt{\frac{0.5 \cdot \left(0.5 \cdot 0.5\right) + \left(\left(0.5 \cdot \left(0.5 \cdot 0.5\right)\right) \cdot \color{blue}{\frac{x}{\frac{x \cdot x + \left(p \cdot 4\right) \cdot p}{x}}}\right) \cdot \frac{x}{\sqrt{x \cdot x + \left(p \cdot 4\right) \cdot p}}}{0.5 \cdot 0.5 - \left(0.5 \cdot \frac{x}{\sqrt{x \cdot x + \left(p \cdot 4\right) \cdot p}}\right) \cdot \left(0.5 - 0.5 \cdot \frac{x}{\sqrt{x \cdot x + \left(p \cdot 4\right) \cdot p}}\right)}}\]
9. Using strategy rm

10. Applied *-un-lft-identity 13.6

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

11. Applied add-sqr-sqrt 13.6

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

12. Applied times-frac 13.5

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

13. Applied *-un-lft-identity 13.5

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

14. Applied times-frac 13.7

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

15. Simplified 13.7

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

16. Simplified 13.8

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

17. Final simplification 13.8

    \[\leadsto \sqrt{\frac{0.5 \cdot \left(0.5 \cdot 0.5\right) + \left(\left(0.5 \cdot \left(0.5 \cdot 0.5\right)\right) \cdot \left(\frac{x \cdot x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}} \cdot \frac{1}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}\right)\right) \cdot \frac{x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}}{0.5 \cdot 0.5 - \left(0.5 \cdot \frac{x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}\right) \cdot \left(0.5 - 0.5 \cdot \frac{x}{\sqrt{x \cdot x + p \cdot \left(4 \cdot p\right)}}\right)}}\]

Reproduce

herbie shell --seed 2019164 
(FPCore (p x)
  :name "Given's Rotation SVD example"
  :pre (< 1e-150 (fabs x) 1e+150)

  :herbie-target
  (sqrt (+ 1/2 (/ (copysign 1/2 x) (hypot 1 (/ (* 2 p) x)))))

  (sqrt (* 0.5 (+ 1 (/ x (sqrt (+ (* (* 4 p) p) (* x x))))))))