2isqrt (example 3.6)

Average Error: 20.2 → 0.8

Time: 20.1s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r4026558 = 1.0;
        double r4026559 = x;
        double r4026560 = sqrt(r4026559);
        double r4026561 = r4026558 / r4026560;
        double r4026562 = r4026559 + r4026558;
        double r4026563 = sqrt(r4026562);
        double r4026564 = r4026558 / r4026563;
        double r4026565 = r4026561 - r4026564;
        return r4026565;
}

↓

double f(double x) {
        double r4026566 = 1.0;
        double r4026567 = x;
        double r4026568 = r4026567 + r4026566;
        double r4026569 = sqrt(r4026567);
        double r4026570 = r4026566 / r4026569;
        double r4026571 = sqrt(r4026568);
        double r4026572 = r4026566 / r4026571;
        double r4026573 = r4026570 + r4026572;
        double r4026574 = r4026567 * r4026573;
        double r4026575 = r4026568 * r4026574;
        double r4026576 = r4026566 / r4026575;
        return r4026576;
}

Error

Bits error versus x

Target

Original	20.2
Target	0.7
Herbie	0.8

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

Derivation

1. Initial program 20.2

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

3. Applied flip-- 20.2

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

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

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

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

   \[\leadsto \frac{\frac{\color{blue}{\left(x + 1\right) - x}}{\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.7

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

11. Applied div-inv 19.7

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

12. Applied associate-/l* 19.7

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

13. Simplified 19.7

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

14. Taylor expanded around -inf 0.8

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

15. Final simplification 0.8

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

Reproduce

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