Average Error: 19.8 → 5.1
Time: 23.3s
Precision: 64
\[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}\]
↓
\[\begin{array}{l} \mathbf{if}\;y \le -1.3656303004097706 \cdot 10^{+154}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \le -7.522985421753554 \cdot 10^{-157}:\\ \;\;\;\;\left(\frac{x}{\sqrt{x \cdot x + y \cdot y}} - \sqrt{\frac{y \cdot y}{x \cdot x + y \cdot y}}\right) \cdot \left(\sqrt{\frac{y \cdot y}{x \cdot x + y \cdot y}} + \frac{x}{\sqrt{x \cdot x + y \cdot y}}\right)\\ \mathbf{elif}\;y \le 1.9144746578538855 \cdot 10^{-162}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\frac{x \cdot x + y \cdot y}{x \cdot x}} - \frac{y \cdot y}{x \cdot x + y \cdot y}\\ \end{array}\]
\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}
↓
\begin{array}{l}
\mathbf{if}\;y \le -1.3656303004097706 \cdot 10^{+154}:\\
\;\;\;\;-1\\

\mathbf{elif}\;y \le -7.522985421753554 \cdot 10^{-157}:\\
\;\;\;\;\left(\frac{x}{\sqrt{x \cdot x + y \cdot y}} - \sqrt{\frac{y \cdot y}{x \cdot x + y \cdot y}}\right) \cdot \left(\sqrt{\frac{y \cdot y}{x \cdot x + y \cdot y}} + \frac{x}{\sqrt{x \cdot x + y \cdot y}}\right)\\

\mathbf{elif}\;y \le 1.9144746578538855 \cdot 10^{-162}:\\
\;\;\;\;1\\

\mathbf{else}:\\
\;\;\;\;\frac{1}{\frac{x \cdot x + y \cdot y}{x \cdot x}} - \frac{y \cdot y}{x \cdot x + y \cdot y}\\

\end{array}
double f(double x, double y) {
        double r4099284 = x;
        double r4099285 = y;
        double r4099286 = r4099284 - r4099285;
        double r4099287 = r4099284 + r4099285;
        double r4099288 = r4099286 * r4099287;
        double r4099289 = r4099284 * r4099284;
        double r4099290 = r4099285 * r4099285;
        double r4099291 = r4099289 + r4099290;
        double r4099292 = r4099288 / r4099291;
        return r4099292;
}
↓
double f(double x, double y) {
        double r4099293 = y;
        double r4099294 = -1.3656303004097706e+154;
        bool r4099295 = r4099293 <= r4099294;
        double r4099296 = -1.0;
        double r4099297 = -7.522985421753554e-157;
        bool r4099298 = r4099293 <= r4099297;
        double r4099299 = x;
        double r4099300 = r4099299 * r4099299;
        double r4099301 = r4099293 * r4099293;
        double r4099302 = r4099300 + r4099301;
        double r4099303 = sqrt(r4099302);
        double r4099304 = r4099299 / r4099303;
        double r4099305 = r4099301 / r4099302;
        double r4099306 = sqrt(r4099305);
        double r4099307 = r4099304 - r4099306;
        double r4099308 = r4099306 + r4099304;
        double r4099309 = r4099307 * r4099308;
        double r4099310 = 1.9144746578538855e-162;
        bool r4099311 = r4099293 <= r4099310;
        double r4099312 = 1.0;
        double r4099313 = r4099302 / r4099300;
        double r4099314 = r4099312 / r4099313;
        double r4099315 = r4099314 - r4099305;
        double r4099316 = r4099311 ? r4099312 : r4099315;
        double r4099317 = r4099298 ? r4099309 : r4099316;
        double r4099318 = r4099295 ? r4099296 : r4099317;
        return r4099318;
}

Error

Bits error versus x

Bits error versus y

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original19.8
Target0.0
Herbie5.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. Split input into 4 regimes

  2. if y < -1.3656303004097706e+154

    1. Initial program 63.6

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

    2. Simplified63.6

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

    3. Taylor expanded around 0 0

      \[\leadsto \color{blue}{-1}\]

    if -1.3656303004097706e+154 < y < -7.522985421753554e-157

    1. Initial program 0.0

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

    2. Simplified0.0

      \[\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-sqrt0.0

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

    5. Applied add-sqr-sqrt0.0

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

    6. Applied times-frac0.0

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

    7. Applied difference-of-squares0.0

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

    if -7.522985421753554e-157 < y < 1.9144746578538855e-162

    1. Initial program 28.2

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

    2. Simplified28.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 clear-num28.2

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

    5. Taylor expanded around -inf 16.1

      \[\leadsto \color{blue}{1}\]

    if 1.9144746578538855e-162 < y

    1. Initial program 0.1

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

    2. Simplified0.1

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

      \[\leadsto \color{blue}{\frac{1}{\frac{x \cdot x + y \cdot y}{x \cdot x}}} - \frac{y \cdot y}{x \cdot x + y \cdot y}\]
  3. Recombined 4 regimes into one program.

  4. Final simplification5.1

    \[\leadsto \begin{array}{l} \mathbf{if}\;y \le -1.3656303004097706 \cdot 10^{+154}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \le -7.522985421753554 \cdot 10^{-157}:\\ \;\;\;\;\left(\frac{x}{\sqrt{x \cdot x + y \cdot y}} - \sqrt{\frac{y \cdot y}{x \cdot x + y \cdot y}}\right) \cdot \left(\sqrt{\frac{y \cdot y}{x \cdot x + y \cdot y}} + \frac{x}{\sqrt{x \cdot x + y \cdot y}}\right)\\ \mathbf{elif}\;y \le 1.9144746578538855 \cdot 10^{-162}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\frac{x \cdot x + y \cdot y}{x \cdot x}} - \frac{y \cdot y}{x \cdot x + y \cdot y}\\ \end{array}\]

Reproduce

herbie shell --seed 2019144 
(FPCore (x y)
  :name "Kahan p9 Example"
  :pre (and (< 0 x 1) (< y 1))

  :herbie-target
  (if (< 0.5 (fabs (/ x y)) 2) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- 1 (/ 2 (+ 1 (* (/ x y) (/ x y))))))

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