Given's Rotation SVD example, simplified

Average Error: 15.7 → 0.2

Time: 7.5s

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.00140844293895725134:\\ \;\;\;\;\frac{\mathsf{fma}\left(-0.5, 1 + e^{\log \left(\frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 1 \cdot 1\right)}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}\\ \mathbf{elif}\;x \le 4.6405660865541179 \cdot 10^{-4}:\\ \;\;\;\;\frac{\mathsf{fma}\left(0.25, \frac{{x}^{2}}{{\left(\sqrt{1}\right)}^{3}}, 0.5 - \mathsf{fma}\left(0.5, \frac{1}{\sqrt{1}}, 0.1875 \cdot \frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5}}\right)\right)}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\log \left(\mathsf{fma}\left(-0.5, 1 + e^{2 \cdot \log \left(\frac{\sqrt[3]{1}}{\sqrt[3]{\mathsf{hypot}\left(1, x\right)}}\right) + \log \left(\frac{\sqrt[3]{1}}{\sqrt[3]{\mathsf{hypot}\left(1, x\right)}}\right)}, 1 \cdot 1\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 r246743 = 1.0;
        double r246744 = 0.5;
        double r246745 = x;
        double r246746 = hypot(r246743, r246745);
        double r246747 = r246743 / r246746;
        double r246748 = r246743 + r246747;
        double r246749 = r246744 * r246748;
        double r246750 = sqrt(r246749);
        double r246751 = r246743 - r246750;
        return r246751;
}

↓

double f(double x) {
        double r246752 = x;
        double r246753 = -0.0014084429389572513;
        bool r246754 = r246752 <= r246753;
        double r246755 = 0.5;
        double r246756 = -r246755;
        double r246757 = 1.0;
        double r246758 = hypot(r246757, r246752);
        double r246759 = r246757 / r246758;
        double r246760 = log(r246759);
        double r246761 = exp(r246760);
        double r246762 = r246757 + r246761;
        double r246763 = r246757 * r246757;
        double r246764 = fma(r246756, r246762, r246763);
        double r246765 = r246757 + r246759;
        double r246766 = r246755 * r246765;
        double r246767 = sqrt(r246766);
        double r246768 = r246757 + r246767;
        double r246769 = r246764 / r246768;
        double r246770 = 0.0004640566086554118;
        bool r246771 = r246752 <= r246770;
        double r246772 = 0.25;
        double r246773 = 2.0;
        double r246774 = pow(r246752, r246773);
        double r246775 = sqrt(r246757);
        double r246776 = 3.0;
        double r246777 = pow(r246775, r246776);
        double r246778 = r246774 / r246777;
        double r246779 = 1.0;
        double r246780 = r246779 / r246775;
        double r246781 = 0.1875;
        double r246782 = 4.0;
        double r246783 = pow(r246752, r246782);
        double r246784 = 5.0;
        double r246785 = pow(r246775, r246784);
        double r246786 = r246783 / r246785;
        double r246787 = r246781 * r246786;
        double r246788 = fma(r246755, r246780, r246787);
        double r246789 = r246755 - r246788;
        double r246790 = fma(r246772, r246778, r246789);
        double r246791 = r246790 / r246768;
        double r246792 = cbrt(r246757);
        double r246793 = cbrt(r246758);
        double r246794 = r246792 / r246793;
        double r246795 = log(r246794);
        double r246796 = r246773 * r246795;
        double r246797 = r246796 + r246795;
        double r246798 = exp(r246797);
        double r246799 = r246757 + r246798;
        double r246800 = fma(r246756, r246799, r246763);
        double r246801 = log(r246800);
        double r246802 = exp(r246801);
        double r246803 = r246802 / r246768;
        double r246804 = r246771 ? r246791 : r246803;
        double r246805 = r246754 ? r246769 : r246804;
        return r246805;
}

Error

Bits error versus x

Derivation

1. Split input into 3 regimes

2. if x < -0.0014084429389572513

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

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

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

   7. Applied add-exp-log 0.1

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

   8. Applied div-exp 0.1

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

   9. Simplified 0.1

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

   if -0.0014084429389572513 < x < 0.0004640566086554118

   1. Initial program 30.5

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

   3. Applied flip-- 30.5

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

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

   5. Taylor expanded around 0 30.5

      \[\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(0.25, \frac{{x}^{2}}{{\left(\sqrt{1}\right)}^{3}}, 0.5 - \mathsf{fma}\left(0.5, \frac{1}{\sqrt{1}}, 0.1875 \cdot \frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5}}\right)\right)}}{1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}\]

   if 0.0004640566086554118 < 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}{\mathsf{fma}\left(-0.5, 1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}, 1 \cdot 1\right)}}{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.2

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

   7. Applied add-exp-log 0.2

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

   8. Applied div-exp 0.2

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

   9. Simplified 0.2

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

   11. Applied add-cube-cbrt 0.2

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

   12. Applied add-cube-cbrt 0.2

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

   13. Applied times-frac 0.2

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

   14. Applied log-prod 0.2

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

   15. Simplified 0.2

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

   17. Applied add-exp-log 0.2

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

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

Reproduce

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