expq3 (problem 3.4.2)

Average Error: 58.7 → 0.2

Time: 2.2m

Precision: 64

• could not determine a ground truth for program body

  1. a = -7.124526950587564e+301
  2. b = -6.9271890162179504e-155
  3. eps = -2.632034696100061e-274

\[-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 0.004832980056266303:\\ \;\;\;\;\frac{\left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right) \cdot \varepsilon}{\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(\left(\sqrt{e^{\varepsilon \cdot b}} + 1\right) \cdot \left(\sqrt[3]{\sqrt{e^{\varepsilon \cdot b}} - 1} \cdot \left(\sqrt[3]{\sqrt{e^{\varepsilon \cdot b}} - 1} \cdot \sqrt[3]{\sqrt{e^{\varepsilon \cdot b}} - 1}\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{b} + \frac{1}{a}\\ \end{array}\]

C

double f(double a, double b, double eps) {
        double r25251018 = eps;
        double r25251019 = a;
        double r25251020 = b;
        double r25251021 = r25251019 + r25251020;
        double r25251022 = r25251021 * r25251018;
        double r25251023 = exp(r25251022);
        double r25251024 = 1.0;
        double r25251025 = r25251023 - r25251024;
        double r25251026 = r25251018 * r25251025;
        double r25251027 = r25251019 * r25251018;
        double r25251028 = exp(r25251027);
        double r25251029 = r25251028 - r25251024;
        double r25251030 = r25251020 * r25251018;
        double r25251031 = exp(r25251030);
        double r25251032 = r25251031 - r25251024;
        double r25251033 = r25251029 * r25251032;
        double r25251034 = r25251026 / r25251033;
        return r25251034;
}

↓

double f(double a, double b, double eps) {
        double r25251035 = a;
        double r25251036 = b;
        double r25251037 = r25251035 + r25251036;
        double r25251038 = eps;
        double r25251039 = r25251037 * r25251038;
        double r25251040 = exp(r25251039);
        double r25251041 = 1.0;
        double r25251042 = r25251040 - r25251041;
        double r25251043 = r25251042 * r25251038;
        double r25251044 = r25251038 * r25251036;
        double r25251045 = exp(r25251044);
        double r25251046 = r25251045 - r25251041;
        double r25251047 = r25251038 * r25251035;
        double r25251048 = exp(r25251047);
        double r25251049 = r25251048 - r25251041;
        double r25251050 = r25251046 * r25251049;
        double r25251051 = r25251043 / r25251050;
        double r25251052 = -inf.0;
        bool r25251053 = r25251051 <= r25251052;
        double r25251054 = r25251041 / r25251036;
        double r25251055 = r25251041 / r25251035;
        double r25251056 = r25251054 + r25251055;
        double r25251057 = 0.004832980056266303;
        bool r25251058 = r25251051 <= r25251057;
        double r25251059 = sqrt(r25251045);
        double r25251060 = r25251059 + r25251041;
        double r25251061 = r25251059 - r25251041;
        double r25251062 = cbrt(r25251061);
        double r25251063 = r25251062 * r25251062;
        double r25251064 = r25251062 * r25251063;
        double r25251065 = r25251060 * r25251064;
        double r25251066 = r25251049 * r25251065;
        double r25251067 = r25251043 / r25251066;
        double r25251068 = r25251058 ? r25251067 : r25251056;
        double r25251069 = r25251053 ? r25251056 : r25251068;
        return r25251069;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	58.7
Target	14.5
Herbie	0.2

\[\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 0.004832980056266303 < (/ (* 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))) < 0.004832980056266303

   1. Initial program 3.2

      \[\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 add-sqr-sqrt 3.3

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

   4. Applied difference-of-sqr-1 3.3

      \[\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(\sqrt{e^{b \cdot \varepsilon}} + 1\right) \cdot \left(\sqrt{e^{b \cdot \varepsilon}} - 1\right)\right)}}\]
   5. Using strategy rm

   6. Applied add-cube-cbrt 3.3

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

4. Final simplification 0.2

   \[\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 0.004832980056266303:\\ \;\;\;\;\frac{\left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right) \cdot \varepsilon}{\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(\left(\sqrt{e^{\varepsilon \cdot b}} + 1\right) \cdot \left(\sqrt[3]{\sqrt{e^{\varepsilon \cdot b}} - 1} \cdot \left(\sqrt[3]{\sqrt{e^{\varepsilon \cdot b}} - 1} \cdot \sqrt[3]{\sqrt{e^{\varepsilon \cdot b}} - 1}\right)\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{b} + \frac{1}{a}\\ \end{array}\]

Reproduce

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