2sqrt (example 3.1)

Average Error: 30.1 → 0.2

Time: 11.2s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

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

↓

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

C

double f(double x) {
        double r152895 = x;
        double r152896 = 1.0;
        double r152897 = r152895 + r152896;
        double r152898 = sqrt(r152897);
        double r152899 = sqrt(r152895);
        double r152900 = r152898 - r152899;
        return r152900;
}

↓

double f(double x) {
        double r152901 = 1.0;
        double r152902 = r152901 * r152901;
        double r152903 = x;
        double r152904 = r152903 + r152901;
        double r152905 = sqrt(r152904);
        double r152906 = sqrt(r152903);
        double r152907 = r152905 * r152906;
        double r152908 = r152904 + r152907;
        double r152909 = r152907 + r152903;
        double r152910 = r152908 + r152909;
        double r152911 = r152902 / r152910;
        double r152912 = 1.0;
        double r152913 = 2.0;
        double r152914 = r152912 / r152913;
        double r152915 = pow(r152911, r152914);
        return r152915;
}

Error

Bits error versus x

Target

Original	30.1
Target	0.2
Herbie	0.2

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

Derivation

1. Initial program 30.1

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

3. Applied flip-- 29.8

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

4. Simplified 0.2

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

6. Applied add-sqr-sqrt 0.3

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

8. Applied pow1 0.3

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

9. Applied sqrt-pow1 0.3

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

10. Applied pow1 0.3

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

11. Applied sqrt-pow1 0.3

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

12. Applied pow-prod-down 0.2

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

13. Simplified 0.2

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

15. Applied distribute-lft-in 0.2

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

16. Simplified 0.2

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

17. Simplified 0.2

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

18. Final simplification 0.2

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

Reproduce

herbie shell --seed 2020043 
(FPCore (x)
  :name "2sqrt (example 3.1)"
  :precision binary64

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

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