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

Average Error: 9.2 → 0.4

Time: 13.5s

Precision: 64

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

Math

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

↓

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

C

double f(double x, double y, double z, double t) {
        double r385650 = x;
        double r385651 = y;
        double r385652 = log(r385651);
        double r385653 = r385650 * r385652;
        double r385654 = z;
        double r385655 = 1.0;
        double r385656 = r385655 - r385651;
        double r385657 = log(r385656);
        double r385658 = r385654 * r385657;
        double r385659 = r385653 + r385658;
        double r385660 = t;
        double r385661 = r385659 - r385660;
        return r385661;
}

↓

double f(double x, double y, double z, double t) {
        double r385662 = x;
        double r385663 = 2.0;
        double r385664 = y;
        double r385665 = cbrt(r385664);
        double r385666 = log(r385665);
        double r385667 = r385663 * r385666;
        double r385668 = r385662 * r385667;
        double r385669 = 0.6666666666666666;
        double r385670 = pow(r385664, r385669);
        double r385671 = pow(r385670, r385669);
        double r385672 = cbrt(r385670);
        double r385673 = r385671 * r385672;
        double r385674 = cbrt(r385673);
        double r385675 = log(r385674);
        double r385676 = r385662 * r385675;
        double r385677 = cbrt(r385665);
        double r385678 = log(r385677);
        double r385679 = r385678 * r385662;
        double r385680 = r385676 + r385679;
        double r385681 = r385668 + r385680;
        double r385682 = z;
        double r385683 = 1.0;
        double r385684 = log(r385683);
        double r385685 = r385683 * r385664;
        double r385686 = r385684 - r385685;
        double r385687 = r385682 * r385686;
        double r385688 = 0.5;
        double r385689 = pow(r385664, r385663);
        double r385690 = r385682 * r385689;
        double r385691 = pow(r385683, r385663);
        double r385692 = r385690 / r385691;
        double r385693 = r385688 * r385692;
        double r385694 = r385687 - r385693;
        double r385695 = r385681 + r385694;
        double r385696 = t;
        double r385697 = r385695 - r385696;
        return r385697;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	9.2
Target	0.3
Herbie	0.4

\[\left(-z\right) \cdot \left(\left(0.5 \cdot \left(y \cdot y\right) + y\right) + \frac{0.333333333333333315}{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.2

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

2. Taylor expanded around 0 0.3

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

3. Simplified 0.3

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

5. Applied add-cube-cbrt 0.3

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

11. Applied cbrt-prod 0.4

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

12. Applied log-prod 0.4

    \[\leadsto \left(\left(x \cdot \left(2 \cdot \log \left(\sqrt[3]{y}\right)\right) + x \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) + \left(z \cdot \left(\log 1 - 1 \cdot y\right) - \frac{1}{2} \cdot \frac{z \cdot {y}^{2}}{{1}^{2}}\right)\right) - t\]

13. Applied distribute-lft-in 0.3

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

14. Simplified 0.3

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

15. Simplified 0.3

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

17. Applied add-cube-cbrt 0.3

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

18. Simplified 0.4

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

19. Final simplification 0.4

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

Reproduce

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

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

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