Average Error: 19.4 → 0.4
Time: 7.5s
Precision: 64
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\frac{1 \cdot \frac{1}{\mathsf{fma}\left(\sqrt{\sqrt[3]{x + 1} \cdot \sqrt[3]{x + 1}}, \sqrt{\sqrt[3]{x + 1}}, \sqrt{x}\right)}}{\sqrt{x} \cdot \sqrt{x + 1}}\]
\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}
↓
\frac{1 \cdot \frac{1}{\mathsf{fma}\left(\sqrt{\sqrt[3]{x + 1} \cdot \sqrt[3]{x + 1}}, \sqrt{\sqrt[3]{x + 1}}, \sqrt{x}\right)}}{\sqrt{x} \cdot \sqrt{x + 1}}
double f(double x) {
        double r157583 = 1.0;
        double r157584 = x;
        double r157585 = sqrt(r157584);
        double r157586 = r157583 / r157585;
        double r157587 = r157584 + r157583;
        double r157588 = sqrt(r157587);
        double r157589 = r157583 / r157588;
        double r157590 = r157586 - r157589;
        return r157590;
}
↓
double f(double x) {
        double r157591 = 1.0;
        double r157592 = x;
        double r157593 = r157592 + r157591;
        double r157594 = cbrt(r157593);
        double r157595 = r157594 * r157594;
        double r157596 = sqrt(r157595);
        double r157597 = sqrt(r157594);
        double r157598 = sqrt(r157592);
        double r157599 = fma(r157596, r157597, r157598);
        double r157600 = r157591 / r157599;
        double r157601 = r157591 * r157600;
        double r157602 = sqrt(r157593);
        double r157603 = r157598 * r157602;
        double r157604 = r157601 / r157603;
        return r157604;
}

Error

Bits error versus x

Target

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

  6. Applied flip--19.2

    \[\leadsto \frac{1 \cdot \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. Simplified18.8

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

  8. Taylor expanded around 0 0.4

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

  10. Applied add-cube-cbrt0.4

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

  11. Applied sqrt-prod0.4

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

  12. Applied fma-def0.4

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

  13. Final simplification0.4

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

Reproduce

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

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

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