expq3 (problem 3.4.2)

Average Error: 58.7 → 51.3

Time: 40.9s

Precision: 64

• could not determine a ground truth for program body

  1. a = 3.5687599324611755e+225
  2. b = -5.061019812820809e-154
  3. eps = 4.894273457956471e-203

\[-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)}\]

↓

\[\begin{array}{l} \mathbf{if}\;b \le -0.020571153449468284:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right)}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(\varepsilon \cdot \left(\left(a \cdot \left(\varepsilon \cdot a\right)\right) \cdot \frac{1}{2} + \left(a + \left(a \cdot \left(\varepsilon \cdot a\right)\right) \cdot \left(\frac{1}{6} \cdot \left(\varepsilon \cdot a\right)\right)\right)\right)\right)}\\ \mathbf{elif}\;b \le 7.448916943974044 \cdot 10^{+141}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right)}{\left(\left(\varepsilon \cdot \frac{1}{6}\right) \cdot \left(\left(\left(\varepsilon \cdot b\right) \cdot \left(\varepsilon \cdot b\right)\right) \cdot b\right) + \left(\varepsilon \cdot b + \left(\varepsilon \cdot b\right) \cdot \left(\frac{1}{2} \cdot \left(\varepsilon \cdot b\right)\right)\right)\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right)}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(\varepsilon \cdot \left(\left(a \cdot \left(\varepsilon \cdot a\right)\right) \cdot \frac{1}{2} + \left(a + \left(a \cdot \left(\varepsilon \cdot a\right)\right) \cdot \left(\frac{1}{6} \cdot \left(\varepsilon \cdot a\right)\right)\right)\right)\right)}\\ \end{array}\]

C

double f(double a, double b, double eps) {
        double r3568373 = eps;
        double r3568374 = a;
        double r3568375 = b;
        double r3568376 = r3568374 + r3568375;
        double r3568377 = r3568376 * r3568373;
        double r3568378 = exp(r3568377);
        double r3568379 = 1.0;
        double r3568380 = r3568378 - r3568379;
        double r3568381 = r3568373 * r3568380;
        double r3568382 = r3568374 * r3568373;
        double r3568383 = exp(r3568382);
        double r3568384 = r3568383 - r3568379;
        double r3568385 = r3568375 * r3568373;
        double r3568386 = exp(r3568385);
        double r3568387 = r3568386 - r3568379;
        double r3568388 = r3568384 * r3568387;
        double r3568389 = r3568381 / r3568388;
        return r3568389;
}

↓

