2isqrt (example 3.6)

Average Error: 0.6 → 0.6

Time: 24.3s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r8107470 = 1.0;
        double r8107471 = /* ERROR: no posit support in C */;
        double r8107472 = x;
        double r8107473 = sqrt(r8107472);
        double r8107474 = r8107471 / r8107473;
        double r8107475 = r8107472 + r8107471;
        double r8107476 = sqrt(r8107475);
        double r8107477 = r8107471 / r8107476;
        double r8107478 = r8107474 - r8107477;
        return r8107478;
}

↓

double f(double x) {
        double r8107479 = 1.0;
        double r8107480 = x;
        double r8107481 = r8107479 + r8107480;
        double r8107482 = sqrt(r8107481);
        double r8107483 = r8107479 / r8107482;
        double r8107484 = sqrt(r8107480);
        double r8107485 = r8107479 / r8107484;
        double r8107486 = r8107483 + r8107485;
        double r8107487 = r8107485 - r8107483;
        double r8107488 = r8107487 / r8107486;
        double r8107489 = r8107486 * r8107488;
        return r8107489;
}

Error

Bits error versus x

Derivation

1. Initial program 0.6

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

3. Applied p16-flip-- 0.7

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

5. Applied p16-*-un-lft-identity 0.7

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

6. Applied p16-*-un-lft-identity 0.7

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

7. Applied p16-times-frac 0.7

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

8. Applied p16-*-un-lft-identity 0.7

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

9. Applied p16-*-un-lft-identity 0.7

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

10. Applied p16-times-frac 0.7

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

11. Applied distribute-lft-out 0.7

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

12. Applied difference-of-squares 0.6

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

13. Applied p16-times-frac 0.6

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

14. Simplified 0.6

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

15. Simplified 0.6

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

16. Final simplification 0.6

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

Reproduce

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