2isqrt (example 3.6)

Average Error: 19.5 → 0.3

Time: 2.4m

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r14715348 = 1.0;
        double r14715349 = x;
        double r14715350 = sqrt(r14715349);
        double r14715351 = r14715348 / r14715350;
        double r14715352 = r14715349 + r14715348;
        double r14715353 = sqrt(r14715352);
        double r14715354 = r14715348 / r14715353;
        double r14715355 = r14715351 - r14715354;
        return r14715355;
}

↓

double f(double x) {
        double r14715356 = 1.0;
        double r14715357 = x;
        double r14715358 = r14715357 + r14715356;
        double r14715359 = r14715356 / r14715358;
        double r14715360 = sqrt(r14715357);
        double r14715361 = r14715359 / r14715360;
        double r14715362 = sqrt(r14715358);
        double r14715363 = r14715360 / r14715362;
        double r14715364 = r14715360 / r14715360;
        double r14715365 = r14715363 + r14715364;
        double r14715366 = r14715361 / r14715365;
        return r14715366;
}

Error

Bits error versus x

Target

Original	19.5
Target	0.7
Herbie	0.3

\[\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 flip-- 19.6

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

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

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

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

   \[\leadsto \frac{\frac{\color{blue}{1}}{\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 5.6

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

11. Applied *-un-lft-identity 5.6

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

12. Applied *-un-lft-identity 5.6

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

13. Applied times-frac 5.6

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

14. Applied *-un-lft-identity 5.6

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

15. Applied *-un-lft-identity 5.6

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

16. Applied times-frac 5.6

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

17. Applied distribute-lft-out 5.6

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

18. Applied *-un-lft-identity 5.6

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

19. Applied add-cube-cbrt 5.6

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

20. Applied times-frac 5.6

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

21. Applied times-frac 5.6

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

22. Simplified 5.6

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

23. Simplified 0.3

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

25. Applied *-un-lft-identity 0.3

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

26. Applied add-sqr-sqrt 0.3

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

27. Applied times-frac 0.3

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

28. Applied *-un-lft-identity 0.3

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

29. Applied add-sqr-sqrt 0.3

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

30. Applied times-frac 0.3

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

31. Applied distribute-lft-out 0.3

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

32. Applied associate-/r* 0.3

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

33. Final simplification 0.3

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

Reproduce

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