expq3 (problem 3.4.2)

Average Error: 58.6 → 4.4

Time: 43.3s

Precision: 64

• could not determine a ground truth for program body

  1. a = -5.3203362579500095e-06
  2. b = 8.982188186591226e+192
  3. eps = 7.519418569700105e-169

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

C

double f(double a, double b, double eps) {
        double r4145667 = eps;
        double r4145668 = a;
        double r4145669 = b;
        double r4145670 = r4145668 + r4145669;
        double r4145671 = r4145670 * r4145667;
        double r4145672 = exp(r4145671);
        double r4145673 = 1.0;
        double r4145674 = r4145672 - r4145673;
        double r4145675 = r4145667 * r4145674;
        double r4145676 = r4145668 * r4145667;
        double r4145677 = exp(r4145676);
        double r4145678 = r4145677 - r4145673;
        double r4145679 = r4145669 * r4145667;
        double r4145680 = exp(r4145679);
        double r4145681 = r4145680 - r4145673;
        double r4145682 = r4145678 * r4145681;
        double r4145683 = r4145675 / r4145682;
        return r4145683;
}

↓

double f(double a, double b, double eps) {
        double r4145684 = a;
        double r4145685 = 9.568816560533687e+240;
        bool r4145686 = r4145684 <= r4145685;
        double r4145687 = 1.0;
        double r4145688 = b;
        double r4145689 = r4145687 / r4145688;
        double r4145690 = r4145687 / r4145684;
        double r4145691 = r4145689 + r4145690;
        double r4145692 = 2.5364343459522345e+271;
        bool r4145693 = r4145684 <= r4145692;
        double r4145694 = r4145688 + r4145684;
        double r4145695 = exp(r4145694);
        double r4145696 = eps;
        double r4145697 = pow(r4145695, r4145696);
        double r4145698 = r4145697 - r4145687;
        double r4145699 = r4145698 * r4145696;
        double r4145700 = r4145684 * r4145696;
        double r4145701 = exp(r4145700);
        double r4145702 = r4145701 - r4145687;
        double r4145703 = r4145688 * r4145696;
        double r4145704 = exp(r4145703);
        double r4145705 = r4145704 - r4145687;
        double r4145706 = r4145702 * r4145705;
        double r4145707 = r4145699 / r4145706;
        double r4145708 = r4145696 * r4145694;
        double r4145709 = exp(r4145708);
        double r4145710 = r4145709 - r4145687;
        double r4145711 = r4145696 * r4145710;
        double r4145712 = 0.5;
        double r4145713 = r4145703 * r4145712;
        double r4145714 = r4145703 * r4145713;
        double r4145715 = r4145703 * r4145703;
        double r4145716 = r4145696 * r4145715;
        double r4145717 = 0.16666666666666666;
        double r4145718 = r4145716 * r4145717;
        double r4145719 = r4145718 + r4145696;
        double r4145720 = r4145719 * r4145688;
        double r4145721 = r4145714 + r4145720;
        double r4145722 = r4145721 * r4145702;
        double r4145723 = r4145711 / r4145722;
        double r4145724 = r4145693 ? r4145707 : r4145723;
        double r4145725 = r4145686 ? r4145691 : r4145724;
        return r4145725;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	58.6
Target	14.0
Herbie	4.4

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

Derivation

1. Split input into 3 regimes

2. if a < 9.568816560533687e+240

   1. Initial program 59.0

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

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

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

   4. Taylor expanded around 0 3.0

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

   if 9.568816560533687e+240 < a < 2.5364343459522345e+271

   1. Initial program 48.4

      \[\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. Using strategy rm

   3. Applied exp-prod 48.6

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

   if 2.5364343459522345e+271 < a

   1. Initial program 48.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 37.4

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

   3. Simplified 26.8

      \[\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(\frac{1}{6} \cdot \left(\varepsilon \cdot \left(\left(\varepsilon \cdot b\right) \cdot \left(\varepsilon \cdot b\right)\right)\right) + \varepsilon\right) + \left(\frac{1}{2} \cdot \left(\varepsilon \cdot b\right)\right) \cdot \left(\varepsilon \cdot b\right)\right)}}\]
3. Recombined 3 regimes into one program.

4. Final simplification 4.4

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

Reproduce

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