Average Error: 0.2 → 0.1
Time: 47.5s
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(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{a + \left(c + b\right)}{2} - b\right)\right) \cdot \left(\frac{\left(c + b\right) + a}{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(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{a + \left(c + b\right)}{2} - b\right)\right) \cdot \left(\frac{\left(c + b\right) + a}{2} - c\right)}
double f(double a, double b, double c) {
        double r1814833 = a;
        double r1814834 = b;
        double r1814835 = r1814833 + r1814834;
        double r1814836 = c;
        double r1814837 = r1814835 + r1814836;
        double r1814838 = 2.0;
        double r1814839 = /* ERROR: no posit support in C */;
        double r1814840 = r1814837 / r1814839;
        double r1814841 = r1814840 - r1814833;
        double r1814842 = r1814840 * r1814841;
        double r1814843 = r1814840 - r1814834;
        double r1814844 = r1814842 * r1814843;
        double r1814845 = r1814840 - r1814836;
        double r1814846 = r1814844 * r1814845;
        double r1814847 = sqrt(r1814846);
        return r1814847;
}
↓
double f(double a, double b, double c) {
        double r1814848 = a;
        double r1814849 = b;
        double r1814850 = r1814848 + r1814849;
        double r1814851 = c;
        double r1814852 = r1814850 + r1814851;
        double r1814853 = 2.0;
        double r1814854 = r1814852 / r1814853;
        double r1814855 = r1814854 - r1814848;
        double r1814856 = r1814854 * r1814855;
        double r1814857 = r1814851 + r1814849;
        double r1814858 = r1814848 + r1814857;
        double r1814859 = r1814858 / r1814853;
        double r1814860 = r1814859 - r1814849;
        double r1814861 = r1814856 * r1814860;
        double r1814862 = r1814857 + r1814848;
        double r1814863 = r1814862 / r1814853;
        double r1814864 = r1814863 - r1814851;
        double r1814865 = r1814861 * r1814864;
        double r1814866 = sqrt(r1814865);
        return r1814866;
}

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-*-un-lft-identity0.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{\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)}{\color{blue}{\left(\left(1.0\right) \cdot \left(2\right)\right)}}\right) - c\right)\right)}\]

  4. Applied associate-/r*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{\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(\color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(1.0\right)}\right)}{\left(2\right)}\right)} - c\right)\right)}\]

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

  7. Applied p16-*-un-lft-identity0.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{\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)}{\color{blue}{\left(\left(1.0\right) \cdot \left(2\right)\right)}}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) - c\right)\right)}\]

  8. Applied associate-/r*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{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(1.0\right)}\right)}{\left(2\right)}\right)} - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) - c\right)\right)}\]

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

  10. Final simplification0.1

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

Reproduce

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