2isqrt (example 3.6)

Average Error: 19.8 → 5.2

Time: 9.0s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r517153 = 1.0;
        double r517154 = x;
        double r517155 = sqrt(r517154);
        double r517156 = r517153 / r517155;
        double r517157 = r517154 + r517153;
        double r517158 = sqrt(r517157);
        double r517159 = r517153 / r517158;
        double r517160 = r517156 - r517159;
        return r517160;
}

↓

double f(double x) {
        double r517161 = 1.0;
        double r517162 = 3.0;
        double r517163 = pow(r517161, r517162);
        double r517164 = x;
        double r517165 = r517164 + r517161;
        double r517166 = r517163 / r517165;
        double r517167 = r517166 / r517164;
        double r517168 = sqrt(r517161);
        double r517169 = sqrt(r517164);
        double r517170 = r517168 / r517169;
        double r517171 = sqrt(r517165);
        double r517172 = r517168 / r517171;
        double r517173 = r517170 + r517172;
        double r517174 = r517173 * r517168;
        double r517175 = r517167 / r517174;
        return r517175;
}

Error

Bits error versus x

Target

Original	19.8
Target	0.6
Herbie	5.2

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

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

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

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

   \[\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(1 \cdot 1\right) \cdot \left(\left(x + 1\right) - x\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}}}\]

9. Simplified 19.2

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

10. Taylor expanded around 0 5.5

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

12. Applied *-un-lft-identity 5.5

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

13. Applied add-sqr-sqrt 5.5

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

14. Applied times-frac 5.5

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

15. Applied *-un-lft-identity 5.5

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

16. Applied add-sqr-sqrt 5.5

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

17. Applied times-frac 5.5

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

18. Applied distribute-lft-out 5.5

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

19. Applied times-frac 5.2

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

20. Applied times-frac 0.4

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

21. Simplified 0.4

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

22. Final simplification 5.2

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

Reproduce

herbie shell --seed 350497007 
(FPCore (x)
  :name "2isqrt (example 3.6)"
  :precision binary64

  :herbie-target
  (/ 1 (+ (* (+ x 1) (sqrt x)) (* x (sqrt (+ x 1)))))

  (- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))