Average Error: 0.2 → 0.2
Time: 1.1m
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 \frac{1.0}{\frac{\frac{\left(a + b\right) + c}{2} + b}{\frac{\left(a + b\right) + c}{2} \cdot \frac{\left(a + b\right) + c}{2} - b \cdot b}}\right) \cdot \frac{\frac{\left(a + b\right) + c}{2} \cdot \frac{\left(a + b\right) + c}{2} - c \cdot c}{\frac{\left(a + b\right) + c}{2} + 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 \frac{1.0}{\frac{\frac{\left(a + b\right) + c}{2} + b}{\frac{\left(a + b\right) + c}{2} \cdot \frac{\left(a + b\right) + c}{2} - b \cdot b}}\right) \cdot \frac{\frac{\left(a + b\right) + c}{2} \cdot \frac{\left(a + b\right) + c}{2} - c \cdot c}{\frac{\left(a + b\right) + c}{2} + c}}
double f(double a, double b, double c) {
        double r1916048 = a;
        double r1916049 = b;
        double r1916050 = r1916048 + r1916049;
        double r1916051 = c;
        double r1916052 = r1916050 + r1916051;
        double r1916053 = 2.0;
        double r1916054 = /* ERROR: no posit support in C */;
        double r1916055 = r1916052 / r1916054;
        double r1916056 = r1916055 - r1916048;
        double r1916057 = r1916055 * r1916056;
        double r1916058 = r1916055 - r1916049;
        double r1916059 = r1916057 * r1916058;
        double r1916060 = r1916055 - r1916051;
        double r1916061 = r1916059 * r1916060;
        double r1916062 = sqrt(r1916061);
        return r1916062;
}
↓
double f(double a, double b, double c) {
        double r1916063 = a;
        double r1916064 = b;
        double r1916065 = r1916063 + r1916064;
        double r1916066 = c;
        double r1916067 = r1916065 + r1916066;
        double r1916068 = 2.0;
        double r1916069 = r1916067 / r1916068;
        double r1916070 = r1916069 - r1916063;
        double r1916071 = r1916069 * r1916070;
        double r1916072 = 1.0;
        double r1916073 = r1916069 + r1916064;
        double r1916074 = r1916069 * r1916069;
        double r1916075 = r1916064 * r1916064;
        double r1916076 = r1916074 - r1916075;
        double r1916077 = r1916073 / r1916076;
        double r1916078 = r1916072 / r1916077;
        double r1916079 = r1916071 * r1916078;
        double r1916080 = r1916066 * r1916066;
        double r1916081 = r1916074 - r1916080;
        double r1916082 = r1916069 + r1916066;
        double r1916083 = r1916081 / r1916082;
        double r1916084 = r1916079 * r1916083;
        double r1916085 = sqrt(r1916084);
        return r1916085;
}

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 \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 \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)}\]
  4. Using strategy rm

  5. Applied p16-flip--0.3

    \[\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 \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(\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. Using strategy rm

  7. Applied p16-*-un-lft-identity0.3

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

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

  9. Final simplification0.2

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

Reproduce

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