2isqrt (example 3.6)

Average Error: 19.0 → 18.4

Time: 13.6s

Precision: 64

Math

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

↓

\[\frac{1 \cdot \left(\left(\sqrt{x} \cdot \sqrt{x} + \sqrt{1} \cdot \sqrt{1}\right) - \sqrt{x} \cdot \sqrt{x}\right)}{\mathsf{fma}\left(\sqrt{x}, \mathsf{hypot}\left(\sqrt{x}, \sqrt{1}\right), x\right) \cdot \mathsf{hypot}\left(\sqrt{x}, \sqrt{1}\right)}\]

C

double f(double x) {
        double r256156 = 1.0;
        double r256157 = x;
        double r256158 = sqrt(r256157);
        double r256159 = r256156 / r256158;
        double r256160 = r256157 + r256156;
        double r256161 = sqrt(r256160);
        double r256162 = r256156 / r256161;
        double r256163 = r256159 - r256162;
        return r256163;
}

↓

double f(double x) {
        double r256164 = 1.0;
        double r256165 = x;
        double r256166 = sqrt(r256165);
        double r256167 = r256166 * r256166;
        double r256168 = sqrt(r256164);
        double r256169 = r256168 * r256168;
        double r256170 = r256167 + r256169;
        double r256171 = r256170 - r256167;
        double r256172 = r256164 * r256171;
        double r256173 = hypot(r256166, r256168);
        double r256174 = fma(r256166, r256173, r256165);
        double r256175 = r256174 * r256173;
        double r256176 = r256172 / r256175;
        return r256176;
}

Error

Bits error versus x

Target

Original	19.0
Target	0.6
Herbie	18.4

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

Derivation

1. Initial program 19.0

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

3. Applied add-sqr-sqrt 19.0

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

4. Applied add-sqr-sqrt 19.0

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

5. Applied hypot-def 19.0

   \[\leadsto \frac{1}{\sqrt{x}} - \frac{1}{\color{blue}{\mathsf{hypot}\left(\sqrt{x}, \sqrt{1}\right)}}\]
6. Using strategy rm

7. Applied frac-sub 19.0

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

8. Simplified 19.0

   \[\leadsto \frac{\color{blue}{1 \cdot \left(\mathsf{hypot}\left(\sqrt{x}, \sqrt{1}\right) - \sqrt{x}\right)}}{\sqrt{x} \cdot \mathsf{hypot}\left(\sqrt{x}, \sqrt{1}\right)}\]
9. Using strategy rm

10. Applied flip-- 18.8

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

11. Applied associate-*r/ 18.8

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

12. Applied associate-/l/ 18.8

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

13. Simplified 18.8

    \[\leadsto \frac{1 \cdot \left(\mathsf{hypot}\left(\sqrt{x}, \sqrt{1}\right) \cdot \mathsf{hypot}\left(\sqrt{x}, \sqrt{1}\right) - \sqrt{x} \cdot \sqrt{x}\right)}{\color{blue}{\mathsf{fma}\left(\sqrt{x}, \mathsf{hypot}\left(\sqrt{x}, \sqrt{1}\right), x\right) \cdot \mathsf{hypot}\left(\sqrt{x}, \sqrt{1}\right)}}\]
14. Using strategy rm

15. Applied hypot-udef 18.8

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

16. Applied hypot-udef 18.8

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

17. Applied rem-square-sqrt 18.4

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

18. Final simplification 18.4

    \[\leadsto \frac{1 \cdot \left(\left(\sqrt{x} \cdot \sqrt{x} + \sqrt{1} \cdot \sqrt{1}\right) - \sqrt{x} \cdot \sqrt{x}\right)}{\mathsf{fma}\left(\sqrt{x}, \mathsf{hypot}\left(\sqrt{x}, \sqrt{1}\right), x\right) \cdot \mathsf{hypot}\left(\sqrt{x}, \sqrt{1}\right)}\]

Reproduce

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