2isqrt (example 3.6)

Average Error: 0.6 → 0.6

Time: 26.9s

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

C

double f(double x) {
        double r5636676 = 1.0;
        double r5636677 = /* ERROR: no posit support in C */;
        double r5636678 = x;
        double r5636679 = sqrt(r5636678);
        double r5636680 = r5636677 / r5636679;
        double r5636681 = r5636678 + r5636677;
        double r5636682 = sqrt(r5636681);
        double r5636683 = r5636677 / r5636682;
        double r5636684 = r5636680 - r5636683;
        return r5636684;
}

↓

double f(double x) {
        double r5636685 = 1.0;
        double r5636686 = /* ERROR: no posit support in C */;
        double r5636687 = x;
        double r5636688 = sqrt(r5636687);
        double r5636689 = r5636686 / r5636688;
        double r5636690 = r5636686 + r5636687;
        double r5636691 = sqrt(r5636690);
        double r5636692 = r5636686 / r5636691;
        double r5636693 = r5636689 + r5636692;
        double r5636694 = r5636689 - r5636692;
        double r5636695 = r5636694 / r5636693;
        double r5636696 = r5636693 * r5636695;
        return r5636696;
}

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

16. Final simplification 0.6

    \[\leadsto \left(\frac{\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) \cdot \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{x}\right)}\right)}{\left(\frac{\left(1\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right)}\right)}\right)}\right)\]

Reproduce

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