Area of a triangle

Average Error: 0.2 → 0.1

Time: 1.0m

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

C

double f(double a, double b, double c) {
        double r4937838 = a;
        double r4937839 = b;
        double r4937840 = r4937838 + r4937839;
        double r4937841 = c;
        double r4937842 = r4937840 + r4937841;
        double r4937843 = 2.0;
        double r4937844 = /* ERROR: no posit support in C */;
        double r4937845 = r4937842 / r4937844;
        double r4937846 = r4937845 - r4937838;
        double r4937847 = r4937845 * r4937846;
        double r4937848 = r4937845 - r4937839;
        double r4937849 = r4937847 * r4937848;
        double r4937850 = r4937845 - r4937841;
        double r4937851 = r4937849 * r4937850;
        double r4937852 = sqrt(r4937851);
        return r4937852;
}

↓

double f(double a, double b, double c) {
        double r4937853 = a;
        double r4937854 = b;
        double r4937855 = r4937853 + r4937854;
        double r4937856 = c;
        double r4937857 = r4937855 + r4937856;
        double r4937858 = 2.0;
        double r4937859 = r4937857 / r4937858;
        double r4937860 = r4937856 + r4937854;
        double r4937861 = r4937853 + r4937860;
        double r4937862 = r4937861 / r4937858;
        double r4937863 = r4937862 - r4937853;
        double r4937864 = r4937859 * r4937863;
        double r4937865 = r4937853 + r4937856;
        double r4937866 = r4937854 + r4937865;
        double r4937867 = r4937866 / r4937858;
        double r4937868 = r4937867 - r4937854;
        double r4937869 = /*Error: no posit support in C */;
        double r4937870 = /*Error: no posit support in C */;
        double r4937871 = r4937864 * r4937870;
        double r4937872 = r4937859 - r4937856;
        double r4937873 = r4937871 * r4937872;
        double r4937874 = sqrt(r4937873);
        return r4937874;
}

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-rgt-identity-expand 0.2

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

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

5. Applied p16-times-frac 0.2

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

6. Applied associate-*l* 0.2

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

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

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

11. Simplified 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{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\frac{\left(\left(\frac{b}{\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right)}\right) \cdot \left(\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right) - b\right)\right)}{\color{blue}{\left(\frac{b}{\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\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. Using strategy rm

13. Applied introduce-quire 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{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \color{blue}{\left(\left(\left(\frac{\left(\left(\frac{b}{\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right)}\right) \cdot \left(\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right) - b\right)\right)}{\left(\frac{b}{\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right)}\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)}\]

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

15. Final simplification 0.1

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

Reproduce

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