Average Error: 0.7 → 0.7
Time: 29.7s
Precision: 64
\[\alpha \gt \left(-1\right) \land \beta \gt \left(-1\right)\]
\[\frac{\left(\frac{\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}\]
↓
\[\frac{\left(\frac{1.0}{\left(\alpha + \beta\right) + 2.0} \cdot \beta + \frac{1.0}{\left(\alpha + \beta\right) + 2.0} \cdot \left(-\alpha\right)\right) + 1.0}{2.0}\]
\frac{\left(\frac{\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(2.0\right)}\right)}\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}
↓
\frac{\left(\frac{1.0}{\left(\alpha + \beta\right) + 2.0} \cdot \beta + \frac{1.0}{\left(\alpha + \beta\right) + 2.0} \cdot \left(-\alpha\right)\right) + 1.0}{2.0}
double f(double alpha, double beta) {
        double r295114 = beta;
        double r295115 = alpha;
        double r295116 = r295114 - r295115;
        double r295117 = r295115 + r295114;
        double r295118 = 2.0;
        double r295119 = /* ERROR: no posit support in C */;
        double r295120 = r295117 + r295119;
        double r295121 = r295116 / r295120;
        double r295122 = 1.0;
        double r295123 = /* ERROR: no posit support in C */;
        double r295124 = r295121 + r295123;
        double r295125 = r295124 / r295119;
        return r295125;
}
↓
double f(double alpha, double beta) {
        double r295126 = 1.0;
        double r295127 = alpha;
        double r295128 = beta;
        double r295129 = r295127 + r295128;
        double r295130 = 2.0;
        double r295131 = r295129 + r295130;
        double r295132 = r295126 / r295131;
        double r295133 = r295132 * r295128;
        double r295134 = -r295127;
        double r295135 = r295132 * r295134;
        double r295136 = r295133 + r295135;
        double r295137 = r295136 + r295126;
        double r295138 = r295137 / r295130;
        return r295138;
}

Error

Bits error versus alpha

Bits error versus beta

Derivation

  1. Initial program 0.7

    \[\frac{\left(\frac{\left(\frac{\left(\beta - \alpha\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\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.7

    \[\leadsto \frac{\left(\frac{\left(\frac{\left(\beta - \alpha\right)}{\color{blue}{\left(\left(\frac{\left(\frac{\alpha}{\beta}\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.7

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

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

  6. Simplified0.8

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

  8. Applied sub-neg0.8

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

  9. Applied distribute-lft-in0.7

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

  10. Final simplification0.7

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

Reproduce

herbie shell --seed 2019153 +o rules:numerics
(FPCore (alpha beta)
  :name "Octave 3.8, jcobi/1"
  :pre (and (>.p16 alpha (real->posit16 -1)) (>.p16 beta (real->posit16 -1)))
  (/.p16 (+.p16 (/.p16 (-.p16 beta alpha) (+.p16 (+.p16 alpha beta) (real->posit16 2.0))) (real->posit16 1.0)) (real->posit16 2.0)))