Numeric.SpecFunctions:invIncompleteBetaWorker from math-functions-0.1.5.2, B

Average Error: 9.6 → 0.4

Time: 21.4s

Precision: 64

Math

\[\left(x \cdot \log y + z \cdot \log \left(1 - y\right)\right) - t\]

↓

\[\left(\left(z \cdot \left(\log 1 - 1 \cdot y\right) - \frac{\left(y \cdot y\right) \cdot \left(\frac{1}{2} \cdot z\right)}{1 \cdot 1}\right) + \left(\left(\log \left(\sqrt[3]{\sqrt[3]{y} \cdot \sqrt[3]{y}}\right) \cdot 2\right) \cdot x + \left(\log \left(\sqrt[3]{y}\right) + \log \left(\sqrt[3]{\sqrt[3]{y}}\right) \cdot 2\right) \cdot x\right)\right) - t\]

C

double f(double x, double y, double z, double t) {
        double r248023 = x;
        double r248024 = y;
        double r248025 = log(r248024);
        double r248026 = r248023 * r248025;
        double r248027 = z;
        double r248028 = 1.0;
        double r248029 = r248028 - r248024;
        double r248030 = log(r248029);
        double r248031 = r248027 * r248030;
        double r248032 = r248026 + r248031;
        double r248033 = t;
        double r248034 = r248032 - r248033;
        return r248034;
}

↓

double f(double x, double y, double z, double t) {
        double r248035 = z;
        double r248036 = 1.0;
        double r248037 = log(r248036);
        double r248038 = y;
        double r248039 = r248036 * r248038;
        double r248040 = r248037 - r248039;
        double r248041 = r248035 * r248040;
        double r248042 = r248038 * r248038;
        double r248043 = 0.5;
        double r248044 = r248043 * r248035;
        double r248045 = r248042 * r248044;
        double r248046 = r248036 * r248036;
        double r248047 = r248045 / r248046;
        double r248048 = r248041 - r248047;
        double r248049 = cbrt(r248038);
        double r248050 = r248049 * r248049;
        double r248051 = cbrt(r248050);
        double r248052 = log(r248051);
        double r248053 = 2.0;
        double r248054 = r248052 * r248053;
        double r248055 = x;
        double r248056 = r248054 * r248055;
        double r248057 = log(r248049);
        double r248058 = cbrt(r248049);
        double r248059 = log(r248058);
        double r248060 = r248059 * r248053;
        double r248061 = r248057 + r248060;
        double r248062 = r248061 * r248055;
        double r248063 = r248056 + r248062;
        double r248064 = r248048 + r248063;
        double r248065 = t;
        double r248066 = r248064 - r248065;
        return r248066;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	9.6
Target	0.3
Herbie	0.4

\[\left(-z\right) \cdot \left(\left(0.5 \cdot \left(y \cdot y\right) + y\right) + \frac{0.3333333333333333148296162562473909929395}{1 \cdot \left(1 \cdot 1\right)} \cdot \left(y \cdot \left(y \cdot y\right)\right)\right) - \left(t - x \cdot \log y\right)\]

Derivation

1. Initial program 9.6

   \[\left(x \cdot \log y + z \cdot \log \left(1 - y\right)\right) - t\]

2. Taylor expanded around 0 0.4

   \[\leadsto \left(x \cdot \log y + \color{blue}{\left(\log 1 \cdot z - \left(\frac{1}{2} \cdot \frac{z \cdot {y}^{2}}{{1}^{2}} + 1 \cdot \left(z \cdot y\right)\right)\right)}\right) - t\]

3. Simplified 0.4

   \[\leadsto \left(x \cdot \log y + \color{blue}{\left(z \cdot \left(\log 1 - y \cdot 1\right) - \frac{\left(z \cdot \frac{1}{2}\right) \cdot \left(y \cdot y\right)}{1 \cdot 1}\right)}\right) - t\]
4. Using strategy rm

5. Applied add-cube-cbrt 0.4

   \[\leadsto \left(x \cdot \log \color{blue}{\left(\left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) \cdot \sqrt[3]{y}\right)} + \left(z \cdot \left(\log 1 - y \cdot 1\right) - \frac{\left(z \cdot \frac{1}{2}\right) \cdot \left(y \cdot y\right)}{1 \cdot 1}\right)\right) - t\]

6. Applied log-prod 0.4

   \[\leadsto \left(x \cdot \color{blue}{\left(\log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) + \log \left(\sqrt[3]{y}\right)\right)} + \left(z \cdot \left(\log 1 - y \cdot 1\right) - \frac{\left(z \cdot \frac{1}{2}\right) \cdot \left(y \cdot y\right)}{1 \cdot 1}\right)\right) - t\]

7. Applied distribute-lft-in 0.4

   \[\leadsto \left(\color{blue}{\left(x \cdot \log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) + x \cdot \log \left(\sqrt[3]{y}\right)\right)} + \left(z \cdot \left(\log 1 - y \cdot 1\right) - \frac{\left(z \cdot \frac{1}{2}\right) \cdot \left(y \cdot y\right)}{1 \cdot 1}\right)\right) - t\]

8. Simplified 0.4

   \[\leadsto \left(\left(\color{blue}{x \cdot \left(2 \cdot \log \left(\sqrt[3]{y}\right)\right)} + x \cdot \log \left(\sqrt[3]{y}\right)\right) + \left(z \cdot \left(\log 1 - y \cdot 1\right) - \frac{\left(z \cdot \frac{1}{2}\right) \cdot \left(y \cdot y\right)}{1 \cdot 1}\right)\right) - t\]
