2isqrt (example 3.6)

Average Error: 19.7 → 0.4

Time: 20.0s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r4101413 = 1.0;
        double r4101414 = x;
        double r4101415 = sqrt(r4101414);
        double r4101416 = r4101413 / r4101415;
        double r4101417 = r4101414 + r4101413;
        double r4101418 = sqrt(r4101417);
        double r4101419 = r4101413 / r4101418;
        double r4101420 = r4101416 - r4101419;
        return r4101420;
}

↓

double f(double x) {
        double r4101421 = 1.0;
        double r4101422 = x;
        double r4101423 = r4101421 / r4101422;
        double r4101424 = sqrt(r4101422);
        double r4101425 = r4101421 / r4101424;
        double r4101426 = r4101422 + r4101421;
        double r4101427 = sqrt(r4101426);
        double r4101428 = r4101421 / r4101427;
        double r4101429 = r4101425 + r4101428;
        double r4101430 = r4101429 * r4101426;
        double r4101431 = r4101421 / r4101430;
        double r4101432 = r4101423 * r4101431;
        return r4101432;
}

Error

Bits error versus x

Target

Original	19.7
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.7

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

3. Applied flip-- 19.7

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

5. Applied frac-times 24.6

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

6. Applied frac-times 19.8

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

7. Applied frac-sub 19.6

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

8. Simplified 19.2

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

9. Simplified 19.1

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

10. Taylor expanded around inf 5.4

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

12. Applied *-un-lft-identity 5.4

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

13. Applied sqrt-prod 5.4

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

14. Applied *-un-lft-identity 5.4

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

15. Applied times-frac 5.4

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

16. Applied *-un-lft-identity 5.4

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

17. Applied sqrt-prod 5.4

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

18. Applied *-un-lft-identity 5.4

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

19. Applied times-frac 5.4

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

20. Applied distribute-lft-out 5.4

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

21. Applied add-cube-cbrt 5.4

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

22. Applied times-frac 5.1

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

23. Applied times-frac 0.5

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

24. Simplified 0.5

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

25. Simplified 0.4

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

26. Final simplification 0.4

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

Reproduce

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