Average Error: 0.8 → 0.3
Time: 18.4s
Precision: 64
\[\left(\sqrt{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\sqrt{x}\right)\]
↓
\[\left(\left(\frac{1.0 \cdot \left(1 + \left(x - \sqrt{x} \cdot \sqrt{x}\right)\right)}{\sqrt{x} + \sqrt{1 + x}}\right)\right)\]
\left(\sqrt{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\sqrt{x}\right)
↓
\left(\left(\frac{1.0 \cdot \left(1 + \left(x - \sqrt{x} \cdot \sqrt{x}\right)\right)}{\sqrt{x} + \sqrt{1 + x}}\right)\right)
double f(double x) {
        double r7478582 = x;
        double r7478583 = 1.0;
        double r7478584 = /* ERROR: no posit support in C */;
        double r7478585 = r7478582 + r7478584;
        double r7478586 = sqrt(r7478585);
        double r7478587 = sqrt(r7478582);
        double r7478588 = r7478586 - r7478587;
        return r7478588;
}
↓
double f(double x) {
        double r7478589 = 1.0;
        double r7478590 = 1.0;
        double r7478591 = x;
        double r7478592 = sqrt(r7478591);
        double r7478593 = r7478592 * r7478592;
        double r7478594 = r7478591 - r7478593;
        double r7478595 = r7478590 + r7478594;
        double r7478596 = r7478589 * r7478595;
        double r7478597 = r7478590 + r7478591;
        double r7478598 = sqrt(r7478597);
        double r7478599 = r7478592 + r7478598;
        double r7478600 = r7478596 / r7478599;
        double r7478601 = /*Error: no posit support in C */;
        double r7478602 = /*Error: no posit support in C */;
        return r7478602;
}

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. Simplified0.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. Simplified0.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.p160.5

    \[\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 introduce-quire0.5

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

  14. Simplified0.3

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

  15. Final simplification0.3

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

Reproduce

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