expq3 (problem 3.4.2)

Average Error: 60.6 → 51.6

Time: 12.8s

Precision: 64

• could not determine a ground truth for program body

  1. a = 9.924781450718653e+287
  2. b = -2.5114980751472456e-157
  3. eps = 8.616451277929908e-154

\[-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}\;a \le -757299.643995453021489083766937255859375:\\ \;\;\;\;\frac{\varepsilon \cdot \frac{\left(-1 \cdot 1\right) + {\left(e^{a + b}\right)}^{\left(2 \cdot \varepsilon\right)}}{e^{\left(a + b\right) \cdot \varepsilon} + 1}}{\frac{\left(-1 \cdot 1\right) + {\left(e^{a}\right)}^{\left(2 \cdot \varepsilon\right)}}{e^{a \cdot \varepsilon} + 1} \cdot \left(b \cdot \left(\left(\left(\frac{1}{2} \cdot {\varepsilon}^{2}\right) \cdot b + \left(\frac{1}{6} \cdot {\varepsilon}^{3}\right) \cdot {b}^{2}\right) + \varepsilon\right)\right)}\\ \mathbf{elif}\;a \le 5.131059667828880019345609589816760230017 \cdot 10^{79}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(\varepsilon \cdot \left(\left(\left(\frac{1}{2} \cdot {a}^{2}\right) \cdot \varepsilon + \left(\frac{1}{6} \cdot {a}^{3}\right) \cdot {\varepsilon}^{2}\right) + a\right)\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(b \cdot \left(\left(\left(\frac{1}{2} \cdot {\varepsilon}^{2}\right) \cdot b + \left(\frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot b\right)\right) \cdot {b}^{\left(\frac{2}{2}\right)}\right) + \varepsilon\right)\right)}\\ \end{array}\]

C

double f(double a, double b, double eps) {
        double r131120 = eps;
        double r131121 = a;
        double r131122 = b;
        double r131123 = r131121 + r131122;
        double r131124 = r131123 * r131120;
        double r131125 = exp(r131124);
        double r131126 = 1.0;
        double r131127 = r131125 - r131126;
        double r131128 = r131120 * r131127;
        double r131129 = r131121 * r131120;
        double r131130 = exp(r131129);
        double r131131 = r131130 - r131126;
        double r131132 = r131122 * r131120;
        double r131133 = exp(r131132);
        double r131134 = r131133 - r131126;
        double r131135 = r131131 * r131134;
        double r131136 = r131128 / r131135;
        return r131136;
}

↓

double f(double a, double b, double eps) {
        double r131137 = a;
        double r131138 = -757299.643995453;
        bool r131139 = r131137 <= r131138;
        double r131140 = eps;
        double r131141 = 1.0;
        double r131142 = r131141 * r131141;
        double r131143 = -r131142;
        double r131144 = b;
        double r131145 = r131137 + r131144;
        double r131146 = exp(r131145);
        double r131147 = 2.0;
        double r131148 = r131147 * r131140;
        double r131149 = pow(r131146, r131148);
        double r131150 = r131143 + r131149;
        double r131151 = r131145 * r131140;
        double r131152 = exp(r131151);
        double r131153 = r131152 + r131141;
        double r131154 = r131150 / r131153;
        double r131155 = r131140 * r131154;
        double r131156 = exp(r131137);
        double r131157 = pow(r131156, r131148);
        double r131158 = r131143 + r131157;
        double r131159 = r131137 * r131140;
        double r131160 = exp(r131159);
        double r131161 = r131160 + r131141;
        double r131162 = r131158 / r131161;
        double r131163 = 0.5;
        double r131164 = pow(r131140, r131147);
        double r131165 = r131163 * r131164;
        double r131166 = r131165 * r131144;
        double r131167 = 0.16666666666666666;
        double r131168 = 3.0;
        double r131169 = pow(r131140, r131168);
        double r131170 = r131167 * r131169;
        double r131171 = pow(r131144, r131147);
        double r131172 = r131170 * r131171;
        double r131173 = r131166 + r131172;
        double r131174 = r131173 + r131140;
        double r131175 = r131144 * r131174;
        double r131176 = r131162 * r131175;
        double r131177 = r131155 / r131176;
        double r131178 = 5.13105966782888e+79;
        bool r131179 = r131137 <= r131178;
        double r131180 = r131152 - r131141;
        double r131181 = r131140 * r131180;
        double r131182 = pow(r131137, r131147);
        double r131183 = r131163 * r131182;
        double r131184 = r131183 * r131140;
        double r131185 = pow(r131137, r131168);
        double r131186 = r131167 * r131185;
        double r131187 = r131186 * r131164;
        double r131188 = r131184 + r131187;
        double r131189 = r131188 + r131137;
        double r131190 = r131140 * r131189;
        double r131191 = r131144 * r131140;
        double r131192 = exp(r131191);
        double r131193 = r131192 - r131141;
        double r131194 = r131190 * r131193;
        double r131195 = r131181 / r131194;
        double r131196 = r131160 - r131141;
        double r131197 = r131169 * r131144;
        double r131198 = r131167 * r131197;
        double r131199 = r131147 / r131147;
        double r131200 = pow(r131144, r131199);
        double r131201 = r131198 * r131200;
        double r131202 = r131166 + r131201;
        double r131203 = r131202 + r131140;
        double r131204 = r131144 * r131203;
        double r131205 = r131196 * r131204;
        double r131206 = r131181 / r131205;
        double r131207 = r131179 ? r131195 : r131206;
        double r131208 = r131139 ? r131177 : r131207;
        return r131208;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	60.6
Target	14.7
Herbie	51.6

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

Derivation

1. Split input into 3 regimes

2. if a < -757299.643995453

   1. Initial program 56.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 50.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(\frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot {b}^{3}\right) + \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot {b}^{2}\right) + \varepsilon \cdot b\right)\right)}}\]

   3. Simplified 48.5

      \[\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(b \cdot \left(\left(\left(\frac{1}{2} \cdot {\varepsilon}^{2}\right) \cdot b + \left(\frac{1}{6} \cdot {\varepsilon}^{3}\right) \cdot {b}^{2}\right) + \varepsilon\right)\right)}}\]
   4. Using strategy rm

   5. Applied flip-- 50.0

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

   6. Simplified 51.0

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

   8. Applied flip-- 51.0

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

   9. Simplified 44.3

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

   if -757299.643995453 < a < 5.13105966782888e+79

   1. Initial program 63.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)}\]

   2. Taylor expanded around 0 56.7

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

   3. Simplified 56.7

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

   if 5.13105966782888e+79 < a

   1. Initial program 54.1

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

      \[\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(\frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot {b}^{3}\right) + \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot {b}^{2}\right) + \varepsilon \cdot b\right)\right)}}\]

   3. Simplified 43.0

      \[\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(b \cdot \left(\left(\left(\frac{1}{2} \cdot {\varepsilon}^{2}\right) \cdot b + \left(\frac{1}{6} \cdot {\varepsilon}^{3}\right) \cdot {b}^{2}\right) + \varepsilon\right)\right)}}\]
   4. Using strategy rm

   5. Applied sqr-pow 43.0

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

   6. Applied associate-*r* 41.2

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

   7. Simplified 41.2

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

4. Final simplification 51.6

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

Reproduce

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