2isqrt (example 3.6)

Average Error: 19.5 → 0.3

Time: 4.1m

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r19233632 = 1.0;
        double r19233633 = x;
        double r19233634 = sqrt(r19233633);
        double r19233635 = r19233632 / r19233634;
        double r19233636 = r19233633 + r19233632;
        double r19233637 = sqrt(r19233636);
        double r19233638 = r19233632 / r19233637;
        double r19233639 = r19233635 - r19233638;
        return r19233639;
}

↓

double f(double x) {
        double r19233640 = 1.0;
        double r19233641 = x;
        double r19233642 = r19233641 + r19233640;
        double r19233643 = r19233640 / r19233642;
        double r19233644 = sqrt(r19233642);
        double r19233645 = r19233641 / r19233644;
        double r19233646 = sqrt(r19233641);
        double r19233647 = r19233645 + r19233646;
        double r19233648 = r19233643 / r19233647;
        return r19233648;
}

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 div-inv 5.6

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

12. Applied *-un-lft-identity 5.6

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

13. Applied distribute-lft-out 5.6

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

14. Applied *-un-lft-identity 5.6

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

15. Applied add-sqr-sqrt 5.6

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

16. Applied times-frac 5.6

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

17. Applied times-frac 5.6

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

18. Simplified 5.6

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

19. Simplified 0.3

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

21. 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}}}}\]

22. 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}}}\]

23. 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}}}}\]

24. Simplified 0.3

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

25. Simplified 0.3

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

26. Final simplification 0.3

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

Reproduce

herbie shell --seed 2019112 +o rules:numerics
(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)))))