Average Error: 19.5 → 0.4
Time: 1.5m
Precision: 64
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\frac{\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{\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 r3980021 = 1.0;
        double r3980022 = x;
        double r3980023 = sqrt(r3980022);
        double r3980024 = r3980021 / r3980023;
        double r3980025 = r3980022 + r3980021;
        double r3980026 = sqrt(r3980025);
        double r3980027 = r3980021 / r3980026;
        double r3980028 = r3980024 - r3980027;
        return r3980028;
}
↓
double f(double x) {
        double r3980029 = 1.0;
        double r3980030 = x;
        double r3980031 = r3980030 + r3980029;
        double r3980032 = cbrt(r3980031);
        double r3980033 = r3980032 * r3980032;
        double r3980034 = sqrt(r3980033);
        double r3980035 = sqrt(r3980032);
        double r3980036 = sqrt(r3980030);
        double r3980037 = fma(r3980034, r3980035, r3980036);
        double r3980038 = r3980029 / r3980037;
        double r3980039 = sqrt(r3980031);
        double r3980040 = r3980036 * r3980039;
        double r3980041 = r3980038 / r3980040;
        return r3980041;
}

Error

Bits error versus x

Target

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

Derivation

  1. Initial program 19.5

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

  9. Applied add-cube-cbrt0.4

    \[\leadsto \frac{\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}}\]

  10. Applied sqrt-prod0.4

    \[\leadsto \frac{\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}}\]

  11. Applied fma-def0.4

    \[\leadsto \frac{\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}}\]

  12. Final simplification0.4

    \[\leadsto \frac{\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 2019142 +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)))))