Average Error: 0.9 → 0.6
Time: 52.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{\alpha + \beta}{1.0}}{\left(\left(\beta + \left(\alpha + 2 \cdot i\right)\right) \cdot \frac{1.0}{\beta - \alpha}\right) \cdot \frac{\left(\left(\beta + \alpha\right) + i \cdot 2\right) + 2.0}{1.0}} + 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{\alpha + \beta}{1.0}}{\left(\left(\beta + \left(\alpha + 2 \cdot i\right)\right) \cdot \frac{1.0}{\beta - \alpha}\right) \cdot \frac{\left(\left(\beta + \alpha\right) + i \cdot 2\right) + 2.0}{1.0}} + 1.0}{2.0}
double f(double alpha, double beta, double i) {
        double r1324045 = alpha;
        double r1324046 = beta;
        double r1324047 = r1324045 + r1324046;
        double r1324048 = r1324046 - r1324045;
        double r1324049 = r1324047 * r1324048;
        double r1324050 = 2.0;
        double r1324051 = /* ERROR: no posit support in C */;
        double r1324052 = i;
        double r1324053 = r1324051 * r1324052;
        double r1324054 = r1324047 + r1324053;
        double r1324055 = r1324049 / r1324054;
        double r1324056 = 2.0;
        double r1324057 = /* ERROR: no posit support in C */;
        double r1324058 = r1324054 + r1324057;
        double r1324059 = r1324055 / r1324058;
        double r1324060 = 1.0;
        double r1324061 = /* ERROR: no posit support in C */;
        double r1324062 = r1324059 + r1324061;
        double r1324063 = r1324062 / r1324057;
        return r1324063;
}

double f(double alpha, double beta, double i) {
        double r1324064 = alpha;
        double r1324065 = beta;
        double r1324066 = r1324064 + r1324065;
        double r1324067 = 1.0;
        double r1324068 = r1324066 / r1324067;
        double r1324069 = 2.0;
        double r1324070 = i;
        double r1324071 = r1324069 * r1324070;
        double r1324072 = r1324064 + r1324071;
        double r1324073 = r1324065 + r1324072;
        double r1324074 = r1324065 - r1324064;
        double r1324075 = r1324067 / r1324074;
        double r1324076 = r1324073 * r1324075;
        double r1324077 = r1324065 + r1324064;
        double r1324078 = r1324070 * r1324069;
        double r1324079 = r1324077 + r1324078;
        double r1324080 = 2.0;
        double r1324081 = r1324079 + r1324080;
        double r1324082 = r1324081 / r1324067;
        double r1324083 = r1324076 * r1324082;
        double r1324084 = r1324068 / r1324083;
        double r1324085 = r1324084 + r1324067;
        double r1324086 = r1324085 / r1324080;
        return r1324086;
}

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-*-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(\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)}\]
  4. 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(\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)}\]
  5. Applied associate-/l*0.6

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

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\right)}\right)}{\color{blue}{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}{\left(2.0\right)}\right)}{\left(\beta - \alpha\right)}\right)\right)}}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  7. Using strategy rm
  8. Applied *p16-rgt-identity-expand0.6

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\right)}\right)}{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}{\left(2.0\right)}\right)}{\color{blue}{\left(\left(\beta - \alpha\right) \cdot \left(1.0\right)\right)}}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  9. Applied p16-*-un-lft-identity0.6

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\right)}\right)}{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}{\color{blue}{\left(\left(1.0\right) \cdot \left(2.0\right)\right)}}\right)}{\left(\left(\beta - \alpha\right) \cdot \left(1.0\right)\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  10. Applied p16-*-un-lft-identity0.6

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\right)}\right)}{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right) \cdot \left(\frac{\left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)\right)}}{\left(\left(1.0\right) \cdot \left(2.0\right)\right)}\right)}{\left(\left(\beta - \alpha\right) \cdot \left(1.0\right)\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  11. Applied distribute-lft-out0.6

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\right)}\right)}{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right) \cdot \left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}{\left(2.0\right)}\right)\right)}}{\left(\left(\beta - \alpha\right) \cdot \left(1.0\right)\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  12. Applied p16-times-frac0.7

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\right)}\right)}{\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right) \cdot \color{blue}{\left(\left(\frac{\left(1.0\right)}{\left(\beta - \alpha\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}{\left(2.0\right)}\right)}{\left(1.0\right)}\right)\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  13. Applied associate-*r*0.7

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\right)}\right)}{\color{blue}{\left(\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\left(\beta - \alpha\right)}\right)\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}{\left(2.0\right)}\right)}{\left(1.0\right)}\right)\right)}}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  14. Using strategy rm
  15. Applied p16-*-un-lft-identity0.7

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\right)}\right)}{\left(\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\color{blue}{\left(\left(1.0\right) \cdot \left(\beta - \alpha\right)\right)}}\right)\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}{\left(2.0\right)}\right)}{\left(1.0\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  16. Applied p16-*-un-lft-identity0.7

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\right)}\right)}{\left(\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right) \cdot \left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \left(1.0\right)\right)}}{\left(\left(1.0\right) \cdot \left(\beta - \alpha\right)\right)}\right)\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}{\left(2.0\right)}\right)}{\left(1.0\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  17. Applied p16-times-frac0.7

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(1.0\right)}\right)}{\left(\left(\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right) \cdot \color{blue}{\left(\left(\frac{\left(1.0\right)}{\left(1.0\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\left(\beta - \alpha\right)}\right)\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\frac{\beta}{\alpha}\right)}{\left(i \cdot \left(2\right)\right)}\right)}{\left(2.0\right)}\right)}{\left(1.0\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
  18. Applied associate-*r*0.7

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

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

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

Reproduce

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