2isqrt (example 3.6)

Average Error: 0.6 → 0.6

Time: 19.2s

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 r1854854 = 1.0;
        double r1854855 = /* ERROR: no posit support in C */;
        double r1854856 = x;
        double r1854857 = sqrt(r1854856);
        double r1854858 = r1854855 / r1854857;
        double r1854859 = r1854856 + r1854855;
        double r1854860 = sqrt(r1854859);
        double r1854861 = r1854855 / r1854860;
        double r1854862 = r1854858 - r1854861;
        return r1854862;
}

↓

double f(double x) {
        double r1854863 = 1.0;
        double r1854864 = x;
        double r1854865 = r1854863 + r1854864;
        double r1854866 = sqrt(r1854865);
        double r1854867 = r1854863 / r1854866;
        double r1854868 = sqrt(r1854864);
        double r1854869 = r1854863 / r1854868;
        double r1854870 = r1854867 + r1854869;
        double r1854871 = r1854869 - r1854867;
        double r1854872 = r1854871 / r1854870;
        double r1854873 = r1854870 * r1854872;
        return r1854873;
}

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 2019153 
(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))))))