Area of a triangle

Average Error: 0.1 → 0.2

Time: 1.3m

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

C

double f(double a, double b, double c) {
        double r6087745 = a;
        double r6087746 = b;
        double r6087747 = r6087745 + r6087746;
        double r6087748 = c;
        double r6087749 = r6087747 + r6087748;
        double r6087750 = 2.0;
        double r6087751 = /* ERROR: no posit support in C */;
        double r6087752 = r6087749 / r6087751;
        double r6087753 = r6087752 - r6087745;
        double r6087754 = r6087752 * r6087753;
        double r6087755 = r6087752 - r6087746;
        double r6087756 = r6087754 * r6087755;
        double r6087757 = r6087752 - r6087748;
        double r6087758 = r6087756 * r6087757;
        double r6087759 = sqrt(r6087758);
        return r6087759;
}

↓

double f(double a, double b, double c) {
        double r6087760 = a;
        double r6087761 = b;
        double r6087762 = r6087760 + r6087761;
        double r6087763 = c;
        double r6087764 = r6087762 + r6087763;
        double r6087765 = 2.0;
        double r6087766 = /* ERROR: no posit support in C */;
        double r6087767 = r6087764 / r6087766;
        double r6087768 = r6087767 - r6087760;
        double r6087769 = r6087767 - r6087761;
        double r6087770 = r6087768 * r6087769;
        double r6087771 = r6087767 * r6087770;
        double r6087772 = r6087767 * r6087767;
        double r6087773 = r6087763 * r6087763;
        double r6087774 = r6087772 - r6087773;
        double r6087775 = r6087767 + r6087763;
        double r6087776 = r6087774 / r6087775;
        double r6087777 = r6087771 * r6087776;
        double r6087778 = sqrt(r6087777);
        return r6087778;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Derivation

1. Initial program 0.1

   \[\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 associate-*l* 0.1

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

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

6. Final simplification 0.2

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

Reproduce

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