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

Average Error: 5.7 → 3.8

Time: 15.0s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

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.0248860342918865 \cdot 10^{30}:\\ \;\;\;\;\left(\left(\log \left(\sqrt[3]{x} \cdot \left(\sqrt[3]{\sqrt{x}} \cdot \sqrt[3]{\sqrt{x}}\right)\right) \cdot \left(x - 0.5\right) + \left(\log \left({\left({x}^{\left(\sqrt[3]{\frac{1}{3}} \cdot \sqrt[3]{\frac{1}{3}}\right)}\right)}^{\left(\sqrt[3]{\frac{1}{3}}\right)}\right) \cdot \left(x - 0.5\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}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\right) - x\right)\right) + 0.91893853320467001\right) + \left(\frac{{z}^{2}}{x} \cdot \left(y + 7.93650079365100015 \cdot 10^{-4}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)\\ \end{array}\]

C

double f(double x, double y, double z) {
        double r393904 = x;
        double r393905 = 0.5;
        double r393906 = r393904 - r393905;
        double r393907 = log(r393904);
        double r393908 = r393906 * r393907;
        double r393909 = r393908 - r393904;
        double r393910 = 0.91893853320467;
        double r393911 = r393909 + r393910;
        double r393912 = y;
        double r393913 = 0.0007936500793651;
        double r393914 = r393912 + r393913;
        double r393915 = z;
        double r393916 = r393914 * r393915;
        double r393917 = 0.0027777777777778;
        double r393918 = r393916 - r393917;
        double r393919 = r393918 * r393915;
        double r393920 = 0.083333333333333;
        double r393921 = r393919 + r393920;
        double r393922 = r393921 / r393904;
        double r393923 = r393911 + r393922;
        return r393923;
}

↓

double f(double x, double y, double z) {
        double r393924 = x;
        double r393925 = 9.024886034291887e+30;
        bool r393926 = r393924 <= r393925;
        double r393927 = cbrt(r393924);
        double r393928 = sqrt(r393924);
        double r393929 = cbrt(r393928);
        double r393930 = r393929 * r393929;
        double r393931 = r393927 * r393930;
        double r393932 = log(r393931);
        double r393933 = 0.5;
        double r393934 = r393924 - r393933;
        double r393935 = r393932 * r393934;
        double r393936 = 0.3333333333333333;
        double r393937 = cbrt(r393936);
        double r393938 = r393937 * r393937;
        double r393939 = pow(r393924, r393938);
        double r393940 = pow(r393939, r393937);
        double r393941 = log(r393940);
        double r393942 = r393941 * r393934;
        double r393943 = r393942 - r393924;
        double r393944 = r393935 + r393943;
        double r393945 = 0.91893853320467;
        double r393946 = r393944 + r393945;
        double r393947 = y;
        double r393948 = 0.0007936500793651;
        double r393949 = r393947 + r393948;
        double r393950 = z;
        double r393951 = r393949 * r393950;
        double r393952 = 0.0027777777777778;
        double r393953 = r393951 - r393952;
        double r393954 = r393953 * r393950;
        double r393955 = 0.083333333333333;
        double r393956 = r393954 + r393955;
        double r393957 = r393956 / r393924;
        double r393958 = r393946 + r393957;
        double r393959 = r393927 * r393927;
        double r393960 = log(r393959);
        double r393961 = r393960 * r393934;
        double r393962 = log(r393927);
        double r393963 = r393962 * r393934;
        double r393964 = r393963 - r393924;
        double r393965 = r393961 + r393964;
        double r393966 = r393965 + r393945;
        double r393967 = 2.0;
        double r393968 = pow(r393950, r393967);
        double r393969 = r393968 / r393924;
        double r393970 = r393969 * r393949;
        double r393971 = r393950 / r393924;
        double r393972 = r393952 * r393971;
        double r393973 = r393970 - r393972;
        double r393974 = r393966 + r393973;
        double r393975 = r393926 ? r393958 : r393974;
        return r393975;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	5.7
Target	1.2
Herbie	3.8

\[\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.024886034291887e+30

   1. Initial program 0.2

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

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

      \[\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-rgt-in 0.2

      \[\leadsto \left(\left(\color{blue}{\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\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+ 0.2

      \[\leadsto \left(\color{blue}{\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\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. Using strategy rm

   8. Applied pow1/3 0.2

      \[\leadsto \left(\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \left(\log \color{blue}{\left({x}^{\frac{1}{3}}\right)} \cdot \left(x - 0.5\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}\]
   9. Using strategy rm

   10. Applied add-sqr-sqrt 0.2

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

   11. Applied cbrt-prod 0.2

       \[\leadsto \left(\left(\log \left(\sqrt[3]{x} \cdot \color{blue}{\left(\sqrt[3]{\sqrt{x}} \cdot \sqrt[3]{\sqrt{x}}\right)}\right) \cdot \left(x - 0.5\right) + \left(\log \left({x}^{\frac{1}{3}}\right) \cdot \left(x - 0.5\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}\]
   12. Using strategy rm

   13. Applied add-cube-cbrt 0.2

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

   14. Applied pow-unpow 0.2

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

   if 9.024886034291887e+30 < x

   1. Initial program 10.6

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

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

      \[\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-rgt-in 10.7

      \[\leadsto \left(\left(\color{blue}{\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\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+ 10.6

      \[\leadsto \left(\color{blue}{\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\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. Taylor expanded around inf 10.7

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

   8. Simplified 6.9

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

4. Final simplification 3.8

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le 9.0248860342918865 \cdot 10^{30}:\\ \;\;\;\;\left(\left(\log \left(\sqrt[3]{x} \cdot \left(\sqrt[3]{\sqrt{x}} \cdot \sqrt[3]{\sqrt{x}}\right)\right) \cdot \left(x - 0.5\right) + \left(\log \left({\left({x}^{\left(\sqrt[3]{\frac{1}{3}} \cdot \sqrt[3]{\frac{1}{3}}\right)}\right)}^{\left(\sqrt[3]{\frac{1}{3}}\right)}\right) \cdot \left(x - 0.5\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}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\right) - x\right)\right) + 0.91893853320467001\right) + \left(\frac{{z}^{2}}{x} \cdot \left(y + 7.93650079365100015 \cdot 10^{-4}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020045 
(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)))