2sqrt (example 3.1)

Average Error: 30.4 → 0.2

Time: 6.7s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r114225 = x;
        double r114226 = 1.0;
        double r114227 = r114225 + r114226;
        double r114228 = sqrt(r114227);
        double r114229 = sqrt(r114225);
        double r114230 = r114228 - r114229;
        return r114230;
}

↓

double f(double x) {
        double r114231 = 1.0;
        double r114232 = sqrt(r114231);
        double r114233 = 1.0;
        double r114234 = sqrt(r114233);
        double r114235 = sqrt(r114234);
        double r114236 = r114232 / r114235;
        double r114237 = x;
        double r114238 = r114237 + r114231;
        double r114239 = sqrt(r114238);
        double r114240 = sqrt(r114237);
        double r114241 = r114239 + r114240;
        double r114242 = r114241 / r114232;
        double r114243 = r114236 / r114242;
        return r114243;
}

Error

Bits error versus x

Target

Original	30.4
Target	0.2
Herbie	0.2

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

Derivation

1. Initial program 30.4

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

3. Applied flip-- 30.2

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

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

7. Applied associate-/r* 0.3

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

9. Applied *-un-lft-identity 0.3

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

10. Applied sqrt-prod 0.3

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

11. Applied *-un-lft-identity 0.3

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

12. Applied sqrt-prod 0.3

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

13. Applied distribute-lft-out 0.3

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

14. Applied sqrt-prod 0.3

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

15. Applied add-sqr-sqrt 0.3

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

16. Applied times-frac 0.3

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

17. Applied associate-/l* 0.4

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

18. Simplified 0.2

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

19. Final simplification 0.2

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

Reproduce

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

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

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