2isqrt (example 3.6)

Average Error: 19.9 → 0.4

Time: 15.0s

Precision: 64

Math

\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]

↓

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

C

double f(double x) {
        double r137046 = 1.0;
        double r137047 = x;
        double r137048 = sqrt(r137047);
        double r137049 = r137046 / r137048;
        double r137050 = r137047 + r137046;
        double r137051 = sqrt(r137050);
        double r137052 = r137046 / r137051;
        double r137053 = r137049 - r137052;
        return r137053;
}

↓

double f(double x) {
        double r137054 = 1.0;
        double r137055 = x;
        double r137056 = cbrt(r137055);
        double r137057 = r137056 * r137056;
        double r137058 = sqrt(r137057);
        double r137059 = sqrt(r137056);
        double r137060 = r137055 + r137054;
        double r137061 = sqrt(r137060);
        double r137062 = fma(r137058, r137059, r137061);
        double r137063 = r137054 * r137062;
        double r137064 = r137054 / r137063;
        double r137065 = sqrt(r137055);
        double r137066 = r137065 * r137061;
        double r137067 = r137064 / r137066;
        return r137067;
}

Error

Bits error versus x

Target

Original	19.9
Target	0.7
Herbie	0.4

\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

1. Initial program 19.9

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

3. Applied frac-sub 19.9

   \[\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.7

   \[\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. Simplified 19.3

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

7. Simplified 19.3

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

8. Taylor expanded around 0 0.4

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

10. Applied add-cube-cbrt 0.4

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

11. Applied sqrt-prod 0.4

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

12. Applied fma-def 0.4

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

13. Final simplification 0.4

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

Reproduce

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