expq3 (problem 3.4.2)

Average Error: 60.5 → 52.3

Time: 31.5s

Precision: 64

• could not determine a ground truth for program body

  1. a = -4.378245219510849e+106
  2. b = -1.404089089984425e+261
  3. eps = -4.518429747333079e-151

\[-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 -2.3529465240552971988881604336729755856 \cdot 10^{80} \lor \neg \left(a \le 8.49205507659549180334390020270641032806 \cdot 10^{150}\right):\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(b \cdot \left(b \cdot \left(\left(\frac{1}{6} \cdot {\varepsilon}^{3}\right) \cdot b + \frac{1}{2} \cdot \left(\varepsilon \cdot \varepsilon\right)\right) + \varepsilon\right)\right) \cdot \left(e^{a \cdot \varepsilon} - 1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(a \cdot \varepsilon + \varepsilon \cdot \left(\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {a}^{3}\right) \cdot \varepsilon + \frac{1}{2} \cdot \left(a \cdot a\right)\right)\right)\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\\ \end{array}\]

C

double f(double a, double b, double eps) {
        double r79717 = eps;
        double r79718 = a;
        double r79719 = b;
        double r79720 = r79718 + r79719;
        double r79721 = r79720 * r79717;
        double r79722 = exp(r79721);
        double r79723 = 1.0;
        double r79724 = r79722 - r79723;
        double r79725 = r79717 * r79724;
        double r79726 = r79718 * r79717;
        double r79727 = exp(r79726);
        double r79728 = r79727 - r79723;
        double r79729 = r79719 * r79717;
        double r79730 = exp(r79729);
        double r79731 = r79730 - r79723;
        double r79732 = r79728 * r79731;
        double r79733 = r79725 / r79732;
        return r79733;
}

↓

double f(double a, double b, double eps) {
        double r79734 = a;
        double r79735 = -2.3529465240552972e+80;
        bool r79736 = r79734 <= r79735;
        double r79737 = 8.492055076595492e+150;
        bool r79738 = r79734 <= r79737;
        double r79739 = !r79738;
        bool r79740 = r79736 || r79739;
        double r79741 = eps;
        double r79742 = b;
        double r79743 = r79734 + r79742;
        double r79744 = r79743 * r79741;
        double r79745 = exp(r79744);
        double r79746 = 1.0;
        double r79747 = r79745 - r79746;
        double r79748 = r79741 * r79747;
        double r79749 = 0.16666666666666666;
        double r79750 = 3.0;
        double r79751 = pow(r79741, r79750);
        double r79752 = r79749 * r79751;
        double r79753 = r79752 * r79742;
        double r79754 = 0.5;
        double r79755 = r79741 * r79741;
        double r79756 = r79754 * r79755;
        double r79757 = r79753 + r79756;
        double r79758 = r79742 * r79757;
        double r79759 = r79758 + r79741;
        double r79760 = r79742 * r79759;
        double r79761 = r79734 * r79741;
        double r79762 = exp(r79761);
        double r79763 = r79762 - r79746;
        double r79764 = r79760 * r79763;
        double r79765 = r79748 / r79764;
        double r79766 = pow(r79734, r79750);
        double r79767 = r79749 * r79766;
        double r79768 = r79767 * r79741;
        double r79769 = r79734 * r79734;
        double r79770 = r79754 * r79769;
        double r79771 = r79768 + r79770;
        double r79772 = r79741 * r79771;
        double r79773 = r79741 * r79772;
        double r79774 = r79761 + r79773;
        double r79775 = r79742 * r79741;
        double r79776 = exp(r79775);
        double r79777 = r79776 - r79746;
        double r79778 = r79774 * r79777;
        double r79779 = r79748 / r79778;
        double r79780 = r79740 ? r79765 : r79779;
        return r79780;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	60.5
Target	14.7
Herbie	52.3

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

Derivation

1. Split input into 2 regimes

2. if a < -2.3529465240552972e+80 or 8.492055076595492e+150 < a

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

   2. Taylor expanded around 0 45.9

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

   5. Applied *-un-lft-identity 42.2

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

   6. Applied associate-*l* 42.2

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

   7. Simplified 40.8

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

   if -2.3529465240552972e+80 < a < 8.492055076595492e+150

   1. Initial program 62.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 56.3

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

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

   5. Applied associate-*l* 56.3

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

4. Final simplification 52.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;a \le -2.3529465240552971988881604336729755856 \cdot 10^{80} \lor \neg \left(a \le 8.49205507659549180334390020270641032806 \cdot 10^{150}\right):\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(b \cdot \left(b \cdot \left(\left(\frac{1}{6} \cdot {\varepsilon}^{3}\right) \cdot b + \frac{1}{2} \cdot \left(\varepsilon \cdot \varepsilon\right)\right) + \varepsilon\right)\right) \cdot \left(e^{a \cdot \varepsilon} - 1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(a \cdot \varepsilon + \varepsilon \cdot \left(\varepsilon \cdot \left(\left(\frac{1}{6} \cdot {a}^{3}\right) \cdot \varepsilon + \frac{1}{2} \cdot \left(a \cdot a\right)\right)\right)\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\\ \end{array}\]

Reproduce

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