2sqrt (example 3.1)

Average Error: 0.8 → 0.6

Time: 13.3s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r9564883 = x;
        double r9564884 = /* ERROR: no support for value #<cpointer:posit16> in C */;
        double r9564885 = r9564883 + r9564884;
        double r9564886 = sqrt(r9564885);
        double r9564887 = sqrt(r9564883);
        double r9564888 = r9564886 - r9564887;
        return r9564888;
}

↓

double f(double x) {
        double r9564889 = x;
        double r9564890 = sqrt(r9564889);
        double r9564891 = /* ERROR: no support for value #<cpointer:posit16> in C */;
        double r9564892 = r9564891 + r9564889;
        double r9564893 = sqrt(r9564892);
        double r9564894 = r9564890 + r9564893;
        double r9564895 = r9564894 * r9564893;
        double r9564896 = -r9564890;
        double r9564897 = r9564894 * r9564896;
        double r9564898 = r9564895 + r9564897;
        double r9564899 = r9564898 / r9564894;
        return r9564899;
}

Error

Bits error versus x

Derivation

1. Initial program 0.8

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

4. Simplified 0.8

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

5. Simplified 0.8

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

7. Applied sub-neg 0.8

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

8. Applied distribute-lft-in 0.6

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

9. Final simplification 0.6

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

Reproduce

herbie shell --seed 0 
(FPCore (x)
  :name "2sqrt (example 3.1)"
  (-.p16 (sqrt.p16 (+.p16 x #<cpointer:posit16>)) (sqrt.p16 x)))