Area of a triangle

Average Error: 0.2 → 0.1

Time: 56.7s

Precision: 64

\[\left(0\right) \lt a \land \left(0\right) \lt b \land \left(0\right) \lt c\]

Math

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

C

double f(double a, double b, double c) {
        double r5679481 = a;
        double r5679482 = b;
        double r5679483 = r5679481 + r5679482;
        double r5679484 = c;
        double r5679485 = r5679483 + r5679484;
        double r5679486 = 2.0;
        double r5679487 = /* ERROR: no posit support in C */;
        double r5679488 = r5679485 / r5679487;
        double r5679489 = r5679488 - r5679481;
        double r5679490 = r5679488 * r5679489;
        double r5679491 = r5679488 - r5679482;
        double r5679492 = r5679490 * r5679491;
        double r5679493 = r5679488 - r5679484;
        double r5679494 = r5679492 * r5679493;
        double r5679495 = sqrt(r5679494);
        return r5679495;
}

↓

double f(double a, double b, double c) {
        double r5679496 = c;
        double r5679497 = b;
        double r5679498 = r5679496 + r5679497;
        double r5679499 = a;
        double r5679500 = r5679498 + r5679499;
        double r5679501 = 2.0;
        double r5679502 = r5679500 / r5679501;
        double r5679503 = r5679499 + r5679498;
        double r5679504 = r5679503 / r5679501;
        double r5679505 = r5679504 - r5679499;
        double r5679506 = r5679499 + r5679504;
        double r5679507 = r5679505 * r5679506;
        double r5679508 = r5679502 + r5679499;
        double r5679509 = r5679507 / r5679508;
        double r5679510 = r5679502 * r5679509;
        double r5679511 = r5679510 * r5679508;
        double r5679512 = r5679504 + r5679499;
        double r5679513 = r5679511 / r5679512;
        double r5679514 = r5679499 + r5679497;
        double r5679515 = r5679514 + r5679496;
        double r5679516 = r5679515 / r5679501;
        double r5679517 = r5679516 - r5679497;
        double r5679518 = r5679513 * r5679517;
        double r5679519 = r5679516 - r5679496;
        double r5679520 = r5679518 * r5679519;
        double r5679521 = sqrt(r5679520);
        return r5679521;
}

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-flip-- 0.2

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

4. Applied associate-*r/ 0.2

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

6. Applied associate-/l* 0.2

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

7. Simplified 0.1

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

9. Applied p16-flip-- 0.1

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

10. Applied associate-/r/ 0.1

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

11. Applied associate-/r* 0.1

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

12. Simplified 0.1

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

14. Applied p16-flip-- 0.2

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

15. Simplified 0.1

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

16. Final simplification 0.1

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

Reproduce

herbie shell --seed 2019133 +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))))