9. Using strategy rm

10. Applied add-cube-cbrt 0.4

    \[\leadsto \left(\left(x \cdot \left(2 \cdot \log \left(\sqrt[3]{\color{blue}{\left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) \cdot \sqrt[3]{y}}}\right)\right) + x \cdot \log \left(\sqrt[3]{y}\right)\right) + \left(z \cdot \left(\log 1 - y \cdot 1\right) - \frac{\left(z \cdot \frac{1}{2}\right) \cdot \left(y \cdot y\right)}{1 \cdot 1}\right)\right) - t\]

11. Applied cbrt-prod 0.4

    \[\leadsto \left(\left(x \cdot \left(2 \cdot \log \color{blue}{\left(\sqrt[3]{\sqrt[3]{y} \cdot \sqrt[3]{y}} \cdot \sqrt[3]{\sqrt[3]{y}}\right)}\right) + x \cdot \log \left(\sqrt[3]{y}\right)\right) + \left(z \cdot \left(\log 1 - y \cdot 1\right) - \frac{\left(z \cdot \frac{1}{2}\right) \cdot \left(y \cdot y\right)}{1 \cdot 1}\right)\right) - t\]

12. Applied log-prod 0.4

    \[\leadsto \left(\left(x \cdot \left(2 \cdot \color{blue}{\left(\log \left(\sqrt[3]{\sqrt[3]{y} \cdot \sqrt[3]{y}}\right) + \log \left(\sqrt[3]{\sqrt[3]{y}}\right)\right)}\right) + x \cdot \log \left(\sqrt[3]{y}\right)\right) + \left(z \cdot \left(\log 1 - y \cdot 1\right) - \frac{\left(z \cdot \frac{1}{2}\right) \cdot \left(y \cdot y\right)}{1 \cdot 1}\right)\right) - t\]

13. Applied distribute-lft-in 0.4

    \[\leadsto \left(\left(x \cdot \color{blue}{\left(2 \cdot \log \left(\sqrt[3]{\sqrt[3]{y} \cdot \sqrt[3]{y}}\right) + 2 \cdot \log \left(\sqrt[3]{\sqrt[3]{y}}\right)\right)} + x \cdot \log \left(\sqrt[3]{y}\right)\right) + \left(z \cdot \left(\log 1 - y \cdot 1\right) - \frac{\left(z \cdot \frac{1}{2}\right) \cdot \left(y \cdot y\right)}{1 \cdot 1}\right)\right) - t\]

14. Applied distribute-lft-in 0.4

    \[\leadsto \left(\left(\color{blue}{\left(x \cdot \left(2 \cdot \log \left(\sqrt[3]{\sqrt[3]{y} \cdot \sqrt[3]{y}}\right)\right) + x \cdot \left(2 \cdot \log \left(\sqrt[3]{\sqrt[3]{y}}\right)\right)\right)} + x \cdot \log \left(\sqrt[3]{y}\right)\right) + \left(z \cdot \left(\log 1 - y \cdot 1\right) - \frac{\left(z \cdot \frac{1}{2}\right) \cdot \left(y \cdot y\right)}{1 \cdot 1}\right)\right) - t\]

15. Applied associate-+l+ 0.4

    \[\leadsto \left(\color{blue}{\left(x \cdot \left(2 \cdot \log \left(\sqrt[3]{\sqrt[3]{y} \cdot \sqrt[3]{y}}\right)\right) + \left(x \cdot \left(2 \cdot \log \left(\sqrt[3]{\sqrt[3]{y}}\right)\right) + x \cdot \log \left(\sqrt[3]{y}\right)\right)\right)} + \left(z \cdot \left(\log 1 - y \cdot 1\right) - \frac{\left(z \cdot \frac{1}{2}\right) \cdot \left(y \cdot y\right)}{1 \cdot 1}\right)\right) - t\]

16. Simplified 0.4

    \[\leadsto \left(\left(x \cdot \left(2 \cdot \log \left(\sqrt[3]{\sqrt[3]{y} \cdot \sqrt[3]{y}}\right)\right) + \color{blue}{x \cdot \left(\log \left(\sqrt[3]{\sqrt[3]{y}}\right) \cdot 2 + \log \left(\sqrt[3]{y}\right)\right)}\right) + \left(z \cdot \left(\log 1 - y \cdot 1\right) - \frac{\left(z \cdot \frac{1}{2}\right) \cdot \left(y \cdot y\right)}{1 \cdot 1}\right)\right) - t\]

17. Final simplification 0.4

    \[\leadsto \left(\left(z \cdot \left(\log 1 - 1 \cdot y\right) - \frac{\left(y \cdot y\right) \cdot \left(\frac{1}{2} \cdot z\right)}{1 \cdot 1}\right) + \left(\left(\log \left(\sqrt[3]{\sqrt[3]{y} \cdot \sqrt[3]{y}}\right) \cdot 2\right) \cdot x + \left(\log \left(\sqrt[3]{y}\right) + \log \left(\sqrt[3]{\sqrt[3]{y}}\right) \cdot 2\right) \cdot x\right)\right) - t\]

Reproduce

herbie shell --seed 2019179 
(FPCore (x y z t)
  :name "Numeric.SpecFunctions:invIncompleteBetaWorker from math-functions-0.1.5.2, B"

  :herbie-target
  (- (* (- z) (+ (+ (* 0.5 (* y y)) y) (* (/ 0.3333333333333333 (* 1.0 (* 1.0 1.0))) (* y (* y y))))) (- t (* x (log y))))

  (- (+ (* x (log y)) (* z (log (- 1.0 y)))) t))