Area of a triangle

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\]

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(\left(\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)}\]

C

double f(double a, double b, double c) {
        double r5217564 = a;
        double r5217565 = b;
        double r5217566 = r5217564 + r5217565;
        double r5217567 = c;
        double r5217568 = r5217566 + r5217567;
        double r5217569 = 2.0;
        double r5217570 = /* ERROR: no posit support in C */;
        double r5217571 = r5217568 / r5217570;
        double r5217572 = r5217571 - r5217564;
        double r5217573 = r5217571 * r5217572;
        double r5217574 = r5217571 - r5217565;
        double r5217575 = r5217573 * r5217574;
        double r5217576 = r5217571 - r5217567;
        double r5217577 = r5217575 * r5217576;
        double r5217578 = sqrt(r5217577);
        return r5217578;
}

↓

double f(double a, double b, double c) {
        double r5217579 = b;
        double r5217580 = a;
        double r5217581 = c;
        double r5217582 = r5217580 + r5217581;
        double r5217583 = r5217579 + r5217582;
        double r5217584 = 2.0;
        double r5217585 = /* ERROR: no posit support in C */;
        double r5217586 = r5217583 / r5217585;
        double r5217587 = r5217586 - r5217579;
        double r5217588 = r5217586 * r5217587;
        double r5217589 = 1.0;
        double r5217590 = /* ERROR: no posit support in C */;
        double r5217591 = r5217586 - r5217580;
        double r5217592 = r5217590 / r5217591;
        double r5217593 = r5217588 / r5217592;
        double r5217594 = /*Error: no posit support in C */;
        double r5217595 = /*Error: no posit support in C */;
        double r5217596 = r5217580 + r5217579;
        double r5217597 = r5217596 + r5217581;
        double r5217598 = r5217597 / r5217585;
        double r5217599 = r5217598 - r5217581;
        double r5217600 = r5217595 * r5217599;
        double r5217601 = sqrt(r5217600);
        return r5217601;
}

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 *-commutative 0.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-quire 0.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. Simplified 0.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 simplification 0.1

    \[\leadsto \sqrt{\left(\left(\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)}\]

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))))