expq3 (problem 3.4.2)

Average Error: 58.9 → 0.3

Time: 36.9s

Precision: 64

• could not determine a ground truth for program body

  1. a = -1.1000495125221241e+294
  2. b = -2.8192679536690592e-123
  3. eps = -3.1746452403495127e-34

\[-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 9.94144611454887 \cdot 10^{-08}:\\ \;\;\;\;\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 r3616712 = eps;
        double r3616713 = a;
        double r3616714 = b;
        double r3616715 = r3616713 + r3616714;
        double r3616716 = r3616715 * r3616712;
        double r3616717 = exp(r3616716);
        double r3616718 = 1.0;
        double r3616719 = r3616717 - r3616718;
        double r3616720 = r3616712 * r3616719;
        double r3616721 = r3616713 * r3616712;
        double r3616722 = exp(r3616721);
        double r3616723 = r3616722 - r3616718;
        double r3616724 = r3616714 * r3616712;
        double r3616725 = exp(r3616724);
        double r3616726 = r3616725 - r3616718;
        double r3616727 = r3616723 * r3616726;
        double r3616728 = r3616720 / r3616727;
        return r3616728;
}

↓

double f(double a, double b, double eps) {
        double r3616729 = a;
        double r3616730 = b;
        double r3616731 = r3616729 + r3616730;
        double r3616732 = eps;
        double r3616733 = r3616731 * r3616732;
        double r3616734 = exp(r3616733);
        double r3616735 = 1.0;
        double r3616736 = r3616734 - r3616735;
        double r3616737 = r3616736 * r3616732;
        double r3616738 = r3616732 * r3616730;
        double r3616739 = exp(r3616738);
        double r3616740 = r3616739 - r3616735;
        double r3616741 = r3616732 * r3616729;
        double r3616742 = exp(r3616741);
        double r3616743 = r3616742 - r3616735;
        double r3616744 = r3616740 * r3616743;
        double r3616745 = r3616737 / r3616744;
        double r3616746 = -inf.0;
        bool r3616747 = r3616745 <= r3616746;
        double r3616748 = r3616735 / r3616730;
        double r3616749 = r3616735 / r3616729;
        double r3616750 = r3616748 + r3616749;
        double r3616751 = 9.94144611454887e-08;
        bool r3616752 = r3616745 <= r3616751;
        double r3616753 = r3616752 ? r3616745 : r3616750;
        double r3616754 = r3616747 ? r3616750 : r3616753;
        return r3616754;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	58.9
Target	14.3
Herbie	0.3

\[\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 9.94144611454887e-08 < (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1)))

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

      \[\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))) < 9.94144611454887e-08

   1. Initial program 4.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 -inf 4.0

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\color{blue}{\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:\\ \;\;\;\;\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 9.94144611454887 \cdot 10^{-08}:\\ \;\;\;\;\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 2019135 
(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))))