2isqrt (example 3.6)

Average Error: 19.8 → 0.4

Time: 1.5m

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r6542244 = 1.0;
        double r6542245 = x;
        double r6542246 = sqrt(r6542245);
        double r6542247 = r6542244 / r6542246;
        double r6542248 = r6542245 + r6542244;
        double r6542249 = sqrt(r6542248);
        double r6542250 = r6542244 / r6542249;
        double r6542251 = r6542247 - r6542250;
        return r6542251;
}

↓

double f(double x) {
        double r6542252 = 1.0;
        double r6542253 = x;
        double r6542254 = r6542253 + r6542252;
        double r6542255 = sqrt(r6542254);
        double r6542256 = sqrt(r6542253);
        double r6542257 = r6542255 + r6542256;
        double r6542258 = r6542252 / r6542257;
        double r6542259 = sqrt(r6542258);
        double r6542260 = r6542255 * r6542256;
        double r6542261 = r6542257 * r6542257;
        double r6542262 = r6542252 / r6542261;
        double r6542263 = r6542262 / r6542257;
        double r6542264 = cbrt(r6542263);
        double r6542265 = sqrt(r6542264);
        double r6542266 = r6542260 / r6542265;
        double r6542267 = r6542259 / r6542266;
        return r6542267;
}

Error

Bits error versus x

Target

Original	19.8
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.8

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

3. Applied frac-sub 19.8

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

4. Simplified 19.8

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

6. Applied flip-- 19.6

   \[\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. Simplified 0.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-sqr-sqrt 0.4

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

10. Applied associate-/l* 0.4

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

12. Applied add-cbrt-cube 0.9

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

13. Applied add-cbrt-cube 0.9

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

14. Applied cbrt-undiv 0.9

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

15. Simplified 0.4

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

16. Final simplification 0.4

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

Reproduce

herbie shell --seed 2019149 
(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)))))