Average Error: 0.8 → 0.4
Time: 8.6s
Precision: 64
\[\left(\sqrt{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\sqrt{x}\right)\]
↓
\[\frac{1 \cdot \left(x + \left(1 + x\right)\right)}{\left(\sqrt{x + 1} + \sqrt{x}\right) \cdot \left(\left(x + 1\right) + x\right)}\]
\left(\sqrt{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\sqrt{x}\right)
↓
\frac{1 \cdot \left(x + \left(1 + x\right)\right)}{\left(\sqrt{x + 1} + \sqrt{x}\right) \cdot \left(\left(x + 1\right) + x\right)}
double f(double x) {
        double r1587180 = x;
        double r1587181 = 1.0;
        double r1587182 = /* ERROR: no posit support in C */;
        double r1587183 = r1587180 + r1587182;
        double r1587184 = sqrt(r1587183);
        double r1587185 = sqrt(r1587180);
        double r1587186 = r1587184 - r1587185;
        return r1587186;
}
↓
double f(double x) {
        double r1587187 = 1.0;
        double r1587188 = x;
        double r1587189 = r1587187 + r1587188;
        double r1587190 = r1587188 + r1587189;
        double r1587191 = r1587187 * r1587190;
        double r1587192 = r1587188 + r1587187;
        double r1587193 = sqrt(r1587192);
        double r1587194 = sqrt(r1587188);
        double r1587195 = r1587193 + r1587194;
        double r1587196 = r1587192 + r1587188;
        double r1587197 = r1587195 * r1587196;
        double r1587198 = r1587191 / r1587197;
        return r1587198;
}

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. Using strategy rm

  5. Applied sqrt-sqrd.p160.5

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

  7. Applied sqrt-sqrd.p160.4

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

  9. Applied p16-flip--0.9

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

  10. Applied associate-/l/0.9

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

  11. Simplified0.4

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

  12. Final simplification0.4

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

Reproduce

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