expq3 (problem 3.4.2)

Average Error: 60.3 → 0.8

Time: 33.0s

Precision: 64

• could not determine a ground truth for program body

  1. a = -5.278031834180875e+72
  2. b = -5.9461326997729256e+41
  3. eps = -2.3299265771866867e-17

\[-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}\;\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)} = -\infty \lor \neg \left(\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)} \le 1.492763212396486590455423330799142226004 \cdot 10^{-92}\right):\\ \;\;\;\;\frac{1}{b} + \frac{1}{a}\\ \mathbf{else}:\\ \;\;\;\;\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)}\\ \end{array}\]

C

double f(double a, double b, double eps) {
        double r83410 = eps;
        double r83411 = a;
        double r83412 = b;
        double r83413 = r83411 + r83412;
        double r83414 = r83413 * r83410;
        double r83415 = exp(r83414);
        double r83416 = 1.0;
        double r83417 = r83415 - r83416;
        double r83418 = r83410 * r83417;
        double r83419 = r83411 * r83410;
        double r83420 = exp(r83419);
        double r83421 = r83420 - r83416;
        double r83422 = r83412 * r83410;
        double r83423 = exp(r83422);
        double r83424 = r83423 - r83416;
        double r83425 = r83421 * r83424;
        double r83426 = r83418 / r83425;
        return r83426;
}

↓

double f(double a, double b, double eps) {
        double r83427 = eps;
        double r83428 = a;
        double r83429 = b;
        double r83430 = r83428 + r83429;
        double r83431 = r83430 * r83427;
        double r83432 = exp(r83431);
        double r83433 = 1.0;
        double r83434 = r83432 - r83433;
        double r83435 = r83427 * r83434;
        double r83436 = r83428 * r83427;
        double r83437 = exp(r83436);
        double r83438 = r83437 - r83433;
        double r83439 = r83429 * r83427;
        double r83440 = exp(r83439);
        double r83441 = r83440 - r83433;
        double r83442 = r83438 * r83441;
        double r83443 = r83435 / r83442;
        double r83444 = -inf.0;
        bool r83445 = r83443 <= r83444;
        double r83446 = 1.4927632123964866e-92;
        bool r83447 = r83443 <= r83446;
        double r83448 = !r83447;
        bool r83449 = r83445 || r83448;
        double r83450 = 1.0;
        double r83451 = r83450 / r83429;
        double r83452 = r83450 / r83428;
        double r83453 = r83451 + r83452;
        double r83454 = r83449 ? r83453 : r83443;
        return r83454;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	60.3
Target	15.2
Herbie	0.8

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

Derivation

1. Split input into 2 regimes

2. if (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0))) < -inf.0 or 1.4927632123964866e-92 < (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0)))

   1. Initial program 63.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 0.7

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

   if -inf.0 < (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0))) < 1.4927632123964866e-92

   1. Initial program 3.6

      \[\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)}\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.8

   \[\leadsto \begin{array}{l} \mathbf{if}\;\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)} = -\infty \lor \neg \left(\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)} \le 1.492763212396486590455423330799142226004 \cdot 10^{-92}\right):\\ \;\;\;\;\frac{1}{b} + \frac{1}{a}\\ \mathbf{else}:\\ \;\;\;\;\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)}\\ \end{array}\]

Reproduce

herbie shell --seed 2019323 
(FPCore (a b eps)
  :name "expq3 (problem 3.4.2)"
  :precision binary64
  :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))))