exp2 (problem 3.3.7)

Average Error: 29.9 → 0.7

Time: 4.0s

Precision: binary64

Math

\[\left(e^{x} - 2\right) + e^{-x}\]

↓

\[\begin{array}{l} \mathbf{if}\;x \leq -0.0005096403824734452:\\ \;\;\;\;\frac{\frac{{2}^{4} - \left(2 + \left(e^{x} + \left({\left(e^{x}\right)}^{3} - {2}^{3}\right)\right)\right) \cdot \left(\left(2 + \left(e^{x} + \left({\left(e^{x}\right)}^{3} - {2}^{3}\right)\right)\right) \cdot {\left(e^{x}\right)}^{2}\right)}{2 \cdot 2 - e^{x} \cdot \left(2 + \left(e^{x} + \left({\left(e^{x}\right)}^{3} - {2}^{3}\right)\right)\right)}}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(2 + e^{x}\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\frac{\left(x \cdot x\right) \cdot \left(7 + x \cdot 11\right) + {x}^{4} \cdot 11.083333333333334}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(2 + e^{x}\right)\right)}} \cdot \sqrt{\frac{\left(x \cdot x\right) \cdot \left(7 + x \cdot 11\right) + {x}^{4} \cdot 11.083333333333334}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(2 + e^{x}\right)\right)}}\\ \end{array}\]

FPCore

(FPCore (x) :precision binary64 (+ (- (exp x) 2.0) (exp (- x))))

↓

(FPCore (x)
 :precision binary64
 (if (<= x -0.0005096403824734452)
   (/
    (/
     (-
      (pow 2.0 4.0)
      (*
       (+ 2.0 (+ (exp x) (- (pow (exp x) 3.0) (pow 2.0 3.0))))
       (*
        (+ 2.0 (+ (exp x) (- (pow (exp x) 3.0) (pow 2.0 3.0))))
        (pow (exp x) 2.0))))
     (-
      (* 2.0 2.0)
      (* (exp x) (+ 2.0 (+ (exp x) (- (pow (exp x) 3.0) (pow 2.0 3.0)))))))
    (+ (pow (exp x) 3.0) (* 2.0 (* (exp x) (+ 2.0 (exp x))))))
   (*
    (sqrt
     (/
      (+ (* (* x x) (+ 7.0 (* x 11.0))) (* (pow x 4.0) 11.083333333333334))
      (+ (pow (exp x) 3.0) (* 2.0 (* (exp x) (+ 2.0 (exp x)))))))
    (sqrt
     (/
      (+ (* (* x x) (+ 7.0 (* x 11.0))) (* (pow x 4.0) 11.083333333333334))
      (+ (pow (exp x) 3.0) (* 2.0 (* (exp x) (+ 2.0 (exp x))))))))))

C

double code(double x) {
	return ((double) (((double) (((double) exp(x)) - 2.0)) + ((double) exp(((double) -(x))))));
}

↓

double code(double x) {
	double tmp;
	if ((x <= -0.0005096403824734452)) {
		tmp = ((((double) (((double) pow(2.0, 4.0)) - ((double) (((double) (2.0 + ((double) (((double) exp(x)) + ((double) (((double) pow(((double) exp(x)), 3.0)) - ((double) pow(2.0, 3.0)))))))) * ((double) (((double) (2.0 + ((double) (((double) exp(x)) + ((double) (((double) pow(((double) exp(x)), 3.0)) - ((double) pow(2.0, 3.0)))))))) * ((double) pow(((double) exp(x)), 2.0)))))))) / ((double) (((double) (2.0 * 2.0)) - ((double) (((double) exp(x)) * ((double) (2.0 + ((double) (((double) exp(x)) + ((double) (((double) pow(((double) exp(x)), 3.0)) - ((double) pow(2.0, 3.0))))))))))))) / ((double) (((double) pow(((double) exp(x)), 3.0)) + ((double) (2.0 * ((double) (((double) exp(x)) * ((double) (2.0 + ((double) exp(x)))))))))));
	} else {
		tmp = ((double) (((double) sqrt((((double) (((double) (((double) (x * x)) * ((double) (7.0 + ((double) (x * 11.0)))))) + ((double) (((double) pow(x, 4.0)) * 11.083333333333334)))) / ((double) (((double) pow(((double) exp(x)), 3.0)) + ((double) (2.0 * ((double) (((double) exp(x)) * ((double) (2.0 + ((double) exp(x))))))))))))) * ((double) sqrt((((double) (((double) (((double) (x * x)) * ((double) (7.0 + ((double) (x * 11.0)))))) + ((double) (((double) pow(x, 4.0)) * 11.083333333333334)))) / ((double) (((double) pow(((double) exp(x)), 3.0)) + ((double) (2.0 * ((double) (((double) exp(x)) * ((double) (2.0 + ((double) exp(x)))))))))))))));
	}
	return tmp;
}

