Average Error: 19.4 → 0.6
Time: 26.7s
Precision: 64
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\frac{\left(\sqrt{x + 1} \cdot \sqrt{x + 1} + \left(\sqrt{x} \cdot \sqrt{x} - \sqrt{x + 1} \cdot \sqrt{x}\right)\right) \cdot \frac{1}{\mathsf{fma}\left(\sqrt{x}, x, \left(x + 1\right) \cdot \sqrt{x + 1}\right)}}{\sqrt{x + 1} \cdot \sqrt{x}}\]
\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}
↓
\frac{\left(\sqrt{x + 1} \cdot \sqrt{x + 1} + \left(\sqrt{x} \cdot \sqrt{x} - \sqrt{x + 1} \cdot \sqrt{x}\right)\right) \cdot \frac{1}{\mathsf{fma}\left(\sqrt{x}, x, \left(x + 1\right) \cdot \sqrt{x + 1}\right)}}{\sqrt{x + 1} \cdot \sqrt{x}}
double f(double x) {
        double r6655646 = 1.0;
        double r6655647 = x;
        double r6655648 = sqrt(r6655647);
        double r6655649 = r6655646 / r6655648;
        double r6655650 = r6655647 + r6655646;
        double r6655651 = sqrt(r6655650);
        double r6655652 = r6655646 / r6655651;
        double r6655653 = r6655649 - r6655652;
        return r6655653;
}
↓
double f(double x) {
        double r6655654 = x;
        double r6655655 = 1.0;
        double r6655656 = r6655654 + r6655655;
        double r6655657 = sqrt(r6655656);
        double r6655658 = r6655657 * r6655657;
        double r6655659 = sqrt(r6655654);
        double r6655660 = r6655659 * r6655659;
        double r6655661 = r6655657 * r6655659;
        double r6655662 = r6655660 - r6655661;
        double r6655663 = r6655658 + r6655662;
        double r6655664 = r6655656 * r6655657;
        double r6655665 = fma(r6655659, r6655654, r6655664);
        double r6655666 = r6655655 / r6655665;
        double r6655667 = r6655663 * r6655666;
        double r6655668 = r6655667 / r6655661;
        return r6655668;
}

Error

Bits error versus x

Target

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

Derivation

  1. Initial program 19.4

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

  3. Applied frac-sub19.4

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

  4. Simplified19.4

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

  6. Applied flip--19.2

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

  7. Simplified0.4

    \[\leadsto \frac{\frac{\color{blue}{1 + 0}}{\sqrt{x + 1} + \sqrt{x}}}{\sqrt{x} \cdot \sqrt{x + 1}}\]
  8. Using strategy rm

  9. Applied flip3-+0.8

    \[\leadsto \frac{\frac{1 + 0}{\color{blue}{\frac{{\left(\sqrt{x + 1}\right)}^{3} + {\left(\sqrt{x}\right)}^{3}}{\sqrt{x + 1} \cdot \sqrt{x + 1} + \left(\sqrt{x} \cdot \sqrt{x} - \sqrt{x + 1} \cdot \sqrt{x}\right)}}}}{\sqrt{x} \cdot \sqrt{x + 1}}\]

  10. Applied associate-/r/0.8

    \[\leadsto \frac{\color{blue}{\frac{1 + 0}{{\left(\sqrt{x + 1}\right)}^{3} + {\left(\sqrt{x}\right)}^{3}} \cdot \left(\sqrt{x + 1} \cdot \sqrt{x + 1} + \left(\sqrt{x} \cdot \sqrt{x} - \sqrt{x + 1} \cdot \sqrt{x}\right)\right)}}{\sqrt{x} \cdot \sqrt{x + 1}}\]

  11. Simplified0.6

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

  12. Final simplification0.6

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

Reproduce

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

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

  (- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))