Average Error: 0.7 → 0.8
Time: 3.4m
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{\left(\left(\beta - \alpha\right) \cdot \left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(2.0\right)}\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\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{\left(\left(\beta - \alpha\right) \cdot \left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\alpha}{\beta}\right)}{\left(2.0\right)}\right)}\right)\right)}{\left(1.0\right)}\right)}{\left(2.0\right)}
double f(double alpha, double beta) {
        double r5189506 = beta;
        double r5189507 = alpha;
        double r5189508 = r5189506 - r5189507;
        double r5189509 = r5189507 + r5189506;
        double r5189510 = 2.0;
        double r5189511 = /* ERROR: no posit support in C */;
        double r5189512 = r5189509 + r5189511;
        double r5189513 = r5189508 / r5189512;
        double r5189514 = 1.0;
        double r5189515 = /* ERROR: no posit support in C */;
        double r5189516 = r5189513 + r5189515;
        double r5189517 = r5189516 / r5189511;
        return r5189517;
}
↓
double f(double alpha, double beta) {
        double r5189518 = beta;
        double r5189519 = alpha;
        double r5189520 = r5189518 - r5189519;
        double r5189521 = 1.0;
        double r5189522 = /* ERROR: no posit support in C */;
        double r5189523 = r5189519 + r5189518;
        double r5189524 = 2.0;
        double r5189525 = /* ERROR: no posit support in C */;
        double r5189526 = r5189523 + r5189525;
        double r5189527 = r5189522 / r5189526;
        double r5189528 = r5189520 * r5189527;
        double r5189529 = r5189528 + r5189522;
        double r5189530 = r5189529 / r5189525;
        return r5189530;
}

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-*-un-lft-identity0.7

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

  5. Applied distribute-lft-out0.7

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

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

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

  7. Applied p16-times-frac0.8

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

  8. Simplified0.8

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

  9. Final simplification0.8

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

Reproduce

herbie shell --seed 2019168 +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)))