Average Error: 0.0 → 0.1
Time: 13.9s
Precision: 64
\[x - \frac{y}{1 + \frac{x \cdot y}{2}}\]
↓
\[x - y \cdot \frac{1}{\mathsf{fma}\left(\frac{x}{2}, y, 1\right)}\]
x - \frac{y}{1 + \frac{x \cdot y}{2}}
↓
x - y \cdot \frac{1}{\mathsf{fma}\left(\frac{x}{2}, y, 1\right)}
double f(double x, double y) {
        double r138405 = x;
        double r138406 = y;
        double r138407 = 1.0;
        double r138408 = r138405 * r138406;
        double r138409 = 2.0;
        double r138410 = r138408 / r138409;
        double r138411 = r138407 + r138410;
        double r138412 = r138406 / r138411;
        double r138413 = r138405 - r138412;
        return r138413;
}
↓
double f(double x, double y) {
        double r138414 = x;
        double r138415 = y;
        double r138416 = 1.0;
        double r138417 = 2.0;
        double r138418 = r138414 / r138417;
        double r138419 = 1.0;
        double r138420 = fma(r138418, r138415, r138419);
        double r138421 = r138416 / r138420;
        double r138422 = r138415 * r138421;
        double r138423 = r138414 - r138422;
        return r138423;
}

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. Using strategy rm

  3. Applied div-inv0.1

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

  4. Simplified0.1

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

  5. Final simplification0.1

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

Reproduce

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