Average Error: 0.2 → 0.1
Time: 46.2s
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{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{a + \left(c + b\right)}{2} - b\right)\right) \cdot \left(\frac{\left(c + b\right) + a}{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{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{a + \left(c + b\right)}{2} - b\right)\right) \cdot \left(\frac{\left(c + b\right) + a}{2} - c\right)}
double f(double a, double b, double c) {
        double r1613242 = a;
        double r1613243 = b;
        double r1613244 = r1613242 + r1613243;
        double r1613245 = c;
        double r1613246 = r1613244 + r1613245;
        double r1613247 = 2.0;
        double r1613248 = /* ERROR: no posit support in C */;
        double r1613249 = r1613246 / r1613248;
        double r1613250 = r1613249 - r1613242;
        double r1613251 = r1613249 * r1613250;
        double r1613252 = r1613249 - r1613243;
        double r1613253 = r1613251 * r1613252;
        double r1613254 = r1613249 - r1613245;
        double r1613255 = r1613253 * r1613254;
        double r1613256 = sqrt(r1613255);
        return r1613256;
}
↓
double f(double a, double b, double c) {
        double r1613257 = a;
        double r1613258 = b;
        double r1613259 = r1613257 + r1613258;
        double r1613260 = c;
        double r1613261 = r1613259 + r1613260;
        double r1613262 = 2.0;
        double r1613263 = r1613261 / r1613262;
        double r1613264 = r1613263 - r1613257;
        double r1613265 = r1613263 * r1613264;
        double r1613266 = r1613260 + r1613258;
        double r1613267 = r1613257 + r1613266;
        double r1613268 = r1613267 / r1613262;
        double r1613269 = r1613268 - r1613258;
        double r1613270 = r1613265 * r1613269;
        double r1613271 = r1613266 + r1613257;
        double r1613272 = r1613271 / r1613262;
        double r1613273 = r1613272 - r1613260;
        double r1613274 = r1613270 * r1613273;
        double r1613275 = sqrt(r1613274);
        return r1613275;
}

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 p16-*-un-lft-identity0.2

    \[\leadsto \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)}{\color{blue}{\left(\left(1.0\right) \cdot \left(2\right)\right)}}\right) - c\right)\right)}\]

  4. Applied associate-/r*0.2

    \[\leadsto \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(\color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(1.0\right)}\right)}{\left(2\right)}\right)} - c\right)\right)}\]

  5. Simplified0.1

    \[\leadsto \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{\color{blue}{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}}{\left(2\right)}\right) - c\right)\right)}\]
  6. Using strategy rm

  7. Applied p16-*-un-lft-identity0.1

    \[\leadsto \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)}{\color{blue}{\left(\left(1.0\right) \cdot \left(2\right)\right)}}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) - c\right)\right)}\]

  8. Applied associate-/r*0.1

    \[\leadsto \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(\color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(1.0\right)}\right)}{\left(2\right)}\right)} - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) - c\right)\right)}\]

  9. Simplified0.1

    \[\leadsto \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{\color{blue}{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) - c\right)\right)}\]

  10. Final simplification0.1

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

Reproduce

herbie shell --seed 2019156 
(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))))