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

Average Error: 5.5 → 4.8

Time: 9.4s

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 1.27804641027178125 \cdot 10^{148}:\\ \;\;\;\;\left(\left(\left(\left(x - 0.5\right) \cdot \left(\log \left(\sqrt[3]{\sqrt[3]{x} \cdot \sqrt[3]{x}}\right) \cdot 2\right) + \left(x - 0.5\right) \cdot \left(\log \left(\sqrt[3]{\sqrt[3]{x}}\right) \cdot 2 + \log \left(\sqrt[3]{x}\right)\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}\\ \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 r517798 = x;
        double r517799 = 0.5;
        double r517800 = r517798 - r517799;
        double r517801 = log(r517798);
        double r517802 = r517800 * r517801;
        double r517803 = r517802 - r517798;
        double r517804 = 0.91893853320467;
        double r517805 = r517803 + r517804;
        double r517806 = y;
        double r517807 = 0.0007936500793651;
        double r517808 = r517806 + r517807;
        double r517809 = z;
        double r517810 = r517808 * r517809;
        double r517811 = 0.0027777777777778;
        double r517812 = r517810 - r517811;
        double r517813 = r517812 * r517809;
        double r517814 = 0.083333333333333;
        double r517815 = r517813 + r517814;
        double r517816 = r517815 / r517798;
        double r517817 = r517805 + r517816;
        return r517817;
}

↓

double f(double x, double y, double z) {
        double r517818 = x;
        double r517819 = 1.2780464102717813e+148;
        bool r517820 = r517818 <= r517819;
        double r517821 = 0.5;
        double r517822 = r517818 - r517821;
        double r517823 = cbrt(r517818);
        double r517824 = r517823 * r517823;
        double r517825 = cbrt(r517824);
        double r517826 = log(r517825);
        double r517827 = 2.0;
        double r517828 = r517826 * r517827;
        double r517829 = r517822 * r517828;
        double r517830 = cbrt(r517823);
        double r517831 = log(r517830);
        double r517832 = r517831 * r517827;
        double r517833 = log(r517823);
        double r517834 = r517832 + r517833;
        double r517835 = r517822 * r517834;
        double r517836 = r517829 + r517835;
        double r517837 = r517836 - r517818;
        double r517838 = 0.91893853320467;
        double r517839 = r517837 + r517838;
        double r517840 = y;
        double r517841 = 0.0007936500793651;
        double r517842 = r517840 + r517841;
        double r517843 = z;
        double r517844 = r517842 * r517843;
        double r517845 = 0.0027777777777778;
        double r517846 = r517844 - r517845;
        double r517847 = r517846 * r517843;
        double r517848 = 0.083333333333333;
        double r517849 = r517847 + r517848;
        double r517850 = r517849 / r517818;
        double r517851 = r517839 + r517850;
        double r517852 = r517827 * r517833;
        double r517853 = r517822 * r517852;
        double r517854 = r517822 * r517833;
        double r517855 = r517853 + r517854;
        double r517856 = r517855 - r517818;
        double r517857 = r517856 + r517838;
        double r517858 = pow(r517843, r517827);
        double r517859 = r517858 / r517818;
        double r517860 = r517841 * r517859;
        double r517861 = 1.0;
        double r517862 = r517861 / r517818;
        double r517863 = r517848 * r517862;
        double r517864 = r517860 + r517863;
        double r517865 = r517843 / r517818;
        double r517866 = r517845 * r517865;
        double r517867 = r517864 - r517866;
        double r517868 = r517857 + r517867;
        double r517869 = r517820 ? r517851 : r517868;
        return r517869;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	5.5
Target	1.2
Herbie	4.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 < 1.2780464102717813e+148

   1. Initial program 2.1

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

      \[\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 2.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 2.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 2.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. Using strategy rm

   8. Applied add-cube-cbrt 2.1

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

   9. Applied cbrt-prod 2.1

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

   10. Applied log-prod 2.1

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

   11. Applied distribute-rgt-in 2.1

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

   12. Applied distribute-lft-in 2.1

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

   13. Applied associate-+l+ 2.1

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

   14. Simplified 2.1

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

   if 1.2780464102717813e+148 < x

   1. Initial program 12.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-cube-cbrt 12.8

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

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

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

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

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

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le 1.27804641027178125 \cdot 10^{148}:\\ \;\;\;\;\left(\left(\left(\left(x - 0.5\right) \cdot \left(\log \left(\sqrt[3]{\sqrt[3]{x} \cdot \sqrt[3]{x}}\right) \cdot 2\right) + \left(x - 0.5\right) \cdot \left(\log \left(\sqrt[3]{\sqrt[3]{x}}\right) \cdot 2 + \log \left(\sqrt[3]{x}\right)\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}\\ \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 2020062 
(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)))