expq3 (problem 3.4.2)

Average Error: 58.8 → 3.2

Time: 33.2s

Precision: 64

• could not determine a ground truth for program body

  1. a = -2.105764741467786e-34
  2. b = -9.597775684611915e+235
  3. eps = -1.591634704085632e-69

\[-1 \lt \varepsilon \land \varepsilon \lt 1\]

Math

\[\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\]

↓

\[\frac{1}{a} + \frac{1}{b}\]

C

double f(double a, double b, double eps) {
        double r3000253 = eps;
        double r3000254 = a;
        double r3000255 = b;
        double r3000256 = r3000254 + r3000255;
        double r3000257 = r3000256 * r3000253;
        double r3000258 = exp(r3000257);
        double r3000259 = 1.0;
        double r3000260 = r3000258 - r3000259;
        double r3000261 = r3000253 * r3000260;
        double r3000262 = r3000254 * r3000253;
        double r3000263 = exp(r3000262);
        double r3000264 = r3000263 - r3000259;
        double r3000265 = r3000255 * r3000253;
        double r3000266 = exp(r3000265);
        double r3000267 = r3000266 - r3000259;
        double r3000268 = r3000264 * r3000267;
        double r3000269 = r3000261 / r3000268;
        return r3000269;
}

↓

double f(double a, double b, double __attribute__((unused)) eps) {
        double r3000270 = 1.0;
        double r3000271 = a;
        double r3000272 = r3000270 / r3000271;
        double r3000273 = b;
        double r3000274 = r3000270 / r3000273;
        double r3000275 = r3000272 + r3000274;
        return r3000275;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	58.8
Target	13.6
Herbie	3.2

\[\frac{a + b}{a \cdot b}\]

Derivation

1. Initial program 58.8

   \[\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\]

2. Taylor expanded around 0 3.2

   \[\leadsto \color{blue}{\frac{1}{a} + \frac{1}{b}}\]

3. Final simplification 3.2

   \[\leadsto \frac{1}{a} + \frac{1}{b}\]

Reproduce

herbie shell --seed 2019144 
(FPCore (a b eps)
  :name "expq3 (problem 3.4.2)"
  :pre (and (< -1 eps) (< eps 1))

  :herbie-target
  (/ (+ a b) (* a b))

  (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))))