2isqrt (example 3.6)

Average Error: 0.6 → 0.6

Time: 23.7s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r2039991 = 1.0;
        double r2039992 = /* ERROR: no posit support in C */;
        double r2039993 = x;
        double r2039994 = sqrt(r2039993);
        double r2039995 = r2039992 / r2039994;
        double r2039996 = r2039993 + r2039992;
        double r2039997 = sqrt(r2039996);
        double r2039998 = r2039992 / r2039997;
        double r2039999 = r2039995 - r2039998;
        return r2039999;
}

↓

double f(double x) {
        double r2040000 = 1.0;
        double r2040001 = 1.0;
        double r2040002 = x;
        double r2040003 = sqrt(r2040002);
        double r2040004 = r2040001 / r2040003;
        double r2040005 = r2040001 + r2040002;
        double r2040006 = sqrt(r2040005);
        double r2040007 = r2040001 / r2040006;
        double r2040008 = r2040004 - r2040007;
        double r2040009 = r2040000 * r2040008;
        return r2040009;
}

Error

Bits error versus x

Derivation

1. Initial program 0.6

   \[\left(\frac{\left(1\right)}{\left(\sqrt{x}\right)}\right) - \left(\frac{\left(1\right)}{\left(\sqrt{\left(\frac{x}{\left(1\right)}\right)}\right)}\right)\]
2. Using strategy rm

3. Applied p16-flip-- 0.7

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

5. Applied *p16-rgt-identity-expand 0.7

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

6. Applied difference-of-squares 0.6

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

7. Applied p16-times-frac 0.6

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

8. Simplified 0.6

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

9. Simplified 0.6

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

10. Final simplification 0.6

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

Reproduce

herbie shell --seed 2019155 
(FPCore (x)
  :name "2isqrt (example 3.6)"
  (-.p16 (/.p16 (real->posit16 1) (sqrt.p16 x)) (/.p16 (real->posit16 1) (sqrt.p16 (+.p16 x (real->posit16 1))))))