Error

Bits error versus x

Target

Original	29.9
Target	0.0
Herbie	0.7

\[4 \cdot {\left(\sinh \left(\frac{x}{2}\right)\right)}^{2}\]

Derivation

1. Split input into 2 regimes

2. if x < -5.09640382473445174e-4

   1. Initial program 5.5

      \[\left(e^{x} - 2\right) + e^{-x}\]
   2. Using strategy rm

   3. Applied exp-neg_binary64 5.6

      \[\leadsto \left(e^{x} - 2\right) + \color{blue}{\frac{1}{e^{x}}}\]

   4. Applied flip3--_binary64 5.6

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

   5. Applied frac-add_binary64 5.5

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

   6. Simplified 5.3

      \[\leadsto \frac{\color{blue}{2 \cdot 2 + e^{x} \cdot \left(2 + \left(\left({\left(e^{x}\right)}^{3} - {2}^{3}\right) + e^{x}\right)\right)}}{\left(e^{x} \cdot e^{x} + \left(2 \cdot 2 + e^{x} \cdot 2\right)\right) \cdot e^{x}}\]

   7. Simplified 5.3

      \[\leadsto \frac{2 \cdot 2 + e^{x} \cdot \left(2 + \left(\left({\left(e^{x}\right)}^{3} - {2}^{3}\right) + e^{x}\right)\right)}{\color{blue}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}}\]
   8. Using strategy rm

   9. Applied flip-+_binary64 5.3

      \[\leadsto \frac{\color{blue}{\frac{\left(2 \cdot 2\right) \cdot \left(2 \cdot 2\right) - \left(e^{x} \cdot \left(2 + \left(\left({\left(e^{x}\right)}^{3} - {2}^{3}\right) + e^{x}\right)\right)\right) \cdot \left(e^{x} \cdot \left(2 + \left(\left({\left(e^{x}\right)}^{3} - {2}^{3}\right) + e^{x}\right)\right)\right)}{2 \cdot 2 - e^{x} \cdot \left(2 + \left(\left({\left(e^{x}\right)}^{3} - {2}^{3}\right) + e^{x}\right)\right)}}}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}\]

   10. Simplified 5.2

       \[\leadsto \frac{\frac{\color{blue}{{2}^{4} - \left(2 + \left(e^{x} + \left({\left(e^{x}\right)}^{3} - {2}^{3}\right)\right)\right) \cdot \left(\left(2 + \left(e^{x} + \left({\left(e^{x}\right)}^{3} - {2}^{3}\right)\right)\right) \cdot {\left(e^{x}\right)}^{2}\right)}}{2 \cdot 2 - e^{x} \cdot \left(2 + \left(\left({\left(e^{x}\right)}^{3} - {2}^{3}\right) + e^{x}\right)\right)}}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}\]

   11. Simplified 5.2

       \[\leadsto \frac{\frac{{2}^{4} - \left(2 + \left(e^{x} + \left({\left(e^{x}\right)}^{3} - {2}^{3}\right)\right)\right) \cdot \left(\left(2 + \left(e^{x} + \left({\left(e^{x}\right)}^{3} - {2}^{3}\right)\right)\right) \cdot {\left(e^{x}\right)}^{2}\right)}{\color{blue}{2 \cdot 2 - e^{x} \cdot \left(2 + \left(e^{x} + \left({\left(e^{x}\right)}^{3} - {2}^{3}\right)\right)\right)}}}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}\]

   if -5.09640382473445174e-4 < x

   1. Initial program 30.2

      \[\left(e^{x} - 2\right) + e^{-x}\]
   2. Using strategy rm

   3. Applied exp-neg_binary64 30.2

      \[\leadsto \left(e^{x} - 2\right) + \color{blue}{\frac{1}{e^{x}}}\]

   4. Applied flip3--_binary64 30.3

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

   5. Applied frac-add_binary64 30.3

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

   6. Simplified 30.3

      \[\leadsto \frac{\color{blue}{2 \cdot 2 + e^{x} \cdot \left(2 + \left(\left({\left(e^{x}\right)}^{3} - {2}^{3}\right) + e^{x}\right)\right)}}{\left(e^{x} \cdot e^{x} + \left(2 \cdot 2 + e^{x} \cdot 2\right)\right) \cdot e^{x}}\]

   7. Simplified 30.3

      \[\leadsto \frac{2 \cdot 2 + e^{x} \cdot \left(2 + \left(\left({\left(e^{x}\right)}^{3} - {2}^{3}\right) + e^{x}\right)\right)}{\color{blue}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}}\]

   8. Taylor expanded around 0 0.6

      \[\leadsto \frac{\color{blue}{7 \cdot {x}^{2} + \left(11 \cdot {x}^{3} + 11.083333333333334 \cdot {x}^{4}\right)}}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}\]

   9. Simplified 0.6

      \[\leadsto \frac{\color{blue}{11.083333333333334 \cdot {x}^{4} + \left(x \cdot x\right) \cdot \left(7 + x \cdot 11\right)}}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}\]
   10. Using strategy rm

   11. Applied add-sqr-sqrt_binary64 0.6

       \[\leadsto \color{blue}{\sqrt{\frac{11.083333333333334 \cdot {x}^{4} + \left(x \cdot x\right) \cdot \left(7 + x \cdot 11\right)}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}} \cdot \sqrt{\frac{11.083333333333334 \cdot {x}^{4} + \left(x \cdot x\right) \cdot \left(7 + x \cdot 11\right)}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}}}\]

   12. Simplified 0.6

       \[\leadsto \color{blue}{\sqrt{\frac{\left(x \cdot x\right) \cdot \left(7 + x \cdot 11\right) + {x}^{4} \cdot 11.083333333333334}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}}} \cdot \sqrt{\frac{11.083333333333334 \cdot {x}^{4} + \left(x \cdot x\right) \cdot \left(7 + x \cdot 11\right)}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}}\]

   13. Simplified 0.6

       \[\leadsto \sqrt{\frac{\left(x \cdot x\right) \cdot \left(7 + x \cdot 11\right) + {x}^{4} \cdot 11.083333333333334}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}} \cdot \color{blue}{\sqrt{\frac{\left(x \cdot x\right) \cdot \left(7 + x \cdot 11\right) + {x}^{4} \cdot 11.083333333333334}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(e^{x} + 2\right)\right)}}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -0.0005096403824734452:\\ \;\;\;\;\frac{\frac{{2}^{4} - \left(2 + \left(e^{x} + \left({\left(e^{x}\right)}^{3} - {2}^{3}\right)\right)\right) \cdot \left(\left(2 + \left(e^{x} + \left({\left(e^{x}\right)}^{3} - {2}^{3}\right)\right)\right) \cdot {\left(e^{x}\right)}^{2}\right)}{2 \cdot 2 - e^{x} \cdot \left(2 + \left(e^{x} + \left({\left(e^{x}\right)}^{3} - {2}^{3}\right)\right)\right)}}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(2 + e^{x}\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\frac{\left(x \cdot x\right) \cdot \left(7 + x \cdot 11\right) + {x}^{4} \cdot 11.083333333333334}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(2 + e^{x}\right)\right)}} \cdot \sqrt{\frac{\left(x \cdot x\right) \cdot \left(7 + x \cdot 11\right) + {x}^{4} \cdot 11.083333333333334}{{\left(e^{x}\right)}^{3} + 2 \cdot \left(e^{x} \cdot \left(2 + e^{x}\right)\right)}}\\ \end{array}\]

Reproduce

herbie shell --seed 2020204 
(FPCore (x)
  :name "exp2 (problem 3.3.7)"
  :precision binary64
  :herbie-expected 1.5

  :herbie-target
  (* 4.0 (pow (sinh (/ x 2.0)) 2.0))

  (+ (- (exp x) 2.0) (exp (- x))))