Given's Rotation SVD example, simplified

Average Error: 15.5 → 0.2

Time: 23.3s

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.000000000005262457136723242001608014107:\\ \;\;\;\;\frac{\mathsf{fma}\left(\frac{{x}^{2}}{{\left(\sqrt{1}\right)}^{3}}, 0.25, 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{\sqrt{\log \left(e^{1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}\right)}}{\frac{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}{\sqrt{\sqrt[3]{{\left(1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right)}^{3}}}}}\\ \end{array}\]

C

double f(double x) {
        double r168051 = 1.0;
        double r168052 = 0.5;
        double r168053 = x;
        double r168054 = hypot(r168051, r168053);
        double r168055 = r168051 / r168054;
        double r168056 = r168051 + r168055;
        double r168057 = r168052 * r168056;
        double r168058 = sqrt(r168057);
        double r168059 = r168051 - r168058;
        return r168059;
}

↓

double f(double x) {
        double r168060 = 1.0;
        double r168061 = x;
        double r168062 = hypot(r168060, r168061);
        double r168063 = 1.0000000000052625;
        bool r168064 = r168062 <= r168063;
        double r168065 = 2.0;
        double r168066 = pow(r168061, r168065);
        double r168067 = sqrt(r168060);
        double r168068 = 3.0;
        double r168069 = pow(r168067, r168068);
        double r168070 = r168066 / r168069;
        double r168071 = 0.25;
        double r168072 = 0.5;
        double r168073 = 4.0;
        double r168074 = pow(r168061, r168073);
        double r168075 = 5.0;
        double r168076 = pow(r168067, r168075);
        double r168077 = r168074 / r168076;
        double r168078 = 0.1875;
        double r168079 = r168072 / r168067;
        double r168080 = fma(r168077, r168078, r168079);
        double r168081 = r168072 - r168080;
        double r168082 = fma(r168070, r168071, r168081);
        double r168083 = r168060 / r168062;
        double r168084 = r168060 + r168083;
        double r168085 = r168072 * r168084;
        double r168086 = sqrt(r168085);
        double r168087 = r168060 + r168086;
        double r168088 = r168082 / r168087;
        double r168089 = r168060 * r168060;
        double r168090 = r168084 * r168072;
        double r168091 = r168089 - r168090;
        double r168092 = exp(r168091);
        double r168093 = log(r168092);
        double r168094 = sqrt(r168093);
        double r168095 = pow(r168091, r168068);
        double r168096 = cbrt(r168095);
        double r168097 = sqrt(r168096);
        double r168098 = r168087 / r168097;
        double r168099 = r168094 / r168098;
        double r168100 = r168064 ? r168088 : r168099;
        return r168100;
}

Error

Bits error versus x

Derivation

1. Split input into 2 regimes

2. if (hypot 1.0 x) < 1.0000000000052625

   1. Initial program 30.0

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

   3. Applied flip-- 30.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 30.0

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

      \[\leadsto \frac{1 \cdot 1 - \color{blue}{\log \left(e^{\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. Applied add-log-exp 30.0

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

   8. Applied diff-log 30.0

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

   9. Simplified 30.0

      \[\leadsto \frac{\log \color{blue}{\left(e^{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. Taylor expanded around 0 30.0

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

   11. Simplified 0.1

       \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\frac{{x}^{2}}{{\left(\sqrt{1}\right)}^{3}}, 0.25, 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.0000000000052625 < (hypot 1.0 x)

   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.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-log-exp 0.3

      \[\leadsto \frac{1 \cdot 1 - \color{blue}{\log \left(e^{\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. Applied add-log-exp 0.3

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

   8. Applied diff-log 1.2

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

   9. Simplified 0.3

      \[\leadsto \frac{\log \color{blue}{\left(e^{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. Using strategy rm

   11. Applied add-sqr-sqrt 1.2

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

   12. Applied associate-/l* 1.2

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

   13. Simplified 1.2

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

   15. Applied add-cbrt-cube 0.3

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

   16. Simplified 0.3

       \[\leadsto \frac{\sqrt{\log \left(e^{1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}\right)}}{\frac{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}{\sqrt{\sqrt[3]{\color{blue}{{\left(1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right)}^{3}}}}}}\]
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.000000000005262457136723242001608014107:\\ \;\;\;\;\frac{\mathsf{fma}\left(\frac{{x}^{2}}{{\left(\sqrt{1}\right)}^{3}}, 0.25, 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{\sqrt{\log \left(e^{1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}\right)}}{\frac{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}{\sqrt{\sqrt[3]{{\left(1 \cdot 1 - \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5\right)}^{3}}}}}\\ \end{array}\]

Reproduce

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