Average Error: 0.9 → 0.6
Time: 50.9s
Precision: 64
\[\alpha \gt \left(-1\right) \land \beta \gt \left(-1\right) \land i \gt \left(0\right)\]
\[\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
↓
\[\frac{\frac{\frac{\beta - \alpha}{2 \cdot i + \left(\beta + \alpha\right)}}{\frac{\left(2.0 + \left(\beta + \alpha\right)\right) + 2 \cdot i}{\beta + \alpha}} + 1.0}{2.0}\]
\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}
↓
\frac{\frac{\frac{\beta - \alpha}{2 \cdot i + \left(\beta + \alpha\right)}}{\frac{\left(2.0 + \left(\beta + \alpha\right)\right) + 2 \cdot i}{\beta + \alpha}} + 1.0}{2.0}
double f(double alpha, double beta, double i) {
        double r3396364 = alpha;
        double r3396365 = beta;
        double r3396366 = r3396364 + r3396365;
        double r3396367 = r3396365 - r3396364;
        double r3396368 = r3396366 * r3396367;
        double r3396369 = 2.0;
        double r3396370 = /* ERROR: no posit support in C */;
        double r3396371 = i;
        double r3396372 = r3396370 * r3396371;
        double r3396373 = r3396366 + r3396372;
        double r3396374 = r3396368 / r3396373;
        double r3396375 = 2.0;
        double r3396376 = /* ERROR: no posit support in C */;
        double r3396377 = r3396373 + r3396376;
        double r3396378 = r3396374 / r3396377;
        double r3396379 = 1.0;
        double r3396380 = /* ERROR: no posit support in C */;
        double r3396381 = r3396378 + r3396380;
        double r3396382 = r3396381 / r3396376;
        return r3396382;
}
↓
double f(double alpha, double beta, double i) {
        double r3396383 = beta;
        double r3396384 = alpha;
        double r3396385 = r3396383 - r3396384;
        double r3396386 = 2.0;
        double r3396387 = i;
        double r3396388 = r3396386 * r3396387;
        double r3396389 = r3396383 + r3396384;
        double r3396390 = r3396388 + r3396389;
        double r3396391 = r3396385 / r3396390;
        double r3396392 = 2.0;
        double r3396393 = r3396392 + r3396389;
        double r3396394 = r3396393 + r3396388;
        double r3396395 = r3396394 / r3396389;
        double r3396396 = r3396391 / r3396395;
        double r3396397 = 1.0;
        double r3396398 = r3396396 + r3396397;
        double r3396399 = r3396398 / r3396392;
        return r3396399;
}

Error

Bits error versus alpha

Bits error versus beta

Bits error versus i

Derivation

  1. Initial program 0.9

    \[\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\frac{\alpha}{\beta}\right) \cdot \left(\beta - \alpha\right)\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  2. Simplified0.9

    \[\leadsto \color{blue}{\frac{\left(\frac{\left(\frac{\left(\left(\beta - \alpha\right) \cdot \left(\frac{\beta}{\alpha}\right)\right)}{\left(\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(\frac{\beta}{\alpha}\right)}\right) \cdot \left(\frac{\left(\frac{\left(2.0\right)}{\left(\frac{\beta}{\alpha}\right)}\right)}{\left(\left(2\right) \cdot i\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}}\]
  3. Using strategy rm

  4. Applied p16-times-frac0.6

    \[\leadsto \frac{\left(\frac{\color{blue}{\left(\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(\frac{\beta}{\alpha}\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(\frac{\left(\frac{\left(2.0\right)}{\left(\frac{\beta}{\alpha}\right)}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)\right)}}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  5. Using strategy rm

  6. Applied associate-*r/0.6

    \[\leadsto \frac{\left(\frac{\color{blue}{\left(\frac{\left(\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(\frac{\beta}{\alpha}\right)}\right)}\right) \cdot \left(\frac{\beta}{\alpha}\right)\right)}{\left(\frac{\left(\frac{\left(2.0\right)}{\left(\frac{\beta}{\alpha}\right)}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  7. Using strategy rm

  8. Applied associate-/l*0.6

    \[\leadsto \frac{\left(\frac{\color{blue}{\left(\frac{\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\left(2\right) \cdot i\right)}{\left(\frac{\beta}{\alpha}\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(2.0\right)}{\left(\frac{\beta}{\alpha}\right)}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(\frac{\beta}{\alpha}\right)}\right)}\right)}}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  9. Final simplification0.6

    \[\leadsto \frac{\frac{\frac{\beta - \alpha}{2 \cdot i + \left(\beta + \alpha\right)}}{\frac{\left(2.0 + \left(\beta + \alpha\right)\right) + 2 \cdot i}{\beta + \alpha}} + 1.0}{2.0}\]

Reproduce

herbie shell --seed 2019134 
(FPCore (alpha beta i)
  :name "Octave 3.8, jcobi/2"
  :pre (and (>.p16 alpha (real->posit16 -1)) (>.p16 beta (real->posit16 -1)) (>.p16 i (real->posit16 0)))
  (/.p16 (+.p16 (/.p16 (/.p16 (*.p16 (+.p16 alpha beta) (-.p16 beta alpha)) (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i))) (+.p16 (+.p16 (+.p16 alpha beta) (*.p16 (real->posit16 2) i)) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)))