2isqrt (example 3.6)

Average Error: 0.5 → 0.7

Time: 27.0s

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{\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(1.0\right)}{\left(\frac{\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)}{\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)}\right)}\right)\]

C

double f(double x) {
        double r5914580 = 1.0;
        double r5914581 = /* ERROR: no posit support in C */;
        double r5914582 = x;
        double r5914583 = sqrt(r5914582);
        double r5914584 = r5914581 / r5914583;
        double r5914585 = r5914582 + r5914581;
        double r5914586 = sqrt(r5914585);
        double r5914587 = r5914581 / r5914586;
        double r5914588 = r5914584 - r5914587;
        return r5914588;
}

↓

double f(double x) {
        double r5914589 = 1.0;
        double r5914590 = /* ERROR: no posit support in C */;
        double r5914591 = x;
        double r5914592 = r5914590 + r5914591;
        double r5914593 = sqrt(r5914592);
        double r5914594 = r5914590 / r5914593;
        double r5914595 = sqrt(r5914591);
        double r5914596 = r5914590 / r5914595;
        double r5914597 = r5914594 + r5914596;
        double r5914598 = 1.0;
        double r5914599 = /* ERROR: no posit support in C */;
        double r5914600 = r5914596 - r5914594;
        double r5914601 = r5914597 / r5914600;
        double r5914602 = r5914599 / r5914601;
        double r5914603 = r5914597 * r5914602;
        return r5914603;
}

Error

Bits error versus x

Derivation

1. Initial program 0.5

   \[\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. Using strategy rm

17. Applied p16-*-un-lft-identity 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 \left(\frac{\left(\left(\frac{\left(1\right)}{\left(\sqrt{x}\right)}\right) - \color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(1\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\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)\]

18. Applied p16-*-un-lft-identity 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 \left(\frac{\left(\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(1\right)}{\left(\sqrt{x}\right)}\right)\right)} - \left(\left(1.0\right) \cdot \left(\frac{\left(1\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\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)\]

19. Applied distribute-lft-out-- 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 \left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \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)\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)\]

20. Applied associate-/l* 0.7

    \[\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(1.0\right)}{\left(\frac{\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)}{\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)}\right)}\right)}\]

21. Final simplification 0.7

    \[\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 \left(\frac{\left(1.0\right)}{\left(\frac{\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)}{\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)}\right)}\right)\]

Reproduce

herbie shell --seed 2019163 +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))))))