Average Error: 20.2 → 20.1
Time: 13.4s
Precision: 64
\[0.0 \lt x \lt 1 \land y \lt 1\]
\[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]
↓
\[\frac{x \cdot x}{x \cdot x + y \cdot y} - \frac{y}{\sqrt{x \cdot x + y \cdot y}} \cdot \frac{y}{\sqrt{x \cdot x + y \cdot y}}\]
\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}
↓
\frac{x \cdot x}{x \cdot x + y \cdot y} - \frac{y}{\sqrt{x \cdot x + y \cdot y}} \cdot \frac{y}{\sqrt{x \cdot x + y \cdot y}}
double f(double x, double y) {
        double r4551418 = x;
        double r4551419 = y;
        double r4551420 = r4551418 - r4551419;
        double r4551421 = r4551418 + r4551419;
        double r4551422 = r4551420 * r4551421;
        double r4551423 = r4551418 * r4551418;
        double r4551424 = r4551419 * r4551419;
        double r4551425 = r4551423 + r4551424;
        double r4551426 = r4551422 / r4551425;
        return r4551426;
}
↓
double f(double x, double y) {
        double r4551427 = x;
        double r4551428 = r4551427 * r4551427;
        double r4551429 = y;
        double r4551430 = r4551429 * r4551429;
        double r4551431 = r4551428 + r4551430;
        double r4551432 = r4551428 / r4551431;
        double r4551433 = sqrt(r4551431);
        double r4551434 = r4551429 / r4551433;
        double r4551435 = r4551434 * r4551434;
        double r4551436 = r4551432 - r4551435;
        return r4551436;
}

Error

Bits error versus x

Bits error versus y

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original20.2
Target0.1
Herbie20.1
\[\begin{array}{l} \mathbf{if}\;0.5 \lt \left|\frac{x}{y}\right| \lt 2:\\ \;\;\;\;\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\\ \mathbf{else}:\\ \;\;\;\;1 - \frac{2}{1 + \frac{x}{y} \cdot \frac{x}{y}}\\ \end{array}\]

Derivation

  1. Initial program 20.2

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

  2. Simplified20.2

    \[\leadsto \color{blue}{\frac{x \cdot x}{x \cdot x + y \cdot y} - \frac{y \cdot y}{x \cdot x + y \cdot y}}\]
  3. Using strategy rm

  4. Applied add-sqr-sqrt20.2

    \[\leadsto \frac{x \cdot x}{x \cdot x + y \cdot y} - \frac{y \cdot y}{\color{blue}{\sqrt{x \cdot x + y \cdot y} \cdot \sqrt{x \cdot x + y \cdot y}}}\]

  5. Applied times-frac20.1

    \[\leadsto \frac{x \cdot x}{x \cdot x + y \cdot y} - \color{blue}{\frac{y}{\sqrt{x \cdot x + y \cdot y}} \cdot \frac{y}{\sqrt{x \cdot x + y \cdot y}}}\]

  6. Final simplification20.1

    \[\leadsto \frac{x \cdot x}{x \cdot x + y \cdot y} - \frac{y}{\sqrt{x \cdot x + y \cdot y}} \cdot \frac{y}{\sqrt{x \cdot x + y \cdot y}}\]

Reproduce

herbie shell --seed 2019171 
(FPCore (x y)
  :name "Kahan p9 Example"
  :pre (and (< 0.0 x 1.0) (< y 1.0))

  :herbie-target
  (if (< 0.5 (fabs (/ x y)) 2.0) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- 1.0 (/ 2.0 (+ 1.0 (* (/ x y) (/ x y))))))

  (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))))