double f(double a, double b, double eps) {
        double r3568390 = b;
        double r3568391 = -0.020571153449468284;
        bool r3568392 = r3568390 <= r3568391;
        double r3568393 = eps;
        double r3568394 = a;
        double r3568395 = r3568390 + r3568394;
        double r3568396 = r3568393 * r3568395;
        double r3568397 = exp(r3568396);
        double r3568398 = 1.0;
        double r3568399 = r3568397 - r3568398;
        double r3568400 = r3568393 * r3568399;
        double r3568401 = r3568393 * r3568390;
        double r3568402 = exp(r3568401);
        double r3568403 = r3568402 - r3568398;
        double r3568404 = r3568393 * r3568394;
        double r3568405 = r3568394 * r3568404;
        double r3568406 = 0.5;
        double r3568407 = r3568405 * r3568406;
        double r3568408 = 0.16666666666666666;
        double r3568409 = r3568408 * r3568404;
        double r3568410 = r3568405 * r3568409;
        double r3568411 = r3568394 + r3568410;
        double r3568412 = r3568407 + r3568411;
        double r3568413 = r3568393 * r3568412;
        double r3568414 = r3568403 * r3568413;
        double r3568415 = r3568400 / r3568414;
        double r3568416 = 7.448916943974044e+141;
        bool r3568417 = r3568390 <= r3568416;
        double r3568418 = r3568393 * r3568408;
        double r3568419 = r3568401 * r3568401;
        double r3568420 = r3568419 * r3568390;
        double r3568421 = r3568418 * r3568420;
        double r3568422 = r3568406 * r3568401;
        double r3568423 = r3568401 * r3568422;
        double r3568424 = r3568401 + r3568423;
        double r3568425 = r3568421 + r3568424;
        double r3568426 = exp(r3568404);
        double r3568427 = r3568426 - r3568398;
        double r3568428 = r3568425 * r3568427;
        double r3568429 = r3568400 / r3568428;
        double r3568430 = r3568417 ? r3568429 : r3568415;
        double r3568431 = r3568392 ? r3568415 : r3568430;
        return r3568431;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	58.7
Target	14.7
Herbie	51.3

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

Derivation

1. Split input into 2 regimes

2. if b < -0.020571153449468284 or 7.448916943974044e+141 < b

   1. Initial program 53.2

      \[\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 47.2

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\color{blue}{\left(\frac{1}{2} \cdot \left({a}^{2} \cdot {\varepsilon}^{2}\right) + \left(\frac{1}{6} \cdot \left({a}^{3} \cdot {\varepsilon}^{3}\right) + a \cdot \varepsilon\right)\right)} \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\]

   3. Simplified 44.1

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\color{blue}{\left(\varepsilon \cdot \left(\frac{1}{6} \cdot \left(\left(\left(\varepsilon \cdot a\right) \cdot \left(\varepsilon \cdot a\right)\right) \cdot a\right) + \left(a \cdot \frac{1}{2}\right) \cdot \left(\varepsilon \cdot a\right)\right) + \varepsilon \cdot a\right)} \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\]
   4. Using strategy rm

   5. Applied *-un-lft-identity 44.1

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(\varepsilon \cdot \left(\frac{1}{6} \cdot \left(\left(\left(\varepsilon \cdot a\right) \cdot \left(\varepsilon \cdot a\right)\right) \cdot a\right) + \left(a \cdot \frac{1}{2}\right) \cdot \left(\varepsilon \cdot a\right)\right) + \varepsilon \cdot a\right) \cdot \color{blue}{\left(1 \cdot \left(e^{b \cdot \varepsilon} - 1\right)\right)}}\]

   6. Applied associate-*r* 44.1

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\color{blue}{\left(\left(\varepsilon \cdot \left(\frac{1}{6} \cdot \left(\left(\left(\varepsilon \cdot a\right) \cdot \left(\varepsilon \cdot a\right)\right) \cdot a\right) + \left(a \cdot \frac{1}{2}\right) \cdot \left(\varepsilon \cdot a\right)\right) + \varepsilon \cdot a\right) \cdot 1\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}}\]

   7. Simplified 44.0

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\color{blue}{\left(\left(\left(a + \left(\frac{1}{6} \cdot \left(\varepsilon \cdot a\right)\right) \cdot \left(\left(\varepsilon \cdot a\right) \cdot a\right)\right) + \left(\left(\varepsilon \cdot a\right) \cdot a\right) \cdot \frac{1}{2}\right) \cdot \varepsilon\right)} \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\]

   if -0.020571153449468284 < b < 7.448916943974044e+141

   1. Initial program 61.3

      \[\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 55.1

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \color{blue}{\left(\varepsilon \cdot b + \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot {b}^{2}\right) + \frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot {b}^{3}\right)\right)\right)}}\]

   3. Simplified 54.9

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \color{blue}{\left(\left(\varepsilon \cdot b + \left(\frac{1}{2} \cdot \left(\varepsilon \cdot b\right)\right) \cdot \left(\varepsilon \cdot b\right)\right) + \left(\frac{1}{6} \cdot \varepsilon\right) \cdot \left(\left(\left(b \cdot \varepsilon\right) \cdot \left(b \cdot \varepsilon\right)\right) \cdot b\right)\right)}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 51.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \le -0.020571153449468284:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right)}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(\varepsilon \cdot \left(\left(a \cdot \left(\varepsilon \cdot a\right)\right) \cdot \frac{1}{2} + \left(a + \left(a \cdot \left(\varepsilon \cdot a\right)\right) \cdot \left(\frac{1}{6} \cdot \left(\varepsilon \cdot a\right)\right)\right)\right)\right)}\\ \mathbf{elif}\;b \le 7.448916943974044 \cdot 10^{+141}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right)}{\left(\left(\varepsilon \cdot \frac{1}{6}\right) \cdot \left(\left(\left(\varepsilon \cdot b\right) \cdot \left(\varepsilon \cdot b\right)\right) \cdot b\right) + \left(\varepsilon \cdot b + \left(\varepsilon \cdot b\right) \cdot \left(\frac{1}{2} \cdot \left(\varepsilon \cdot b\right)\right)\right)\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right)}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(\varepsilon \cdot \left(\left(a \cdot \left(\varepsilon \cdot a\right)\right) \cdot \frac{1}{2} + \left(a + \left(a \cdot \left(\varepsilon \cdot a\right)\right) \cdot \left(\frac{1}{6} \cdot \left(\varepsilon \cdot a\right)\right)\right)\right)\right)}\\ \end{array}\]

Reproduce

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