Given's Rotation SVD example, simplified

Average Error: 15.0 → 0.2

Time: 12.7s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -8.76499040491705134 \cdot 10^{-4}:\\ \;\;\;\;\frac{1 \cdot 1 - \left(1 + \frac{\sqrt{1}}{\sqrt[3]{\mathsf{hypot}\left(1, x\right)} \cdot \sqrt[3]{\mathsf{hypot}\left(1, x\right)}} \cdot \frac{\sqrt{1}}{\sqrt[3]{\mathsf{hypot}\left(1, x\right)}}\right) \cdot 0.5}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}\\ \mathbf{elif}\;x \le 0.00176534550686875788:\\ \;\;\;\;\frac{\mathsf{fma}\left(0.25, \frac{{x}^{2}}{{\left(\sqrt{1}\right)}^{3}}, 0.5 - \mathsf{fma}\left(\frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5}}, 0.1875, \frac{0.5}{\sqrt{1}}\right)\right)}{1 + \sqrt[3]{{\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{{1}^{6} - {\left(\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right)}^{3}}{\mathsf{fma}\left(\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5, \mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right), {1}^{4}\right)}}{1 + \sqrt[3]{{\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}}\\ \end{array}\]

C

double f(double x) {
        double r225268 = 1.0;
        double r225269 = 0.5;
        double r225270 = x;
        double r225271 = hypot(r225268, r225270);
        double r225272 = r225268 / r225271;
        double r225273 = r225268 + r225272;
        double r225274 = r225269 * r225273;
        double r225275 = sqrt(r225274);
        double r225276 = r225268 - r225275;
        return r225276;
}

↓

double f(double x) {
        double r225277 = x;
        double r225278 = -0.0008764990404917051;
        bool r225279 = r225277 <= r225278;
        double r225280 = 1.0;
        double r225281 = r225280 * r225280;
        double r225282 = sqrt(r225280);
        double r225283 = hypot(r225280, r225277);
        double r225284 = cbrt(r225283);
        double r225285 = r225284 * r225284;
        double r225286 = r225282 / r225285;
        double r225287 = r225282 / r225284;
        double r225288 = r225286 * r225287;
        double r225289 = r225280 + r225288;
        double r225290 = 0.5;
        double r225291 = r225289 * r225290;
        double r225292 = r225281 - r225291;
        double r225293 = r225280 / r225283;
        double r225294 = r225280 + r225293;
        double r225295 = r225290 * r225294;
        double r225296 = sqrt(r225295);
        double r225297 = r225280 + r225296;
        double r225298 = r225292 / r225297;
        double r225299 = 0.0017653455068687579;
        bool r225300 = r225277 <= r225299;
        double r225301 = 0.25;
        double r225302 = 2.0;
        double r225303 = pow(r225277, r225302);
        double r225304 = 3.0;
        double r225305 = pow(r225282, r225304);
        double r225306 = r225303 / r225305;
        double r225307 = 4.0;
        double r225308 = pow(r225277, r225307);
        double r225309 = 5.0;
        double r225310 = pow(r225282, r225309);
        double r225311 = r225308 / r225310;
        double r225312 = 0.1875;
        double r225313 = r225290 / r225282;
        double r225314 = fma(r225311, r225312, r225313);
        double r225315 = r225290 - r225314;
        double r225316 = fma(r225301, r225306, r225315);
        double r225317 = pow(r225296, r225304);
        double r225318 = cbrt(r225317);
        double r225319 = r225280 + r225318;
        double r225320 = r225316 / r225319;
        double r225321 = 6.0;
        double r225322 = pow(r225280, r225321);
        double r225323 = r225294 * r225290;
        double r225324 = pow(r225323, r225304);
        double r225325 = r225322 - r225324;
        double r225326 = fma(r225280, r225280, r225295);
        double r225327 = pow(r225280, r225307);
        double r225328 = fma(r225323, r225326, r225327);
        double r225329 = r225325 / r225328;
        double r225330 = r225329 / r225319;
        double r225331 = r225300 ? r225320 : r225330;
        double r225332 = r225279 ? r225298 : r225331;
        return r225332;
}

Error

Bits error versus x

Derivation

1. Split input into 3 regimes

2. if x < -0.0008764990404917051

   1. Initial program 1.1

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

   3. Applied flip-- 1.1

      \[\leadsto \color{blue}{\frac{1 \cdot 1 - \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 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}\]

   4. Simplified 0.1

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

   6. Applied add-cube-cbrt 0.2

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

   7. Applied add-sqr-sqrt 0.2

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

   8. Applied times-frac 0.1

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

   if -0.0008764990404917051 < x < 0.0017653455068687579

   1. Initial program 29.3

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

   3. Applied flip-- 29.3

      \[\leadsto \color{blue}{\frac{1 \cdot 1 - \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 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}\]

   4. Simplified 29.3

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

   6. Applied add-cbrt-cube 29.3

      \[\leadsto \frac{1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}{1 + \color{blue}{\sqrt[3]{\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)}\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}}\]

   7. Simplified 29.3

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

   8. Taylor expanded around 0 29.3

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

   9. Simplified 0.3

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

   if 0.0017653455068687579 < x

   1. Initial program 1.0

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

   3. Applied flip-- 1.0

      \[\leadsto \color{blue}{\frac{1 \cdot 1 - \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 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}\]

   4. Simplified 0.1

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

   6. Applied add-cbrt-cube 0.1

      \[\leadsto \frac{1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}{1 + \color{blue}{\sqrt[3]{\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)}\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}}\]

   7. Simplified 0.1

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

   9. Applied flip3-- 0.1

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

   10. Simplified 0.1

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

   11. Simplified 0.1

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

4. Final simplification 0.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le -8.76499040491705134 \cdot 10^{-4}:\\ \;\;\;\;\frac{1 \cdot 1 - \left(1 + \frac{\sqrt{1}}{\sqrt[3]{\mathsf{hypot}\left(1, x\right)} \cdot \sqrt[3]{\mathsf{hypot}\left(1, x\right)}} \cdot \frac{\sqrt{1}}{\sqrt[3]{\mathsf{hypot}\left(1, x\right)}}\right) \cdot 0.5}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}\\ \mathbf{elif}\;x \le 0.00176534550686875788:\\ \;\;\;\;\frac{\mathsf{fma}\left(0.25, \frac{{x}^{2}}{{\left(\sqrt{1}\right)}^{3}}, 0.5 - \mathsf{fma}\left(\frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5}}, 0.1875, \frac{0.5}{\sqrt{1}}\right)\right)}{1 + \sqrt[3]{{\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{{1}^{6} - {\left(\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right)}^{3}}{\mathsf{fma}\left(\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5, \mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right), {1}^{4}\right)}}{1 + \sqrt[3]{{\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}}\\ \end{array}\]

Reproduce

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