expq3 (problem 3.4.2)

Average Error: 58.8 → 0.6

Time: 29.1s

Precision: 64

• could not determine a ground truth for program body

  1. a = -1.0428622510379046e-74
  2. b = -2.5360604720738347e+179
  3. eps = -6.127530811963465e-117

\[-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{\left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right) \cdot \varepsilon}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)} = -\infty:\\ \;\;\;\;\frac{1}{b} + \frac{1}{a}\\ \mathbf{elif}\;\frac{\left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right) \cdot \varepsilon}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)} \le 2.7242283277550334 \cdot 10^{-62}:\\ \;\;\;\;\frac{\left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right) \cdot \varepsilon}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{b} + \frac{1}{a}\\ \end{array}\]

C

double f(double a, double b, double eps) {
        double r1524334 = eps;
        double r1524335 = a;
        double r1524336 = b;
        double r1524337 = r1524335 + r1524336;
        double r1524338 = r1524337 * r1524334;
        double r1524339 = exp(r1524338);
        double r1524340 = 1.0;
        double r1524341 = r1524339 - r1524340;
        double r1524342 = r1524334 * r1524341;
        double r1524343 = r1524335 * r1524334;
        double r1524344 = exp(r1524343);
        double r1524345 = r1524344 - r1524340;
        double r1524346 = r1524336 * r1524334;
        double r1524347 = exp(r1524346);
        double r1524348 = r1524347 - r1524340;
        double r1524349 = r1524345 * r1524348;
        double r1524350 = r1524342 / r1524349;
        return r1524350;
}

↓

double f(double a, double b, double eps) {
        double r1524351 = a;
        double r1524352 = b;
        double r1524353 = r1524351 + r1524352;
        double r1524354 = eps;
        double r1524355 = r1524353 * r1524354;
        double r1524356 = exp(r1524355);
        double r1524357 = 1.0;
        double r1524358 = r1524356 - r1524357;
        double r1524359 = r1524358 * r1524354;
        double r1524360 = r1524354 * r1524352;
        double r1524361 = exp(r1524360);
        double r1524362 = r1524361 - r1524357;
        double r1524363 = r1524354 * r1524351;
        double r1524364 = exp(r1524363);
        double r1524365 = r1524364 - r1524357;
        double r1524366 = r1524362 * r1524365;
        double r1524367 = r1524359 / r1524366;
        double r1524368 = -inf.0;
        bool r1524369 = r1524367 <= r1524368;
        double r1524370 = r1524357 / r1524352;
        double r1524371 = r1524357 / r1524351;
        double r1524372 = r1524370 + r1524371;
        double r1524373 = 2.7242283277550334e-62;
        bool r1524374 = r1524367 <= r1524373;
        double r1524375 = r1524374 ? r1524367 : r1524372;
        double r1524376 = r1524369 ? r1524372 : r1524375;
        return r1524376;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	58.8
Target	14.1
Herbie	0.6

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

Derivation

1. Split input into 2 regimes

2. if (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) < -inf.0 or 2.7242283277550334e-62 < (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1)))

   1. Initial program 61.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 56.6

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

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

   4. Taylor expanded around 0 0.4

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

   if -inf.0 < (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) < 2.7242283277550334e-62

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

4. Final simplification 0.6

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right) \cdot \varepsilon}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)} = -\infty:\\ \;\;\;\;\frac{1}{b} + \frac{1}{a}\\ \mathbf{elif}\;\frac{\left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right) \cdot \varepsilon}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)} \le 2.7242283277550334 \cdot 10^{-62}:\\ \;\;\;\;\frac{\left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right) \cdot \varepsilon}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{b} + \frac{1}{a}\\ \end{array}\]

Reproduce

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