Average Error: 0.0 → 5.4
Time: 7.6s
Precision: 64
\[x - \frac{y}{1 + \frac{x \cdot y}{2}}\]
↓
\[\begin{array}{l} \mathbf{if}\;y \le -1.0316187449465748 \cdot 10^{92} \lor \neg \left(y \le 1.21058365266928917 \cdot 10^{131}\right):\\ \;\;\;\;\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{2}{x}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{\left(-x \cdot y\right) \cdot y}{2 \cdot \left(1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}\right)}\\ \end{array}\]
x - \frac{y}{1 + \frac{x \cdot y}{2}}
↓
\begin{array}{l}
\mathbf{if}\;y \le -1.0316187449465748 \cdot 10^{92} \lor \neg \left(y \le 1.21058365266928917 \cdot 10^{131}\right):\\
\;\;\;\;\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{2}{x}\\

\mathbf{else}:\\
\;\;\;\;\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{\left(-x \cdot y\right) \cdot y}{2 \cdot \left(1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}\right)}\\

\end{array}
double f(double x, double y) {
        double r233423 = x;
        double r233424 = y;
        double r233425 = 1.0;
        double r233426 = r233423 * r233424;
        double r233427 = 2.0;
        double r233428 = r233426 / r233427;
        double r233429 = r233425 + r233428;
        double r233430 = r233424 / r233429;
        double r233431 = r233423 - r233430;
        return r233431;
}
↓
double f(double x, double y) {
        double r233432 = y;
        double r233433 = -1.0316187449465748e+92;
        bool r233434 = r233432 <= r233433;
        double r233435 = 1.2105836526692892e+131;
        bool r233436 = r233432 <= r233435;
        double r233437 = !r233436;
        bool r233438 = r233434 || r233437;
        double r233439 = x;
        double r233440 = 1.0;
        double r233441 = r233440 * r233440;
        double r233442 = r233439 * r233432;
        double r233443 = 2.0;
        double r233444 = r233442 / r233443;
        double r233445 = r233444 * r233444;
        double r233446 = r233441 - r233445;
        double r233447 = r233432 / r233446;
        double r233448 = r233447 * r233440;
        double r233449 = r233439 - r233448;
        double r233450 = r233443 / r233439;
        double r233451 = r233449 - r233450;
        double r233452 = -r233442;
        double r233453 = r233452 * r233432;
        double r233454 = r233443 * r233446;
        double r233455 = r233453 / r233454;
        double r233456 = r233449 - r233455;
        double r233457 = r233438 ? r233451 : r233456;
        return r233457;
}

Error

Bits error versus x

Bits error versus y

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Split input into 2 regimes

  2. if y < -1.0316187449465748e+92 or 1.2105836526692892e+131 < y

    1. Initial program 0.1

      \[x - \frac{y}{1 + \frac{x \cdot y}{2}}\]
    2. Using strategy rm

    3. Applied flip-+27.4

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

    4. Applied associate-/r/27.5

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

    6. Applied sub-neg27.5

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

    7. Applied distribute-rgt-in27.4

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

    8. Applied associate--r+27.4

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

    9. Simplified27.4

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

    10. Taylor expanded around inf 10.4

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

    if -1.0316187449465748e+92 < y < 1.2105836526692892e+131

    1. Initial program 0.0

      \[x - \frac{y}{1 + \frac{x \cdot y}{2}}\]
    2. Using strategy rm

    3. Applied flip-+1.8

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

    4. Applied associate-/r/1.8

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

    6. Applied sub-neg1.8

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

    7. Applied distribute-rgt-in1.8

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

    8. Applied associate--r+1.8

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

    9. Simplified1.8

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

    11. Applied distribute-neg-frac1.8

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

    12. Applied frac-times3.2

      \[\leadsto \left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \color{blue}{\frac{\left(-x \cdot y\right) \cdot y}{2 \cdot \left(1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}\right)}}\]
  3. Recombined 2 regimes into one program.

  4. Final simplification5.4

    \[\leadsto \begin{array}{l} \mathbf{if}\;y \le -1.0316187449465748 \cdot 10^{92} \lor \neg \left(y \le 1.21058365266928917 \cdot 10^{131}\right):\\ \;\;\;\;\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{2}{x}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}} \cdot 1\right) - \frac{\left(-x \cdot y\right) \cdot y}{2 \cdot \left(1 \cdot 1 - \frac{x \cdot y}{2} \cdot \frac{x \cdot y}{2}\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2020045 
(FPCore (x y)
  :name "Data.Number.Erf:$cinvnormcdf from erf-2.0.0.0, B"
  :precision binary64
  (- x (/ y (+ 1 (/ (* x y) 2)))))