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

Average Error: 19.7 → 0.1

Time: 3.9s

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{\frac{y}{\left(x + y\right) + 1} \cdot \frac{x}{x + y}}{x + y}\]

C

double f(double x, double y) {
        double r510481 = x;
        double r510482 = y;
        double r510483 = r510481 * r510482;
        double r510484 = r510481 + r510482;
        double r510485 = r510484 * r510484;
        double r510486 = 1.0;
        double r510487 = r510484 + r510486;
        double r510488 = r510485 * r510487;
        double r510489 = r510483 / r510488;
        return r510489;
}

↓

double f(double x, double y) {
        double r510490 = y;
        double r510491 = x;
        double r510492 = r510491 + r510490;
        double r510493 = 1.0;
        double r510494 = r510492 + r510493;
        double r510495 = r510490 / r510494;
        double r510496 = r510491 / r510492;
        double r510497 = r510495 * r510496;
        double r510498 = r510497 / r510492;
        return r510498;
}

Error

Bits error versus x

Bits error versus y

Target

Original	19.7
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.7

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

   \[\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 associate-/r* 0.2

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

7. Applied add-sqr-sqrt 33.1

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

8. Applied add-sqr-sqrt 33.2

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

9. Applied *-un-lft-identity 33.2

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

10. Applied times-frac 33.2

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

11. Applied times-frac 33.2

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

12. Simplified 33.1

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

13. Simplified 0.2

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

15. Applied associate-*r/ 0.2

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

16. Applied associate-*l/ 0.2

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

17. Simplified 0.1

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

18. Final simplification 0.1

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

Reproduce

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