Given's Rotation SVD example, simplified

Average Error: 15.9 → 0.2

Time: 24.9s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r208956 = 1.0;
        double r208957 = 0.5;
        double r208958 = x;
        double r208959 = hypot(r208956, r208958);
        double r208960 = r208956 / r208959;
        double r208961 = r208956 + r208960;
        double r208962 = r208957 * r208961;
        double r208963 = sqrt(r208962);
        double r208964 = r208956 - r208963;
        return r208964;
}

↓

double f(double x) {
        double r208965 = 1.0;
        double r208966 = x;
        double r208967 = hypot(r208965, r208966);
        double r208968 = 1.000000000000079;
        bool r208969 = r208967 <= r208968;
        double r208970 = 0.25;
        double r208971 = 2.0;
        double r208972 = pow(r208966, r208971);
        double r208973 = sqrt(r208965);
        double r208974 = 3.0;
        double r208975 = pow(r208973, r208974);
        double r208976 = r208972 / r208975;
        double r208977 = 0.5;
        double r208978 = 4.0;
        double r208979 = pow(r208966, r208978);
        double r208980 = 5.0;
        double r208981 = pow(r208973, r208980);
        double r208982 = r208979 / r208981;
        double r208983 = 0.1875;
        double r208984 = r208977 / r208973;
        double r208985 = fma(r208982, r208983, r208984);
        double r208986 = r208977 - r208985;
        double r208987 = fma(r208970, r208976, r208986);
        double r208988 = r208965 / r208967;
        double r208989 = r208965 + r208988;
        double r208990 = r208977 * r208989;
        double r208991 = sqrt(r208990);
        double r208992 = r208965 + r208991;
        double r208993 = r208987 / r208992;
        double r208994 = exp(1.0);
        double r208995 = pow(r208965, r208978);
        double r208996 = r208989 * r208977;
        double r208997 = r208996 * r208996;
        double r208998 = r208995 - r208997;
        double r208999 = log(r208998);
        double r209000 = pow(r208994, r208999);
        double r209001 = fma(r208965, r208965, r208996);
        double r209002 = log(r209001);
        double r209003 = pow(r208994, r209002);
        double r209004 = r209000 / r209003;
        double r209005 = r209004 / r208992;
        double r209006 = r208969 ? r208993 : r209005;
        return r209006;
}

Error

Bits error versus x

Derivation

1. Split input into 2 regimes

2. if (hypot 1.0 x) < 1.000000000000079

   1. Initial program 30.8

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

   3. Applied flip-- 30.8

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

      \[\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-exp-log 30.8

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

   8. Applied pow1 30.8

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

   9. Applied log-pow 30.8

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

   10. Applied exp-prod 30.8

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

   11. Simplified 30.8

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

   12. Taylor expanded around 0 30.8

       \[\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)}}\]

   13. Simplified 0.0

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

   if 1.000000000000079 < (hypot 1.0 x)

   1. Initial program 1.4

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

   3. Applied flip-- 1.4

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

      \[\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-exp-log 0.4

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

   8. Applied pow1 0.4

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

   9. Applied log-pow 0.4

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

   10. Applied exp-prod 0.4

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

   11. Simplified 0.4

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

   13. Applied flip-- 0.4

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

   14. Applied log-div 0.4

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

   15. Applied pow-sub 0.4

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

   16. Simplified 0.4

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

   17. Simplified 0.4

       \[\leadsto \frac{\frac{{e}^{\left(\log \left({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)\right)\right)}}{\color{blue}{{e}^{\left(\log \left(\mathsf{fma}\left(1, 1, \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right)\right)\right)}}}}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.2

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

Reproduce

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