Average Error: 20.2 → 0.8
Time: 23.4s
Precision: 64
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\frac{\sqrt{\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(\left(\sqrt{x + 1}\right), \left(x + 1\right), \left(x \cdot \sqrt{x}\right)\right)}} \cdot \sqrt{\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(\left(\sqrt{x + 1}\right), \left(x + 1\right), \left(x \cdot \sqrt{x}\right)\right)}}}{\sqrt{x + 1} \cdot \sqrt{x}}\]
\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}
↓
\frac{\sqrt{\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(\left(\sqrt{x + 1}\right), \left(x + 1\right), \left(x \cdot \sqrt{x}\right)\right)}} \cdot \sqrt{\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(\left(\sqrt{x + 1}\right), \left(x + 1\right), \left(x \cdot \sqrt{x}\right)\right)}}}{\sqrt{x + 1} \cdot \sqrt{x}}
double f(double x) {
        double r3211528 = 1.0;
        double r3211529 = x;
        double r3211530 = sqrt(r3211529);
        double r3211531 = r3211528 / r3211530;
        double r3211532 = r3211529 + r3211528;
        double r3211533 = sqrt(r3211532);
        double r3211534 = r3211528 / r3211533;
        double r3211535 = r3211531 - r3211534;
        return r3211535;
}
↓
double f(double x) {
        double r3211536 = x;
        double r3211537 = 1.0;
        double r3211538 = r3211536 + r3211537;
        double r3211539 = sqrt(r3211538);
        double r3211540 = r3211539 * r3211539;
        double r3211541 = sqrt(r3211536);
        double r3211542 = r3211541 * r3211541;
        double r3211543 = r3211539 * r3211541;
        double r3211544 = r3211542 - r3211543;
        double r3211545 = r3211540 + r3211544;
        double r3211546 = r3211536 * r3211541;
        double r3211547 = fma(r3211539, r3211538, r3211546);
        double r3211548 = r3211537 / r3211547;
        double r3211549 = r3211545 * r3211548;
        double r3211550 = sqrt(r3211549);
        double r3211551 = r3211550 * r3211550;
        double r3211552 = r3211551 / r3211543;
        return r3211552;
}

Error

Bits error versus x

Target

Original20.2
Target0.7
Herbie0.8
\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

  1. Initial program 20.2

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

  3. Applied frac-sub20.2

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

  4. Simplified20.2

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

  6. Applied flip--20.1

    \[\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 + \left(x - x\right)}}{\sqrt{x + 1} + \sqrt{x}}}{\sqrt{x} \cdot \sqrt{x + 1}}\]
  8. Using strategy rm

  9. Applied flip3-+0.8

    \[\leadsto \frac{\frac{1 + \left(x - x\right)}{\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 + \left(x - x\right)}{{\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.7

    \[\leadsto \frac{\color{blue}{\frac{1}{\mathsf{fma}\left(\left(\sqrt{x + 1}\right), \left(x + 1\right), \left(\sqrt{x} \cdot x\right)\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. Using strategy rm

  13. Applied add-sqr-sqrt0.8

    \[\leadsto \frac{\color{blue}{\sqrt{\frac{1}{\mathsf{fma}\left(\left(\sqrt{x + 1}\right), \left(x + 1\right), \left(\sqrt{x} \cdot x\right)\right)} \cdot \left(\sqrt{x + 1} \cdot \sqrt{x + 1} + \left(\sqrt{x} \cdot \sqrt{x} - \sqrt{x + 1} \cdot \sqrt{x}\right)\right)} \cdot \sqrt{\frac{1}{\mathsf{fma}\left(\left(\sqrt{x + 1}\right), \left(x + 1\right), \left(\sqrt{x} \cdot x\right)\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}}\]

  14. Final simplification0.8

    \[\leadsto \frac{\sqrt{\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(\left(\sqrt{x + 1}\right), \left(x + 1\right), \left(x \cdot \sqrt{x}\right)\right)}} \cdot \sqrt{\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(\left(\sqrt{x + 1}\right), \left(x + 1\right), \left(x \cdot \sqrt{x}\right)\right)}}}{\sqrt{x + 1} \cdot \sqrt{x}}\]

Reproduce

herbie shell --seed 2019132 +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)))))