Average Error: 20.1 → 0.4
Time: 24.6s
Precision: 64
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
\[\frac{\frac{1}{\sqrt{x} \cdot \mathsf{fma}\left(1, \sqrt{x + 1}, \sqrt{x} \cdot 1\right)}}{\sqrt{x + 1}}\]
\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}
\frac{\frac{1}{\sqrt{x} \cdot \mathsf{fma}\left(1, \sqrt{x + 1}, \sqrt{x} \cdot 1\right)}}{\sqrt{x + 1}}
double f(double x) {
        double r16960608 = 1.0;
        double r16960609 = x;
        double r16960610 = sqrt(r16960609);
        double r16960611 = r16960608 / r16960610;
        double r16960612 = r16960609 + r16960608;
        double r16960613 = sqrt(r16960612);
        double r16960614 = r16960608 / r16960613;
        double r16960615 = r16960611 - r16960614;
        return r16960615;
}

double f(double x) {
        double r16960616 = 1.0;
        double r16960617 = x;
        double r16960618 = sqrt(r16960617);
        double r16960619 = r16960617 + r16960616;
        double r16960620 = sqrt(r16960619);
        double r16960621 = r16960618 * r16960616;
        double r16960622 = fma(r16960616, r16960620, r16960621);
        double r16960623 = r16960618 * r16960622;
        double r16960624 = r16960616 / r16960623;
        double r16960625 = r16960624 / r16960620;
        return r16960625;
}

Error

Bits error versus x

Target

Original20.1
Target0.6
Herbie0.4
\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

  1. Initial program 20.1

    \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
  2. Using strategy rm
  3. Applied frac-sub20.1

    \[\leadsto \color{blue}{\frac{1 \cdot \sqrt{x + 1} - \sqrt{x} \cdot 1}{\sqrt{x} \cdot \sqrt{x + 1}}}\]
  4. Using strategy rm
  5. Applied flip--19.9

    \[\leadsto \frac{\color{blue}{\frac{\left(1 \cdot \sqrt{x + 1}\right) \cdot \left(1 \cdot \sqrt{x + 1}\right) - \left(\sqrt{x} \cdot 1\right) \cdot \left(\sqrt{x} \cdot 1\right)}{1 \cdot \sqrt{x + 1} + \sqrt{x} \cdot 1}}}{\sqrt{x} \cdot \sqrt{x + 1}}\]
  6. Taylor expanded around 0 0.4

    \[\leadsto \frac{\frac{\color{blue}{1}}{1 \cdot \sqrt{x + 1} + \sqrt{x} \cdot 1}}{\sqrt{x} \cdot \sqrt{x + 1}}\]
  7. Using strategy rm
  8. Applied associate-/r*0.4

    \[\leadsto \color{blue}{\frac{\frac{\frac{1}{1 \cdot \sqrt{x + 1} + \sqrt{x} \cdot 1}}{\sqrt{x}}}{\sqrt{x + 1}}}\]
  9. Simplified0.4

    \[\leadsto \frac{\color{blue}{\frac{1}{\sqrt{x} \cdot \mathsf{fma}\left(1, \sqrt{x + 1}, \sqrt{x} \cdot 1\right)}}}{\sqrt{x + 1}}\]
  10. Final simplification0.4

    \[\leadsto \frac{\frac{1}{\sqrt{x} \cdot \mathsf{fma}\left(1, \sqrt{x + 1}, \sqrt{x} \cdot 1\right)}}{\sqrt{x + 1}}\]

Reproduce

herbie shell --seed 2019173 +o rules:numerics
(FPCore (x)
  :name "2isqrt (example 3.6)"

  :herbie-target
  (/ 1.0 (+ (* (+ x 1.0) (sqrt x)) (* x (sqrt (+ x 1.0)))))

  (- (/ 1.0 (sqrt x)) (/ 1.0 (sqrt (+ x 1.0)))))