Given's Rotation SVD example, simplified

Average Error: 15.2 → 0.2

Time: 32.0s

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.000000001230617385772347915917634963989:\\ \;\;\;\;\frac{\sqrt{\mathsf{fma}\left(\frac{x}{\frac{\sqrt{1} \cdot 1}{x}}, 0.25, 0.5 - \mathsf{fma}\left(0.1875, \frac{x \cdot x}{\frac{{\left(\sqrt{1}\right)}^{5}}{x \cdot x}}, \frac{0.5}{\sqrt{1}}\right)\right)} \cdot \sqrt{\mathsf{fma}\left(\frac{x}{\frac{\sqrt{1} \cdot 1}{x}}, 0.25, 0.5 - \mathsf{fma}\left(0.1875, \frac{x \cdot x}{\frac{{\left(\sqrt{1}\right)}^{5}}{x \cdot x}}, \frac{0.5}{\sqrt{1}}\right)\right)}}{1 + \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)} \cdot \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)} - \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)} \cdot 1\right) + 1 \cdot 1\right) \cdot \left(\frac{1 \cdot 1}{\mathsf{fma}\left(0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right), \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}, \left(1 \cdot 1\right) \cdot 1\right)} - \frac{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}{\mathsf{fma}\left(0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right), \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}, \left(1 \cdot 1\right) \cdot 1\right)}\right)\\ \end{array}\]

C

double f(double x) {
        double r11490938 = 1.0;
        double r11490939 = 0.5;
        double r11490940 = x;
        double r11490941 = hypot(r11490938, r11490940);
        double r11490942 = r11490938 / r11490941;
        double r11490943 = r11490938 + r11490942;
        double r11490944 = r11490939 * r11490943;
        double r11490945 = sqrt(r11490944);
        double r11490946 = r11490938 - r11490945;
        return r11490946;
}

↓

double f(double x) {
        double r11490947 = 1.0;
        double r11490948 = x;
        double r11490949 = hypot(r11490947, r11490948);
        double r11490950 = 1.0000000012306174;
        bool r11490951 = r11490949 <= r11490950;
        double r11490952 = sqrt(r11490947);
        double r11490953 = r11490952 * r11490947;
        double r11490954 = r11490953 / r11490948;
        double r11490955 = r11490948 / r11490954;
        double r11490956 = 0.25;
        double r11490957 = 0.5;
        double r11490958 = 0.1875;
        double r11490959 = r11490948 * r11490948;
        double r11490960 = 5.0;
        double r11490961 = pow(r11490952, r11490960);
        double r11490962 = r11490961 / r11490959;
        double r11490963 = r11490959 / r11490962;
        double r11490964 = r11490957 / r11490952;
        double r11490965 = fma(r11490958, r11490963, r11490964);
        double r11490966 = r11490957 - r11490965;
        double r11490967 = fma(r11490955, r11490956, r11490966);
        double r11490968 = sqrt(r11490967);
        double r11490969 = r11490968 * r11490968;
        double r11490970 = r11490947 / r11490949;
        double r11490971 = r11490970 + r11490947;
        double r11490972 = r11490957 * r11490971;
        double r11490973 = sqrt(r11490972);
        double r11490974 = r11490947 + r11490973;
        double r11490975 = r11490969 / r11490974;
        double r11490976 = r11490973 * r11490973;
        double r11490977 = r11490973 * r11490947;
        double r11490978 = r11490976 - r11490977;
        double r11490979 = r11490947 * r11490947;
        double r11490980 = r11490978 + r11490979;
        double r11490981 = r11490979 * r11490947;
        double r11490982 = fma(r11490972, r11490973, r11490981);
        double r11490983 = r11490979 / r11490982;
        double r11490984 = r11490972 / r11490982;
        double r11490985 = r11490983 - r11490984;
        double r11490986 = r11490980 * r11490985;
        double r11490987 = r11490951 ? r11490975 : r11490986;
        return r11490987;
}

Error

Bits error versus x

Derivation

1. Split input into 2 regimes

2. if (hypot 1.0 x) < 1.0000000012306174

   1. Initial program 29.6

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

   3. Applied flip-- 29.6

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

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

   5. Taylor expanded around 0 29.6

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

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

   8. Applied add-sqr-sqrt 0.2

      \[\leadsto \frac{\color{blue}{\sqrt{\mathsf{fma}\left(\frac{x}{\frac{1 \cdot \sqrt{1}}{x}}, 0.25, 0.5 - \mathsf{fma}\left(0.1875, \frac{x \cdot x}{\frac{{\left(\sqrt{1}\right)}^{5}}{x \cdot x}}, \frac{0.5}{\sqrt{1}}\right)\right)} \cdot \sqrt{\mathsf{fma}\left(\frac{x}{\frac{1 \cdot \sqrt{1}}{x}}, 0.25, 0.5 - \mathsf{fma}\left(0.1875, \frac{x \cdot x}{\frac{{\left(\sqrt{1}\right)}^{5}}{x \cdot x}}, \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.0000000012306174 < (hypot 1.0 x)

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

      \[\leadsto \frac{\color{blue}{1 \cdot 1 - 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)}}\]
   5. Using strategy rm

   6. Applied flip3-+ 1.1

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

   7. Applied associate-/r/ 0.2

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

   8. Simplified 0.2

      \[\leadsto \color{blue}{\left(\frac{1 \cdot 1}{\mathsf{fma}\left(0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right), \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}, \left(1 \cdot 1\right) \cdot 1\right)} - \frac{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}{\mathsf{fma}\left(0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right), \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}, \left(1 \cdot 1\right) \cdot 1\right)}\right)} \cdot \left(1 \cdot 1 + \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)} - 1 \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\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.000000001230617385772347915917634963989:\\ \;\;\;\;\frac{\sqrt{\mathsf{fma}\left(\frac{x}{\frac{\sqrt{1} \cdot 1}{x}}, 0.25, 0.5 - \mathsf{fma}\left(0.1875, \frac{x \cdot x}{\frac{{\left(\sqrt{1}\right)}^{5}}{x \cdot x}}, \frac{0.5}{\sqrt{1}}\right)\right)} \cdot \sqrt{\mathsf{fma}\left(\frac{x}{\frac{\sqrt{1} \cdot 1}{x}}, 0.25, 0.5 - \mathsf{fma}\left(0.1875, \frac{x \cdot x}{\frac{{\left(\sqrt{1}\right)}^{5}}{x \cdot x}}, \frac{0.5}{\sqrt{1}}\right)\right)}}{1 + \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)} \cdot \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)} - \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)} \cdot 1\right) + 1 \cdot 1\right) \cdot \left(\frac{1 \cdot 1}{\mathsf{fma}\left(0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right), \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}, \left(1 \cdot 1\right) \cdot 1\right)} - \frac{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}{\mathsf{fma}\left(0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right), \sqrt{0.5 \cdot \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right)}, \left(1 \cdot 1\right) \cdot 1\right)}\right)\\ \end{array}\]

Reproduce

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