expq3 (problem 3.4.2)

Average Error: 60.3 → 0.3

Time: 26.2s

Precision: 64

• could not determine a ground truth for program body

  1. a = -1.0312407122753113e+113
  2. b = 1.9702806022714736e+226
  3. eps = 1.5467071799125403e-134

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

C

double f(double a, double b, double eps) {
        double r77989 = eps;
        double r77990 = a;
        double r77991 = b;
        double r77992 = r77990 + r77991;
        double r77993 = r77992 * r77989;
        double r77994 = exp(r77993);
        double r77995 = 1.0;
        double r77996 = r77994 - r77995;
        double r77997 = r77989 * r77996;
        double r77998 = r77990 * r77989;
        double r77999 = exp(r77998);
        double r78000 = r77999 - r77995;
        double r78001 = r77991 * r77989;
        double r78002 = exp(r78001);
        double r78003 = r78002 - r77995;
        double r78004 = r78000 * r78003;
        double r78005 = r77997 / r78004;
        return r78005;
}

↓

double f(double a, double b, double eps) {
        double r78006 = a;
        double r78007 = b;
        double r78008 = r78006 + r78007;
        double r78009 = eps;
        double r78010 = r78008 * r78009;
        double r78011 = exp(r78010);
        double r78012 = 1.0;
        double r78013 = r78011 - r78012;
        double r78014 = r78013 * r78009;
        double r78015 = r78009 * r78007;
        double r78016 = exp(r78015);
        double r78017 = r78016 - r78012;
        double r78018 = r78009 * r78006;
        double r78019 = exp(r78018);
        double r78020 = r78019 - r78012;
        double r78021 = r78017 * r78020;
        double r78022 = r78014 / r78021;
        double r78023 = -inf.0;
        bool r78024 = r78022 <= r78023;
        double r78025 = 7.159658533251718e-09;
        bool r78026 = r78022 <= r78025;
        double r78027 = !r78026;
        bool r78028 = r78024 || r78027;
        double r78029 = 1.0;
        double r78030 = r78029 / r78007;
        double r78031 = r78029 / r78006;
        double r78032 = r78030 + r78031;
        double r78033 = r78028 ? r78032 : r78022;
        return r78033;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	60.3
Target	14.9
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 7.159658533251718e-09 < (/ (* 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}{a} + \frac{1}{b}}\]

   3. Simplified 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))) < 7.159658533251718e-09

   1. Initial program 3.7

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

Reproduce

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

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

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