2sqrt (example 3.1)

Average Error: 0.8 → 0.4

Time: 16.3s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r5677311 = x;
        double r5677312 = 1.0;
        double r5677313 = /* ERROR: no posit support in C */;
        double r5677314 = r5677311 + r5677313;
        double r5677315 = sqrt(r5677314);
        double r5677316 = sqrt(r5677311);
        double r5677317 = r5677315 - r5677316;
        return r5677317;
}

↓

double f(double x) {
        double r5677318 = x;
        double r5677319 = sqrt(r5677318);
        double r5677320 = r5677319 * r5677319;
        double r5677321 = 1.0;
        double r5677322 = r5677320 + r5677321;
        double r5677323 = r5677318 + r5677322;
        double r5677324 = r5677318 - r5677320;
        double r5677325 = r5677321 + r5677324;
        double r5677326 = r5677323 * r5677325;
        double r5677327 = r5677326 / r5677323;
        double r5677328 = r5677321 + r5677318;
        double r5677329 = sqrt(r5677328);
        double r5677330 = r5677319 + r5677329;
        double r5677331 = r5677327 * r5677330;
        double r5677332 = r5677329 + r5677319;
        double r5677333 = r5677332 * r5677332;
        double r5677334 = r5677331 / r5677333;
        return r5677334;
}

Error

Bits error versus x

Derivation

1. Initial program 0.8

   \[\left(\sqrt{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\sqrt{x}\right)\]
2. Using strategy rm

3. Applied p16-flip-- 0.6

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

4. Simplified 0.8

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

5. Simplified 0.8

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

7. Applied p16-flip-- 0.6

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

8. Applied associate-*l/ 0.6

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

9. Applied associate-/l/ 0.6

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

11. Applied sqrt-sqrd.p16 0.5

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

13. Applied p16-flip-- 0.9

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

14. Simplified 0.4

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

15. Simplified 0.4

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

16. Final simplification 0.4

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

Reproduce

herbie shell --seed 2019163 +o rules:numerics
(FPCore (x)
  :name "2sqrt (example 3.1)"
  (-.p16 (sqrt.p16 (+.p16 x (real->posit16 1))) (sqrt.p16 x)))