expq3 (problem 3.4.2)

Average Error: 60.4 → 0.3

Time: 15.7s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

• could not determine a ground truth for program body

  1. a = -5.670122129476186e-07
  2. b = 1.61157953583811e+280
  3. eps = 1.4915374553808526e-197

\[-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 9.1684011556905069 \cdot 10^{-11}\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 r87456 = eps;
        double r87457 = a;
        double r87458 = b;
        double r87459 = r87457 + r87458;
        double r87460 = r87459 * r87456;
        double r87461 = exp(r87460);
        double r87462 = 1.0;
        double r87463 = r87461 - r87462;
        double r87464 = r87456 * r87463;
        double r87465 = r87457 * r87456;
        double r87466 = exp(r87465);
        double r87467 = r87466 - r87462;
        double r87468 = r87458 * r87456;
        double r87469 = exp(r87468);
        double r87470 = r87469 - r87462;
        double r87471 = r87467 * r87470;
        double r87472 = r87464 / r87471;
        return r87472;
}

↓

double f(double a, double b, double eps) {
        double r87473 = eps;
        double r87474 = a;
        double r87475 = b;
        double r87476 = r87474 + r87475;
        double r87477 = r87476 * r87473;
        double r87478 = exp(r87477);
        double r87479 = 1.0;
        double r87480 = r87478 - r87479;
        double r87481 = r87473 * r87480;
        double r87482 = r87474 * r87473;
        double r87483 = exp(r87482);
        double r87484 = r87483 - r87479;
        double r87485 = r87475 * r87473;
        double r87486 = exp(r87485);
        double r87487 = r87486 - r87479;
        double r87488 = r87484 * r87487;
        double r87489 = r87481 / r87488;
        double r87490 = -inf.0;
        bool r87491 = r87489 <= r87490;
        double r87492 = 9.168401155690507e-11;
        bool r87493 = r87489 <= r87492;
        double r87494 = !r87493;
        bool r87495 = r87491 || r87494;
        double r87496 = 1.0;
        double r87497 = r87496 / r87475;
        double r87498 = r87496 / r87474;
        double r87499 = r87497 + r87498;
        double r87500 = r87495 ? r87499 : r87489;
        return r87500;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	60.4
Target	14.6
Herbie	0.3

\[\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 9.168401155690507e-11 < (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0)))

   1. Initial program 63.9

      \[\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.1

      \[\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))) < 9.168401155690507e-11

   1. Initial program 3.9

      \[\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.3

   \[\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 9.1684011556905069 \cdot 10^{-11}\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 2020043 
(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))))