Average Error: 1.0 → 0.6
Time: 1.6m
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{1.0}{\left(\alpha + \beta\right) + 2 \cdot i} \cdot \left(\beta + \alpha\right)}{\frac{\left(\alpha + \left(\beta + 2 \cdot i\right)\right) + 2.0}{\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{1.0}{\left(\alpha + \beta\right) + 2 \cdot i} \cdot \left(\beta + \alpha\right)}{\frac{\left(\alpha + \left(\beta + 2 \cdot i\right)\right) + 2.0}{\beta - \alpha}} + 1.0}{2.0}
double f(double alpha, double beta, double i) {
        double r1523000 = alpha;
        double r1523001 = beta;
        double r1523002 = r1523000 + r1523001;
        double r1523003 = r1523001 - r1523000;
        double r1523004 = r1523002 * r1523003;
        double r1523005 = 2.0;
        double r1523006 = /* ERROR: no posit support in C */;
        double r1523007 = i;
        double r1523008 = r1523006 * r1523007;
        double r1523009 = r1523002 + r1523008;
        double r1523010 = r1523004 / r1523009;
        double r1523011 = 2.0;
        double r1523012 = /* ERROR: no posit support in C */;
        double r1523013 = r1523009 + r1523012;
        double r1523014 = r1523010 / r1523013;
        double r1523015 = 1.0;
        double r1523016 = /* ERROR: no posit support in C */;
        double r1523017 = r1523014 + r1523016;
        double r1523018 = r1523017 / r1523012;
        return r1523018;
}
↓
double f(double alpha, double beta, double i) {
        double r1523019 = 1.0;
        double r1523020 = alpha;
        double r1523021 = beta;
        double r1523022 = r1523020 + r1523021;
        double r1523023 = 2.0;
        double r1523024 = i;
        double r1523025 = r1523023 * r1523024;
        double r1523026 = r1523022 + r1523025;
        double r1523027 = r1523019 / r1523026;
        double r1523028 = r1523021 + r1523020;
        double r1523029 = r1523027 * r1523028;
        double r1523030 = r1523021 + r1523025;
        double r1523031 = r1523020 + r1523030;
        double r1523032 = 2.0;
        double r1523033 = r1523031 + r1523032;
        double r1523034 = r1523021 - r1523020;
        double r1523035 = r1523033 / r1523034;
        double r1523036 = r1523029 / r1523035;
        double r1523037 = r1523036 + r1523019;
        double r1523038 = r1523037 / r1523032;
        return r1523038;
}

Error

Bits error versus alpha

Bits error versus beta

Bits error versus i

Derivation

  1. Initial program 1.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)}\]
  2. Using strategy rm

  3. Applied *p16-rgt-identity-expand1.0

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

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(\left(2\right) \cdot i\right)}\right)}\right) \cdot \color{blue}{\left(\beta - \alpha\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)}\]
  6. Using strategy rm

  7. Applied associate-+l+0.6

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

  9. Applied associate-/l*0.6

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

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

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

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

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

  13. Applied p16-times-frac0.6

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

  14. Simplified0.6

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

  15. Final simplification0.6

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

Reproduce

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