expq3 (problem 3.4.2)

Average Error: 60.4 → 0.4

Time: 29.9s

Precision: 64

• could not determine a ground truth for program body

  1. a = 3.778834344945485e-87
  2. b = -1.1931599701093257e+183
  3. eps = -1.3639945902168682e-56

\[-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 \lor \neg \left(\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 1.899167644810524055568721384107287965304 \cdot 10^{-22}\right):\\ \;\;\;\;\frac{1}{a} + \frac{1}{b}\\ \mathbf{else}:\\ \;\;\;\;\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)}\\ \end{array}\]

C

double f(double a, double b, double eps) {
        double r87939 = eps;
        double r87940 = a;
        double r87941 = b;
        double r87942 = r87940 + r87941;
        double r87943 = r87942 * r87939;
        double r87944 = exp(r87943);
        double r87945 = 1.0;
        double r87946 = r87944 - r87945;
        double r87947 = r87939 * r87946;
        double r87948 = r87940 * r87939;
        double r87949 = exp(r87948);
        double r87950 = r87949 - r87945;
        double r87951 = r87941 * r87939;
        double r87952 = exp(r87951);
        double r87953 = r87952 - r87945;
        double r87954 = r87950 * r87953;
        double r87955 = r87947 / r87954;
        return r87955;
}

↓

double f(double a, double b, double eps) {
        double r87956 = a;
        double r87957 = b;
        double r87958 = r87956 + r87957;
        double r87959 = eps;
        double r87960 = r87958 * r87959;
        double r87961 = exp(r87960);
        double r87962 = 1.0;
        double r87963 = r87961 - r87962;
        double r87964 = r87963 * r87959;
        double r87965 = r87959 * r87957;
        double r87966 = exp(r87965);
        double r87967 = r87966 - r87962;
        double r87968 = r87959 * r87956;
        double r87969 = exp(r87968);
        double r87970 = r87969 - r87962;
        double r87971 = r87967 * r87970;
        double r87972 = r87964 / r87971;
        double r87973 = -inf.0;
        bool r87974 = r87972 <= r87973;
        double r87975 = 1.899167644810524e-22;
        bool r87976 = r87972 <= r87975;
        double r87977 = !r87976;
        bool r87978 = r87974 || r87977;
        double r87979 = 1.0;
        double r87980 = r87979 / r87956;
        double r87981 = r87979 / r87957;
        double r87982 = r87980 + r87981;
        double r87983 = r87978 ? r87982 : r87972;
        return r87983;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	60.4
Target	15.1
Herbie	0.4

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

Derivation

1. Split input into 2 regimes

2. if (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0))) < -inf.0 or 1.899167644810524e-22 < (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0)))

   1. Initial program 63.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 58.4

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

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

   4. Taylor expanded around 0 0.2

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

   if -inf.0 < (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0))) < 1.899167644810524e-22

   1. Initial program 3.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)}\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.4

   \[\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 \lor \neg \left(\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 1.899167644810524055568721384107287965304 \cdot 10^{-22}\right):\\ \;\;\;\;\frac{1}{a} + \frac{1}{b}\\ \mathbf{else}:\\ \;\;\;\;\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)}\\ \end{array}\]

Reproduce

herbie shell --seed 2019194 
(FPCore (a b eps)
  :name "expq3 (problem 3.4.2)"
  :pre (and (< -1.0 eps) (< eps 1.0))

  :herbie-target
  (/ (+ a b) (* a b))

  (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0))))