expq3 (problem 3.4.2)

Average Error: 60.4 → 0.7

Time: 33.3s

Precision: 64

• could not determine a ground truth for program body

  1. a = 2.8774590365534544e-144
  2. b = 3.0260304830237114e+184
  3. eps = 1.0722929270979165e-66

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

C

double f(double a, double b, double eps) {
        double r65629 = eps;
        double r65630 = a;
        double r65631 = b;
        double r65632 = r65630 + r65631;
        double r65633 = r65632 * r65629;
        double r65634 = exp(r65633);
        double r65635 = 1.0;
        double r65636 = r65634 - r65635;
        double r65637 = r65629 * r65636;
        double r65638 = r65630 * r65629;
        double r65639 = exp(r65638);
        double r65640 = r65639 - r65635;
        double r65641 = r65631 * r65629;
        double r65642 = exp(r65641);
        double r65643 = r65642 - r65635;
        double r65644 = r65640 * r65643;
        double r65645 = r65637 / r65644;
        return r65645;
}

↓

double f(double a, double b, double eps) {
        double r65646 = eps;
        double r65647 = a;
        double r65648 = b;
        double r65649 = r65647 + r65648;
        double r65650 = r65649 * r65646;
        double r65651 = exp(r65650);
        double r65652 = 1.0;
        double r65653 = r65651 - r65652;
        double r65654 = r65646 * r65653;
        double r65655 = r65647 * r65646;
        double r65656 = exp(r65655);
        double r65657 = r65656 - r65652;
        double r65658 = r65648 * r65646;
        double r65659 = exp(r65658);
        double r65660 = r65659 - r65652;
        double r65661 = r65657 * r65660;
        double r65662 = r65654 / r65661;
        double r65663 = -inf.0;
        bool r65664 = r65662 <= r65663;
        double r65665 = 4.2758774830117075e-79;
        bool r65666 = r65662 <= r65665;
        double r65667 = !r65666;
        bool r65668 = r65664 || r65667;
        double r65669 = 1.0;
        double r65670 = r65669 / r65648;
        double r65671 = r65669 / r65647;
        double r65672 = r65670 + r65671;
        double r65673 = r65668 ? r65672 : r65662;
        return r65673;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	60.4
Target	14.8
Herbie	0.7

\[\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 4.2758774830117075e-79 < (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0)))

   1. Initial program 63.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. Taylor expanded around 0 0.6

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

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

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

4. Final simplification 0.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;\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)} = -\infty \lor \neg \left(\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)} \le 4.275877483011707453930622974464582369913 \cdot 10^{-79}\right):\\ \;\;\;\;\frac{1}{b} + \frac{1}{a}\\ \mathbf{else}:\\ \;\;\;\;\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)}\\ \end{array}\]

Reproduce

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