2sqrt (example 3.1)

Average Error: 0.8 → 0.5

Time: 1.5m

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r6816999 = x;
        double r6817000 = 1.0;
        double r6817001 = /* ERROR: no posit support in C */;
        double r6817002 = r6816999 + r6817001;
        double r6817003 = sqrt(r6817002);
        double r6817004 = sqrt(r6816999);
        double r6817005 = r6817003 - r6817004;
        return r6817005;
}

↓

double f(double x) {
        double r6817006 = 1.0;
        double r6817007 = x;
        double r6817008 = r6817006 + r6817007;
        double r6817009 = sqrt(r6817007);
        double r6817010 = -r6817009;
        double r6817011 = r6817009 * r6817010;
        double r6817012 = r6817008 + r6817011;
        double r6817013 = sqrt(r6817008);
        double r6817014 = r6817013 + r6817009;
        double r6817015 = r6817012 / r6817014;
        return r6817015;
}

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

7. Applied +p16-rgt-identity-expand 0.8

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

8. Applied associate--l+ 0.8

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

9. Applied distribute-lft-in 0.6

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

10. Simplified 0.6

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

12. Applied distribute-rgt-in 0.7

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

13. Applied associate-+r+ 0.9

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

14. Simplified 0.6

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

16. Applied sqrt-sqrd.p16 0.5

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

17. Final simplification 0.5

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

Reproduce

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