Numeric.SpecFunctions:$slogFactorial from math-functions-0.1.5.2, B

Average Error: 5.7 → 5.0

Time: 10.3s

Precision: 64

Math

\[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

↓

\[\begin{array}{l} \mathbf{if}\;x \le 9.7322041981229518 \cdot 10^{136}:\\ \;\;\;\;\left(\left(\left(x - 0.5\right) \cdot \left(2 \cdot \log \left(\sqrt[3]{\sqrt{x}}\right)\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{\sqrt{x}}\right)\right) + \left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{1}{\frac{x}{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(x - 0.5\right) \cdot \left(2 \cdot \log \left(\sqrt[3]{x}\right)\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right)\right) - x\right) + 0.91893853320467001\right) + \left(\left(7.93650079365100015 \cdot 10^{-4} \cdot \frac{{z}^{2}}{x} + 0.0833333333333329956 \cdot \frac{1}{x}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)\\ \end{array}\]

C

double f(double x, double y, double z) {
        double r484865 = x;
        double r484866 = 0.5;
        double r484867 = r484865 - r484866;
        double r484868 = log(r484865);
        double r484869 = r484867 * r484868;
        double r484870 = r484869 - r484865;
        double r484871 = 0.91893853320467;
        double r484872 = r484870 + r484871;
        double r484873 = y;
        double r484874 = 0.0007936500793651;
        double r484875 = r484873 + r484874;
        double r484876 = z;
        double r484877 = r484875 * r484876;
        double r484878 = 0.0027777777777778;
        double r484879 = r484877 - r484878;
        double r484880 = r484879 * r484876;
        double r484881 = 0.083333333333333;
        double r484882 = r484880 + r484881;
        double r484883 = r484882 / r484865;
        double r484884 = r484872 + r484883;
        return r484884;
}

↓

double f(double x, double y, double z) {
        double r484885 = x;
        double r484886 = 9.732204198122952e+136;
        bool r484887 = r484885 <= r484886;
        double r484888 = 0.5;
        double r484889 = r484885 - r484888;
        double r484890 = 2.0;
        double r484891 = sqrt(r484885);
        double r484892 = cbrt(r484891);
        double r484893 = log(r484892);
        double r484894 = r484890 * r484893;
        double r484895 = r484889 * r484894;
        double r484896 = r484889 * r484893;
        double r484897 = r484895 + r484896;
        double r484898 = log(r484891);
        double r484899 = r484898 * r484889;
        double r484900 = r484899 - r484885;
        double r484901 = 0.91893853320467;
        double r484902 = r484900 + r484901;
        double r484903 = r484897 + r484902;
        double r484904 = 1.0;
        double r484905 = y;
        double r484906 = 0.0007936500793651;
        double r484907 = r484905 + r484906;
        double r484908 = z;
        double r484909 = r484907 * r484908;
        double r484910 = 0.0027777777777778;
        double r484911 = r484909 - r484910;
        double r484912 = r484911 * r484908;
        double r484913 = 0.083333333333333;
        double r484914 = r484912 + r484913;
        double r484915 = r484885 / r484914;
        double r484916 = r484904 / r484915;
        double r484917 = r484903 + r484916;
        double r484918 = cbrt(r484885);
        double r484919 = log(r484918);
        double r484920 = r484890 * r484919;
        double r484921 = r484889 * r484920;
        double r484922 = r484889 * r484919;
        double r484923 = r484921 + r484922;
        double r484924 = r484923 - r484885;
        double r484925 = r484924 + r484901;
        double r484926 = pow(r484908, r484890);
        double r484927 = r484926 / r484885;
        double r484928 = r484906 * r484927;
        double r484929 = r484904 / r484885;
        double r484930 = r484913 * r484929;
        double r484931 = r484928 + r484930;
        double r484932 = r484908 / r484885;
        double r484933 = r484910 * r484932;
        double r484934 = r484931 - r484933;
        double r484935 = r484925 + r484934;
        double r484936 = r484887 ? r484917 : r484935;
        return r484936;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	5.7
Target	1.1
Herbie	5.0

\[\left(\left(\left(x - 0.5\right) \cdot \log x + \left(0.91893853320467001 - x\right)\right) + \frac{0.0833333333333329956}{x}\right) + \frac{z}{x} \cdot \left(z \cdot \left(y + 7.93650079365100015 \cdot 10^{-4}\right) - 0.0027777777777778\right)\]

Derivation

1. Split input into 2 regimes

2. if x < 9.732204198122952e+136

   1. Initial program 1.8

      \[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]
   2. Using strategy rm

   3. Applied add-sqr-sqrt 1.9

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)} - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   4. Applied log-prod 1.9

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \color{blue}{\left(\log \left(\sqrt{x}\right) + \log \left(\sqrt{x}\right)\right)} - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   5. Applied distribute-lft-in 1.9

      \[\leadsto \left(\left(\color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right)\right)} - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   6. Applied associate--l+ 1.9

      \[\leadsto \left(\color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right)\right)} + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   7. Applied associate-+l+ 1.9

      \[\leadsto \color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right) + 0.91893853320467001\right)\right)} + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   8. Simplified 1.9

      \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \color{blue}{\left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)}\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]
   9. Using strategy rm

   10. Applied clear-num 2.0

       \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \color{blue}{\frac{1}{\frac{x}{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}}}\]
   11. Using strategy rm

   12. Applied add-cube-cbrt 2.0

       \[\leadsto \left(\left(x - 0.5\right) \cdot \log \color{blue}{\left(\left(\sqrt[3]{\sqrt{x}} \cdot \sqrt[3]{\sqrt{x}}\right) \cdot \sqrt[3]{\sqrt{x}}\right)} + \left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{1}{\frac{x}{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}}\]

   13. Applied log-prod 2.0

       \[\leadsto \left(\left(x - 0.5\right) \cdot \color{blue}{\left(\log \left(\sqrt[3]{\sqrt{x}} \cdot \sqrt[3]{\sqrt{x}}\right) + \log \left(\sqrt[3]{\sqrt{x}}\right)\right)} + \left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{1}{\frac{x}{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}}\]

   14. Applied distribute-lft-in 2.0

       \[\leadsto \left(\color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{\sqrt{x}} \cdot \sqrt[3]{\sqrt{x}}\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{\sqrt{x}}\right)\right)} + \left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{1}{\frac{x}{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}}\]

   15. Simplified 2.0

       \[\leadsto \left(\left(\color{blue}{\left(x - 0.5\right) \cdot \left(2 \cdot \log \left(\sqrt[3]{\sqrt{x}}\right)\right)} + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{\sqrt{x}}\right)\right) + \left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{1}{\frac{x}{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}}\]

   if 9.732204198122952e+136 < x

   1. Initial program 13.0

      \[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]
   2. Using strategy rm

   3. Applied add-cube-cbrt 13.0

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \color{blue}{\left(\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \sqrt[3]{x}\right)} - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   4. Applied log-prod 13.1

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \color{blue}{\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \log \left(\sqrt[3]{x}\right)\right)} - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   5. Applied distribute-lft-in 13.1

      \[\leadsto \left(\left(\color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right)\right)} - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   6. Simplified 13.1

      \[\leadsto \left(\left(\left(\color{blue}{\left(x - 0.5\right) \cdot \left(2 \cdot \log \left(\sqrt[3]{x}\right)\right)} + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right)\right) - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   7. Taylor expanded around 0 10.5

      \[\leadsto \left(\left(\left(\left(x - 0.5\right) \cdot \left(2 \cdot \log \left(\sqrt[3]{x}\right)\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right)\right) - x\right) + 0.91893853320467001\right) + \color{blue}{\left(\left(7.93650079365100015 \cdot 10^{-4} \cdot \frac{{z}^{2}}{x} + 0.0833333333333329956 \cdot \frac{1}{x}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)}\]
3. Recombined 2 regimes into one program.

4. Final simplification 5.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le 9.7322041981229518 \cdot 10^{136}:\\ \;\;\;\;\left(\left(\left(x - 0.5\right) \cdot \left(2 \cdot \log \left(\sqrt[3]{\sqrt{x}}\right)\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{\sqrt{x}}\right)\right) + \left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{1}{\frac{x}{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(x - 0.5\right) \cdot \left(2 \cdot \log \left(\sqrt[3]{x}\right)\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right)\right) - x\right) + 0.91893853320467001\right) + \left(\left(7.93650079365100015 \cdot 10^{-4} \cdot \frac{{z}^{2}}{x} + 0.0833333333333329956 \cdot \frac{1}{x}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020034 
(FPCore (x y z)
  :name "Numeric.SpecFunctions:$slogFactorial from math-functions-0.1.5.2, B"
  :precision binary64

  :herbie-target
  (+ (+ (+ (* (- x 0.5) (log x)) (- 0.91893853320467 x)) (/ 0.083333333333333 x)) (* (/ z x) (- (* z (+ y 0.0007936500793651)) 0.0027777777777778)))

  (+ (+ (- (* (- x 0.5) (log x)) x) 0.91893853320467) (/ (+ (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z) 0.083333333333333) x)))