2sqrt (example 3.1)

Average Error: 0.8 → 0.4

Time: 16.7s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r5808663 = x;
        double r5808664 = 1.0;
        double r5808665 = /* ERROR: no posit support in C */;
        double r5808666 = r5808663 + r5808665;
        double r5808667 = sqrt(r5808666);
        double r5808668 = sqrt(r5808663);
        double r5808669 = r5808667 - r5808668;
        return r5808669;
}

↓

double f(double x) {
        double r5808670 = x;
        double r5808671 = sqrt(r5808670);
        double r5808672 = r5808671 * r5808671;
        double r5808673 = 1.0;
        double r5808674 = r5808672 + r5808673;
        double r5808675 = r5808670 + r5808674;
        double r5808676 = r5808670 - r5808672;
        double r5808677 = r5808673 + r5808676;
        double r5808678 = r5808675 * r5808677;
        double r5808679 = r5808678 / r5808675;
        double r5808680 = r5808673 + r5808670;
        double r5808681 = sqrt(r5808680);
        double r5808682 = r5808671 + r5808681;
        double r5808683 = r5808679 * r5808682;
        double r5808684 = r5808681 + r5808671;
        double r5808685 = r5808684 * r5808684;
        double r5808686 = r5808683 / r5808685;
        return r5808686;
}

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(\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right) - \left(\sqrt{x}\right)\right) \cdot \left(\frac{\left(\sqrt{x}\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\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(\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\right) - \left(\sqrt{x}\right)\right) \cdot \left(\frac{\left(\sqrt{x}\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{x}\right)}\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(\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)} \cdot \left(\frac{\left(\sqrt{x}\right)}{\left(\sqrt{\left(\frac{\left(1\right)}{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-*l/ 0.6

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

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

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

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

14. Simplified 0.4

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

15. Simplified 0.4

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

16. Final simplification 0.4

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

Reproduce

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