Given's Rotation SVD example, simplified

Average Error: 15.1 → 0.4

Time: 13.8s

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.847354589138370990937521032293489042786 \cdot 10^{-5}:\\ \;\;\;\;\frac{\frac{\log \left(e^{1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}\right)}{\sqrt{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}}{\sqrt{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}\\ \mathbf{elif}\;x \le 0.00196705341402985496232491691159793845145:\\ \;\;\;\;\frac{\frac{\mathsf{fma}\left(\frac{{x}^{2}}{{\left(\sqrt{1}\right)}^{3}}, 0.25, 0.5 - \mathsf{fma}\left(0.1875, \frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5}}, \frac{0.5}{\sqrt{1}}\right)\right)}{\sqrt{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}}{\sqrt{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}{\sqrt{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}}{\sqrt{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}\\ \end{array}\]

C

double f(double x) {
        double r261459 = 1.0;
        double r261460 = 0.5;
        double r261461 = x;
        double r261462 = hypot(r261459, r261461);
        double r261463 = r261459 / r261462;
        double r261464 = r261459 + r261463;
        double r261465 = r261460 * r261464;
        double r261466 = sqrt(r261465);
        double r261467 = r261459 - r261466;
        return r261467;
}

↓

double f(double x) {
        double r261468 = x;
        double r261469 = -8.847354589138371e-05;
        bool r261470 = r261468 <= r261469;
        double r261471 = 1.0;
        double r261472 = r261471 * r261471;
        double r261473 = hypot(r261471, r261468);
        double r261474 = r261471 / r261473;
        double r261475 = r261471 + r261474;
        double r261476 = 0.5;
        double r261477 = r261475 * r261476;
        double r261478 = r261472 - r261477;
        double r261479 = exp(r261478);
        double r261480 = log(r261479);
        double r261481 = r261476 * r261475;
        double r261482 = sqrt(r261481);
        double r261483 = r261471 + r261482;
        double r261484 = sqrt(r261483);
        double r261485 = r261480 / r261484;
        double r261486 = r261485 / r261484;
        double r261487 = 0.001967053414029855;
        bool r261488 = r261468 <= r261487;
        double r261489 = 2.0;
        double r261490 = pow(r261468, r261489);
        double r261491 = sqrt(r261471);
        double r261492 = 3.0;
        double r261493 = pow(r261491, r261492);
        double r261494 = r261490 / r261493;
        double r261495 = 0.25;
        double r261496 = 0.1875;
        double r261497 = 4.0;
        double r261498 = pow(r261468, r261497);
        double r261499 = 5.0;
        double r261500 = pow(r261491, r261499);
        double r261501 = r261498 / r261500;
        double r261502 = r261476 / r261491;
        double r261503 = fma(r261496, r261501, r261502);
        double r261504 = r261476 - r261503;
        double r261505 = fma(r261494, r261495, r261504);
        double r261506 = r261505 / r261484;
        double r261507 = r261506 / r261484;
        double r261508 = r261478 / r261484;
        double r261509 = r261508 / r261484;
        double r261510 = r261488 ? r261507 : r261509;
        double r261511 = r261470 ? r261486 : r261510;
        return r261511;
}

Error

Bits error versus x

Derivation

1. Split input into 3 regimes

2. if x < -8.847354589138371e-05

   1. Initial program 1.2

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

   3. Applied flip-- 1.2

      \[\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.2

      \[\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-sqr-sqrt 1.2

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

   7. Applied associate-/r* 0.2

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

   9. Applied add-log-exp 0.2

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

   10. Applied add-log-exp 0.2

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

   11. Applied diff-log 1.7

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

   12. Simplified 0.2

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

   if -8.847354589138371e-05 < x < 0.001967053414029855

   1. Initial program 28.9

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

   3. Applied flip-- 28.9

      \[\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 28.9

      \[\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-sqr-sqrt 28.9

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

   7. Applied associate-/r* 28.9

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

   9. Applied add-log-exp 28.9

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

   10. Applied add-log-exp 28.9

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

   11. Applied diff-log 28.9

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

   12. Simplified 28.9

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

   13. Taylor expanded around 0 28.9

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

   14. Simplified 0.6

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

   if 0.001967053414029855 < 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-sqr-sqrt 1.0

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

   7. Applied associate-/r* 0.1

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

4. Final simplification 0.4

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

Reproduce

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