Average Error: 0.9 → 0.6
Time: 1.2m
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{\alpha + \beta}{\left(\left(i \cdot 2 + 2.0\right) + \alpha\right) + \beta} \cdot \frac{\beta - \alpha}{\left(\beta + \alpha\right) + i \cdot 2} + 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{\alpha + \beta}{\left(\left(i \cdot 2 + 2.0\right) + \alpha\right) + \beta} \cdot \frac{\beta - \alpha}{\left(\beta + \alpha\right) + i \cdot 2} + 1.0}{2.0}
double f(double alpha, double beta, double i) {
        double r604382 = alpha;
        double r604383 = beta;
        double r604384 = r604382 + r604383;
        double r604385 = r604383 - r604382;
        double r604386 = r604384 * r604385;
        double r604387 = 2.0;
        double r604388 = /* ERROR: no posit support in C */;
        double r604389 = i;
        double r604390 = r604388 * r604389;
        double r604391 = r604384 + r604390;
        double r604392 = r604386 / r604391;
        double r604393 = 2.0;
        double r604394 = /* ERROR: no posit support in C */;
        double r604395 = r604391 + r604394;
        double r604396 = r604392 / r604395;
        double r604397 = 1.0;
        double r604398 = /* ERROR: no posit support in C */;
        double r604399 = r604396 + r604398;
        double r604400 = r604399 / r604394;
        return r604400;
}
↓
double f(double alpha, double beta, double i) {
        double r604401 = alpha;
        double r604402 = beta;
        double r604403 = r604401 + r604402;
        double r604404 = i;
        double r604405 = 2.0;
        double r604406 = r604404 * r604405;
        double r604407 = 2.0;
        double r604408 = r604406 + r604407;
        double r604409 = r604408 + r604401;
        double r604410 = r604409 + r604402;
        double r604411 = r604403 / r604410;
        double r604412 = r604402 - r604401;
        double r604413 = r604402 + r604401;
        double r604414 = r604413 + r604406;
        double r604415 = r604412 / r604414;
        double r604416 = r604411 * r604415;
        double r604417 = 1.0;
        double r604418 = r604416 + r604417;
        double r604419 = r604418 / r604407;
        return r604419;
}

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

  3. Applied *p16-rgt-identity-expand0.9

    \[\leadsto \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)}{\color{blue}{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}{\left(2.0\right)}\right) \cdot \left(1.0\right)\right)}}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  4. Applied p16-*-un-lft-identity0.9

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

  5. Applied p16-times-frac0.6

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

  6. Applied p16-times-frac0.6

    \[\leadsto \frac{\left(\frac{\color{blue}{\left(\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\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) \cdot \left(\frac{\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right)}{\left(1.0\right)}\right)\right)}}{\left(1.0\right)}\right)}{\left(2.0\right)}\]

  7. Simplified0.6

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

  8. Simplified0.6

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

  10. Applied p16-*-un-lft-identity0.6

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

  11. Applied *p16-lft-identity-expand0.6

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

  12. Applied p16-times-frac0.6

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

  13. Applied associate-*r*0.6

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

  14. Simplified0.6

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

  16. Applied associate-+r+0.6

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

  17. Final simplification0.6

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

Reproduce

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