Average Error: 0.2 → 0.2
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(\left(\frac{\left(a + b\right) + c}{2} - b\right) \cdot \frac{\left(a + b\right) + c}{2}\right) \cdot \left(\frac{\left(a + b\right) + c}{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(\left(\frac{\left(a + b\right) + c}{2} - b\right) \cdot \frac{\left(a + b\right) + c}{2}\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}
double f(double a, double b, double c) {
        double r3834310 = a;
        double r3834311 = b;
        double r3834312 = r3834310 + r3834311;
        double r3834313 = c;
        double r3834314 = r3834312 + r3834313;
        double r3834315 = 2.0;
        double r3834316 = /* ERROR: no posit support in C */;
        double r3834317 = r3834314 / r3834316;
        double r3834318 = r3834317 - r3834310;
        double r3834319 = r3834317 * r3834318;
        double r3834320 = r3834317 - r3834311;
        double r3834321 = r3834319 * r3834320;
        double r3834322 = r3834317 - r3834313;
        double r3834323 = r3834321 * r3834322;
        double r3834324 = sqrt(r3834323);
        return r3834324;
}
↓
double f(double a, double b, double c) {
        double r3834325 = a;
        double r3834326 = b;
        double r3834327 = r3834325 + r3834326;
        double r3834328 = c;
        double r3834329 = r3834327 + r3834328;
        double r3834330 = 2.0;
        double r3834331 = r3834329 / r3834330;
        double r3834332 = r3834331 - r3834326;
        double r3834333 = r3834332 * r3834331;
        double r3834334 = r3834331 - r3834325;
        double r3834335 = r3834333 * r3834334;
        double r3834336 = r3834331 - r3834328;
        double r3834337 = r3834335 * r3834336;
        double r3834338 = sqrt(r3834337);
        return r3834338;
}

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. Final simplification0.2

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