Numeric.SpecFunctions:incompleteBetaApprox from math-functions-0.1.5.2, A

Average Error: 19.8 → 0.1

Time: 4.4s

Precision: 64

Math

\[\frac{x \cdot y}{\left(\left(x + y\right) \cdot \left(x + y\right)\right) \cdot \left(\left(x + y\right) + 1\right)}\]

↓

\[\frac{x \cdot \frac{\frac{y}{\left(x + y\right) + 1}}{x + y}}{x + y} \cdot \sqrt{1}\]

C

double f(double x, double y) {
        double r436725 = x;
        double r436726 = y;
        double r436727 = r436725 * r436726;
        double r436728 = r436725 + r436726;
        double r436729 = r436728 * r436728;
        double r436730 = 1.0;
        double r436731 = r436728 + r436730;
        double r436732 = r436729 * r436731;
        double r436733 = r436727 / r436732;
        return r436733;
}

↓

double f(double x, double y) {
        double r436734 = x;
        double r436735 = y;
        double r436736 = r436734 + r436735;
        double r436737 = 1.0;
        double r436738 = r436736 + r436737;
        double r436739 = r436735 / r436738;
        double r436740 = r436739 / r436736;
        double r436741 = r436734 * r436740;
        double r436742 = r436741 / r436736;
        double r436743 = 1.0;
        double r436744 = sqrt(r436743);
        double r436745 = r436742 * r436744;
        return r436745;
}

Error

Bits error versus x

Bits error versus y

Target

Original	19.8
Target	0.1
Herbie	0.1

\[\frac{\frac{\frac{x}{\left(y + 1\right) + x}}{y + x}}{\frac{1}{\frac{y}{y + x}}}\]

Derivation

1. Initial program 19.8

   \[\frac{x \cdot y}{\left(\left(x + y\right) \cdot \left(x + y\right)\right) \cdot \left(\left(x + y\right) + 1\right)}\]
2. Using strategy rm

3. Applied times-frac 8.0

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

5. Applied *-un-lft-identity 8.0

   \[\leadsto \frac{\color{blue}{1 \cdot x}}{\left(x + y\right) \cdot \left(x + y\right)} \cdot \frac{y}{\left(x + y\right) + 1}\]

6. Applied times-frac 0.2

   \[\leadsto \color{blue}{\left(\frac{1}{x + y} \cdot \frac{x}{x + y}\right)} \cdot \frac{y}{\left(x + y\right) + 1}\]

7. Applied associate-*l* 0.2

   \[\leadsto \color{blue}{\frac{1}{x + y} \cdot \left(\frac{x}{x + y} \cdot \frac{y}{\left(x + y\right) + 1}\right)}\]
8. Using strategy rm

9. Applied *-un-lft-identity 0.2

   \[\leadsto \frac{1}{\color{blue}{1 \cdot \left(x + y\right)}} \cdot \left(\frac{x}{x + y} \cdot \frac{y}{\left(x + y\right) + 1}\right)\]

10. Applied add-sqr-sqrt 0.2

    \[\leadsto \frac{\color{blue}{\sqrt{1} \cdot \sqrt{1}}}{1 \cdot \left(x + y\right)} \cdot \left(\frac{x}{x + y} \cdot \frac{y}{\left(x + y\right) + 1}\right)\]

11. Applied times-frac 0.2

    \[\leadsto \color{blue}{\left(\frac{\sqrt{1}}{1} \cdot \frac{\sqrt{1}}{x + y}\right)} \cdot \left(\frac{x}{x + y} \cdot \frac{y}{\left(x + y\right) + 1}\right)\]

12. Applied associate-*l* 0.2

    \[\leadsto \color{blue}{\frac{\sqrt{1}}{1} \cdot \left(\frac{\sqrt{1}}{x + y} \cdot \left(\frac{x}{x + y} \cdot \frac{y}{\left(x + y\right) + 1}\right)\right)}\]

13. Simplified 0.1

    \[\leadsto \frac{\sqrt{1}}{1} \cdot \color{blue}{\frac{\frac{x}{x + y} \cdot \frac{y}{\left(x + y\right) + 1}}{x + y}}\]
14. Using strategy rm

15. Applied div-inv 0.2

    \[\leadsto \frac{\sqrt{1}}{1} \cdot \frac{\color{blue}{\left(x \cdot \frac{1}{x + y}\right)} \cdot \frac{y}{\left(x + y\right) + 1}}{x + y}\]

16. Applied associate-*l* 0.2

    \[\leadsto \frac{\sqrt{1}}{1} \cdot \frac{\color{blue}{x \cdot \left(\frac{1}{x + y} \cdot \frac{y}{\left(x + y\right) + 1}\right)}}{x + y}\]

17. Simplified 0.1

    \[\leadsto \frac{\sqrt{1}}{1} \cdot \frac{x \cdot \color{blue}{\frac{\frac{y}{\left(x + y\right) + 1}}{x + y}}}{x + y}\]

18. Final simplification 0.1

    \[\leadsto \frac{x \cdot \frac{\frac{y}{\left(x + y\right) + 1}}{x + y}}{x + y} \cdot \sqrt{1}\]

Reproduce

herbie shell --seed 2020024 +o rules:numerics
(FPCore (x y)
  :name "Numeric.SpecFunctions:incompleteBetaApprox from math-functions-0.1.5.2, A"
  :precision binary64

  :herbie-target
  (/ (/ (/ x (+ (+ y 1) x)) (+ y x)) (/ 1 (/ y (+ y x))))

  (/ (* x y) (* (* (+ x y) (+ x y)) (+ (+ x y) 1))))