2sqrt (example 3.1)

Average Error: 0.8 → 0.5

Time: 13.4s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r2139006 = x;
        double r2139007 = 1.0;
        double r2139008 = /* ERROR: no posit support in C */;
        double r2139009 = r2139006 + r2139008;
        double r2139010 = sqrt(r2139009);
        double r2139011 = sqrt(r2139006);
        double r2139012 = r2139010 - r2139011;
        return r2139012;
}

↓

double f(double x) {
        double r2139013 = 1.0;
        double r2139014 = 1.0;
        double r2139015 = x;
        double r2139016 = r2139014 + r2139015;
        double r2139017 = sqrt(r2139015);
        double r2139018 = r2139017 * r2139017;
        double r2139019 = r2139016 - r2139018;
        double r2139020 = sqrt(r2139016);
        double r2139021 = r2139020 + r2139017;
        double r2139022 = r2139019 / r2139021;
        double r2139023 = r2139013 * r2139022;
        return r2139023;
}

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-flip-- 0.6

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

8. Applied associate-*r/ 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(\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{\left(\frac{\left(1\right)}{x}\right)}\right)}{\left(\sqrt{x}\right)}\right)}\]

9. Applied associate-/l/ 0.7

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

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

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

14. Simplified 0.5

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

15. Final simplification 0.5

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

Reproduce

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