Given's Rotation SVD example, simplified

Average Error: 15.2 → 0.2

Time: 24.7s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -0.002686087558037088089679667035625243443064:\\ \;\;\;\;\frac{\frac{{1}^{4} - \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|}{\mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)}}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}\\ \mathbf{elif}\;x \le 0.00280973890453212237286462205076986720087:\\ \;\;\;\;\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)}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\log \left(e^{{1}^{4} - {\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{4}}\right)}{\mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)}}{\mathsf{expm1}\left(\mathsf{log1p}\left(1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)\right)}\\ \end{array}\]

C

double f(double x) {
        double r151998 = 1.0;
        double r151999 = 0.5;
        double r152000 = x;
        double r152001 = hypot(r151998, r152000);
        double r152002 = r151998 / r152001;
        double r152003 = r151998 + r152002;
        double r152004 = r151999 * r152003;
        double r152005 = sqrt(r152004);
        double r152006 = r151998 - r152005;
        return r152006;
}

↓

double f(double x) {
        double r152007 = x;
        double r152008 = -0.002686087558037088;
        bool r152009 = r152007 <= r152008;
        double r152010 = 1.0;
        double r152011 = 4.0;
        double r152012 = pow(r152010, r152011);
        double r152013 = hypot(r152010, r152007);
        double r152014 = r152010 / r152013;
        double r152015 = r152010 + r152014;
        double r152016 = 0.5;
        double r152017 = r152015 * r152016;
        double r152018 = fabs(r152017);
        double r152019 = r152018 * r152018;
        double r152020 = r152012 - r152019;
        double r152021 = r152016 * r152015;
        double r152022 = fma(r152010, r152010, r152021);
        double r152023 = r152020 / r152022;
        double r152024 = sqrt(r152021);
        double r152025 = r152010 + r152024;
        double r152026 = r152023 / r152025;
        double r152027 = 0.0028097389045321224;
        bool r152028 = r152007 <= r152027;
        double r152029 = 2.0;
        double r152030 = pow(r152007, r152029);
        double r152031 = sqrt(r152010);
        double r152032 = 3.0;
        double r152033 = pow(r152031, r152032);
        double r152034 = r152030 / r152033;
        double r152035 = 0.25;
        double r152036 = 0.1875;
        double r152037 = pow(r152007, r152011);
        double r152038 = 5.0;
        double r152039 = pow(r152031, r152038);
        double r152040 = r152037 / r152039;
        double r152041 = r152016 / r152031;
        double r152042 = fma(r152036, r152040, r152041);
        double r152043 = r152016 - r152042;
        double r152044 = fma(r152034, r152035, r152043);
        double r152045 = r152044 / r152025;
        double r152046 = pow(r152024, r152011);
        double r152047 = r152012 - r152046;
        double r152048 = exp(r152047);
        double r152049 = log(r152048);
        double r152050 = r152049 / r152022;
        double r152051 = log1p(r152025);
        double r152052 = expm1(r152051);
        double r152053 = r152050 / r152052;
        double r152054 = r152028 ? r152045 : r152053;
        double r152055 = r152009 ? r152026 : r152054;
        return r152055;
}

Error

Bits error versus x

Derivation

1. Split input into 3 regimes

2. if x < -0.002686087558037088

   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 flip-- 0.1

      \[\leadsto \frac{\color{blue}{\frac{\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \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)}{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)}}\]

   7. Simplified 0.1

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

   8. Simplified 0.1

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

   10. Applied add-sqr-sqrt 0.1

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

   11. Simplified 0.1

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

   12. Simplified 0.1

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

   if -0.002686087558037088 < x < 0.0028097389045321224

   1. Initial program 29.9

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

   3. Applied flip-- 29.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 29.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. Taylor expanded around 0 29.9

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

   6. Simplified 0.2

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

   if 0.0028097389045321224 < 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.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 flip-- 0.1

      \[\leadsto \frac{\color{blue}{\frac{\left(1 \cdot 1\right) \cdot \left(1 \cdot 1\right) - \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)}{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)}}\]

   7. Simplified 0.1

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

   8. Simplified 0.1

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

   10. Applied add-log-exp 1.1

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

   11. Applied add-log-exp 1.1

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

   12. Applied diff-log 1.1

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

   13. Simplified 0.1

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

   15. Applied expm1-log1p-u 0.1

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

4. Final simplification 0.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le -0.002686087558037088089679667035625243443064:\\ \;\;\;\;\frac{\frac{{1}^{4} - \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|}{\mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)}}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}\\ \mathbf{elif}\;x \le 0.00280973890453212237286462205076986720087:\\ \;\;\;\;\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)}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\log \left(e^{{1}^{4} - {\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{4}}\right)}{\mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)}}{\mathsf{expm1}\left(\mathsf{log1p}\left(1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)\right)}\\ \end{array}\]

Reproduce

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