2sqrt (example 3.1)

Average Error: 0.8 → 0.3

Time: 16.8s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r5370755 = x;
        double r5370756 = 1.0;
        double r5370757 = /* ERROR: no posit support in C */;
        double r5370758 = r5370755 + r5370757;
        double r5370759 = sqrt(r5370758);
        double r5370760 = sqrt(r5370755);
        double r5370761 = r5370759 - r5370760;
        return r5370761;
}

↓

double f(double x) {
        double r5370762 = 1.0;
        double r5370763 = x;
        double r5370764 = sqrt(r5370763);
        double r5370765 = r5370764 * r5370764;
        double r5370766 = r5370763 - r5370765;
        double r5370767 = r5370762 + r5370766;
        double r5370768 = r5370762 + r5370763;
        double r5370769 = sqrt(r5370768);
        double r5370770 = r5370769 + r5370764;
        double r5370771 = r5370767 / r5370770;
        double r5370772 = /*Error: no posit support in C */;
        double r5370773 = /*Error: no posit support in C */;
        return r5370773;
}

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(\frac{\left(\sqrt{x}\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right)}\right) \cdot \left(\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right) - \left(\sqrt{x}\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(\frac{\left(\sqrt{x}\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right)}\right) \cdot \left(\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right) - \left(\sqrt{x}\right)\right)\right)}{\color{blue}{\left(\frac{\left(\sqrt{x}\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right)}\right)}}\]
6. Using strategy rm

7. Applied p16-flip-- 0.6

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

8. Applied associate-*r/ 0.6

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

9. Applied associate-/l/ 0.6

   \[\leadsto \color{blue}{\frac{\left(\left(\frac{\left(\sqrt{x}\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right)}\right) \cdot \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)\right)}{\left(\left(\frac{\left(\sqrt{x}\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\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(\frac{\left(\sqrt{x}\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right)}\right) \cdot \left(\color{blue}{\left(\frac{\left(1\right)}{x}\right)} - \left(\left(\sqrt{x}\right) \cdot \left(\sqrt{x}\right)\right)\right)\right)}{\left(\left(\frac{\left(\sqrt{x}\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\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 introduce-quire 0.5

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

14. Simplified 0.3

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

15. Final simplification 0.3

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

Reproduce

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