Average Error: 0.0 → 0.0
Time: 11.9s
Precision: 64
\[x - \frac{y}{1 + \frac{x \cdot y}{2}}\]
↓
\[x + \frac{-y}{\mathsf{fma}\left(x, \frac{y}{2}, 1\right)}\]
x - \frac{y}{1 + \frac{x \cdot y}{2}}
↓
x + \frac{-y}{\mathsf{fma}\left(x, \frac{y}{2}, 1\right)}
double f(double x, double y) {
        double r8689945 = x;
        double r8689946 = y;
        double r8689947 = 1.0;
        double r8689948 = r8689945 * r8689946;
        double r8689949 = 2.0;
        double r8689950 = r8689948 / r8689949;
        double r8689951 = r8689947 + r8689950;
        double r8689952 = r8689946 / r8689951;
        double r8689953 = r8689945 - r8689952;
        return r8689953;
}
↓
double f(double x, double y) {
        double r8689954 = x;
        double r8689955 = y;
        double r8689956 = -r8689955;
        double r8689957 = 2.0;
        double r8689958 = r8689955 / r8689957;
        double r8689959 = 1.0;
        double r8689960 = fma(r8689954, r8689958, r8689959);
        double r8689961 = r8689956 / r8689960;
        double r8689962 = r8689954 + r8689961;
        return r8689962;
}

Error

Bits error versus x

Bits error versus y

Derivation

  1. Initial program 0.0

    \[x - \frac{y}{1 + \frac{x \cdot y}{2}}\]

  2. Simplified0.0

    \[\leadsto \color{blue}{x - \frac{y}{\mathsf{fma}\left(x, \frac{y}{2}, 1\right)}}\]
  3. Using strategy rm

  4. Applied clear-num0.1

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

  6. Applied sub-neg0.1

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

  7. Simplified0.0

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

  8. Final simplification0.0

    \[\leadsto x + \frac{-y}{\mathsf{fma}\left(x, \frac{y}{2}, 1\right)}\]

Reproduce

herbie shell --seed 2019179 +o rules:numerics
(FPCore (x y)
  :name "Data.Number.Erf:$cinvnormcdf from erf-2.0.0.0, B"
  (- x (/ y (+ 1.0 (/ (* x y) 2.0)))))