2sqrt (example 3.1)

Average Error: 0.8 → 0.7

Time: 38.4s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r1647997 = x;
        double r1647998 = 1.0;
        double r1647999 = /* ERROR: no posit support in C */;
        double r1648000 = r1647997 + r1647999;
        double r1648001 = sqrt(r1648000);
        double r1648002 = sqrt(r1647997);
        double r1648003 = r1648001 - r1648002;
        return r1648003;
}

↓

double f(double x) {
        double r1648004 = 1.0;
        double r1648005 = /* ERROR: no posit support in C */;
        double r1648006 = x;
        double r1648007 = r1648005 + r1648006;
        double r1648008 = sqrt(r1648007);
        double r1648009 = sqrt(r1648006);
        double r1648010 = r1648008 + r1648009;
        double r1648011 = r1648010 * r1648008;
        double r1648012 = -r1648009;
        double r1648013 = r1648010 * r1648012;
        double r1648014 = r1648011 + r1648013;
        double r1648015 = r1648014 / r1648010;
        return r1648015;
}

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

8. Applied distribute-lft-in 0.7

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

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

Reproduce

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