2isqrt (example 3.6)

Average Error: 20.1 → 0.2

Time: 16.8s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r2865624 = 1.0;
        double r2865625 = x;
        double r2865626 = sqrt(r2865625);
        double r2865627 = r2865624 / r2865626;
        double r2865628 = r2865625 + r2865624;
        double r2865629 = sqrt(r2865628);
        double r2865630 = r2865624 / r2865629;
        double r2865631 = r2865627 - r2865630;
        return r2865631;
}

↓

double f(double x) {
        double r2865632 = x;
        double r2865633 = -0.5;
        double r2865634 = pow(r2865632, r2865633);
        double r2865635 = 1.0;
        double r2865636 = r2865635 + r2865632;
        double r2865637 = sqrt(r2865636);
        double r2865638 = sqrt(r2865632);
        double r2865639 = r2865637 * r2865638;
        double r2865640 = r2865639 + r2865636;
        double r2865641 = r2865635 / r2865640;
        double r2865642 = r2865634 * r2865641;
        return r2865642;
}

Error

Bits error versus x

Target

Original	20.1
Target	0.7
Herbie	0.2

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

Derivation

1. Initial program 20.1

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

3. Applied frac-sub 20.1

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

4. Simplified 20.1

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

6. Applied flip-- 19.9

   \[\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 *-un-lft-identity 0.4

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

10. Applied sqrt-prod 0.4

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

11. Applied *-un-lft-identity 0.4

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

12. Applied *-un-lft-identity 0.4

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

13. Applied distribute-lft-out 0.4

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

14. Applied sqrt-prod 0.4

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

15. Applied distribute-lft-out 0.4

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

16. Applied add-cube-cbrt 0.4

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

17. Applied times-frac 0.4

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

18. Applied times-frac 0.4

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

19. Simplified 0.4

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

20. Simplified 0.3

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

22. Applied pow1 0.3

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

23. Applied sqrt-pow1 0.3

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

24. Applied pow-flip 0.2

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

25. Simplified 0.2

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

26. Final simplification 0.2

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

Reproduce

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