Average Error: 0.2 → 0.1
Time: 1.1m
Precision: 64
\[\left(0\right) \lt a \land \left(0\right) \lt b \land \left(0\right) \lt c\]
\[\sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]
↓
\[\sqrt{\left(\left(\frac{\frac{b + \left(a + c\right)}{2} \cdot \left(\frac{b + \left(a + c\right)}{2} - b\right)}{\frac{1.0}{\frac{b + \left(a + c\right)}{2} - a}}\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}\]
\sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}
↓
\sqrt{\left(\left(\frac{\frac{b + \left(a + c\right)}{2} \cdot \left(\frac{b + \left(a + c\right)}{2} - b\right)}{\frac{1.0}{\frac{b + \left(a + c\right)}{2} - a}}\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}
double f(double a, double b, double c) {
        double r5206266 = a;
        double r5206267 = b;
        double r5206268 = r5206266 + r5206267;
        double r5206269 = c;
        double r5206270 = r5206268 + r5206269;
        double r5206271 = 2.0;
        double r5206272 = /* ERROR: no posit support in C */;
        double r5206273 = r5206270 / r5206272;
        double r5206274 = r5206273 - r5206266;
        double r5206275 = r5206273 * r5206274;
        double r5206276 = r5206273 - r5206267;
        double r5206277 = r5206275 * r5206276;
        double r5206278 = r5206273 - r5206269;
        double r5206279 = r5206277 * r5206278;
        double r5206280 = sqrt(r5206279);
        return r5206280;
}
↓
double f(double a, double b, double c) {
        double r5206281 = b;
        double r5206282 = a;
        double r5206283 = c;
        double r5206284 = r5206282 + r5206283;
        double r5206285 = r5206281 + r5206284;
        double r5206286 = 2.0;
        double r5206287 = r5206285 / r5206286;
        double r5206288 = r5206287 - r5206281;
        double r5206289 = r5206287 * r5206288;
        double r5206290 = 1.0;
        double r5206291 = r5206287 - r5206282;
        double r5206292 = r5206290 / r5206291;
        double r5206293 = r5206289 / r5206292;
        double r5206294 = /*Error: no posit support in C */;
        double r5206295 = /*Error: no posit support in C */;
        double r5206296 = r5206282 + r5206281;
        double r5206297 = r5206296 + r5206283;
        double r5206298 = r5206297 / r5206286;
        double r5206299 = r5206298 - r5206283;
        double r5206300 = r5206295 * r5206299;
        double r5206301 = sqrt(r5206300);
        return r5206301;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Derivation

  1. Initial program 0.2

    \[\sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]
  2. Using strategy rm

  3. Applied *-commutative0.2

    \[\leadsto \sqrt{\left(\color{blue}{\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right)\right)} \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]
  4. Using strategy rm

  5. Applied associate-*r*0.2

    \[\leadsto \sqrt{\left(\color{blue}{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right) \cdot \left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right)} \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]
  6. Using strategy rm

  7. Applied p16-flip--0.2

    \[\leadsto \sqrt{\left(\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right) \cdot \left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)\right) \cdot \color{blue}{\left(\frac{\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)\right) - \left(a \cdot a\right)\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{a}\right)}\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]

  8. Applied associate-*r/0.2

    \[\leadsto \sqrt{\left(\color{blue}{\left(\frac{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right) \cdot \left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)\right) \cdot \left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)\right) - \left(a \cdot a\right)\right)\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{a}\right)}\right)} \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]
  9. Using strategy rm

  10. Applied introduce-quire0.2

    \[\leadsto \sqrt{\left(\color{blue}{\left(\left(\left(\frac{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right) \cdot \left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)\right) \cdot \left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)\right) - \left(a \cdot a\right)\right)\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{a}\right)}\right)\right)\right)} \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]

  11. Simplified0.1

    \[\leadsto \sqrt{\left(\left(\color{blue}{\left(\left(\frac{\left(\left(\frac{\left(\frac{b}{\left(\frac{a}{c}\right)}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{b}{\left(\frac{a}{c}\right)}\right)}{\left(2\right)}\right) - b\right)\right)}{\left(\frac{\left(1.0\right)}{\left(\left(\frac{\left(\frac{b}{\left(\frac{a}{c}\right)}\right)}{\left(2\right)}\right) - a\right)}\right)}\right)\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]

  12. Final simplification0.1

    \[\leadsto \sqrt{\left(\left(\frac{\frac{b + \left(a + c\right)}{2} \cdot \left(\frac{b + \left(a + c\right)}{2} - b\right)}{\frac{1.0}{\frac{b + \left(a + c\right)}{2} - a}}\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}\]

Reproduce

herbie shell --seed 2019163 +o rules:numerics
(FPCore (a b c)
  :name "Area of a triangle"
  :pre (and (<.p16 (real->posit16 0) a) (<.p16 (real->posit16 0) b) (<.p16 (real->posit16 0) c))
  (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))