Average Error: 0.0 → 0.1
Time: 16.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 r204478 = x;
        double r204479 = y;
        double r204480 = 1.0;
        double r204481 = r204478 * r204479;
        double r204482 = 2.0;
        double r204483 = r204481 / r204482;
        double r204484 = r204480 + r204483;
        double r204485 = r204479 / r204484;
        double r204486 = r204478 - r204485;
        return r204486;
}

double f(double x, double y) {
        double r204487 = x;
        double r204488 = y;
        double r204489 = 1.0;
        double r204490 = 2.0;
        double r204491 = r204487 / r204490;
        double r204492 = 1.0;
        double r204493 = fma(r204491, r204488, r204492);
        double r204494 = r204489 / r204493;
        double r204495 = r204488 * r204494;
        double r204496 = r204487 - r204495;
        return r204496;
}

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 2019199 +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)))))