tanhf (example 3.4)

Average Error: 30.2 → 0.7

Time: 13.8s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

\[\frac{1 - \cos x}{\sin x}\]

↓

\[\begin{array}{l} \mathbf{if}\;\frac{1 - \cos x}{\sin x} \le -0.0097901793206562754:\\ \;\;\;\;\frac{e^{\log \left({1}^{3} - {\left(\cos x\right)}^{3}\right)}}{\left(\cos x \cdot \left(1 + \cos x\right) + 1 \cdot 1\right) \cdot \sin x}\\ \mathbf{elif}\;\frac{1 - \cos x}{\sin x} \le -0.0:\\ \;\;\;\;0.04166666666666663 \cdot {x}^{3} + \left(0.004166666666666624 \cdot {x}^{5} + 0.5 \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos x \cdot \frac{1 \cdot 1 - {\left(\cos x\right)}^{2}}{1 - \cos x} + 1 \cdot 1\right) \cdot \sin x}\\ \end{array}\]

C

double f(double x) {
        double r51630 = 1.0;
        double r51631 = x;
        double r51632 = cos(r51631);
        double r51633 = r51630 - r51632;
        double r51634 = sin(r51631);
        double r51635 = r51633 / r51634;
        return r51635;
}

↓

double f(double x) {
        double r51636 = 1.0;
        double r51637 = x;
        double r51638 = cos(r51637);
        double r51639 = r51636 - r51638;
        double r51640 = sin(r51637);
        double r51641 = r51639 / r51640;
        double r51642 = -0.009790179320656275;
        bool r51643 = r51641 <= r51642;
        double r51644 = 3.0;
        double r51645 = pow(r51636, r51644);
        double r51646 = pow(r51638, r51644);
        double r51647 = r51645 - r51646;
        double r51648 = log(r51647);
        double r51649 = exp(r51648);
        double r51650 = r51636 + r51638;
        double r51651 = r51638 * r51650;
        double r51652 = r51636 * r51636;
        double r51653 = r51651 + r51652;
        double r51654 = r51653 * r51640;
        double r51655 = r51649 / r51654;
        double r51656 = -0.0;
        bool r51657 = r51641 <= r51656;
        double r51658 = 0.04166666666666663;
        double r51659 = pow(r51637, r51644);
        double r51660 = r51658 * r51659;
        double r51661 = 0.004166666666666624;
        double r51662 = 5.0;
        double r51663 = pow(r51637, r51662);
        double r51664 = r51661 * r51663;
        double r51665 = 0.5;
        double r51666 = r51665 * r51637;
        double r51667 = r51664 + r51666;
        double r51668 = r51660 + r51667;
        double r51669 = 2.0;
        double r51670 = pow(r51638, r51669);
        double r51671 = r51652 - r51670;
        double r51672 = r51671 / r51639;
        double r51673 = r51638 * r51672;
        double r51674 = r51673 + r51652;
        double r51675 = r51674 * r51640;
        double r51676 = r51647 / r51675;
        double r51677 = r51657 ? r51668 : r51676;
        double r51678 = r51643 ? r51655 : r51677;
        return r51678;
}

Error

Bits error versus x

Target

Original	30.2
Target	0.0
Herbie	0.7

\[\tan \left(\frac{x}{2}\right)\]

Derivation

1. Split input into 3 regimes

2. if (/ (- 1.0 (cos x)) (sin x)) < -0.009790179320656275

   1. Initial program 0.8

      \[\frac{1 - \cos x}{\sin x}\]
   2. Using strategy rm

   3. Applied add-log-exp 0.9

      \[\leadsto \color{blue}{\log \left(e^{\frac{1 - \cos x}{\sin x}}\right)}\]
   4. Using strategy rm

   5. Applied div-inv 1.0

      \[\leadsto \log \left(e^{\color{blue}{\left(1 - \cos x\right) \cdot \frac{1}{\sin x}}}\right)\]

   6. Applied exp-prod 1.2

      \[\leadsto \log \color{blue}{\left({\left(e^{1 - \cos x}\right)}^{\left(\frac{1}{\sin x}\right)}\right)}\]

   7. Applied log-pow 1.1

      \[\leadsto \color{blue}{\frac{1}{\sin x} \cdot \log \left(e^{1 - \cos x}\right)}\]

   8. Simplified 0.9

      \[\leadsto \frac{1}{\sin x} \cdot \color{blue}{\left(1 - \cos x\right)}\]
   9. Using strategy rm

   10. Applied flip3-- 1.0

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

   11. Applied frac-times 1.0

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

   12. Simplified 1.0

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

   13. Simplified 1.0

       \[\leadsto \frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\left(\cos x \cdot \left(1 + \cos x\right) + 1 \cdot 1\right) \cdot \sin x}}\]
   14. Using strategy rm

   15. Applied add-exp-log 1.0

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

   if -0.009790179320656275 < (/ (- 1.0 (cos x)) (sin x)) < -0.0

   1. Initial program 60.2

      \[\frac{1 - \cos x}{\sin x}\]
   2. Using strategy rm

   3. Applied add-log-exp 60.2

      \[\leadsto \color{blue}{\log \left(e^{\frac{1 - \cos x}{\sin x}}\right)}\]
   4. Using strategy rm

   5. Applied div-inv 60.2

      \[\leadsto \log \left(e^{\color{blue}{\left(1 - \cos x\right) \cdot \frac{1}{\sin x}}}\right)\]

   6. Applied exp-prod 60.2

      \[\leadsto \log \color{blue}{\left({\left(e^{1 - \cos x}\right)}^{\left(\frac{1}{\sin x}\right)}\right)}\]

   7. Applied log-pow 60.2

      \[\leadsto \color{blue}{\frac{1}{\sin x} \cdot \log \left(e^{1 - \cos x}\right)}\]

   8. Simplified 60.2

      \[\leadsto \frac{1}{\sin x} \cdot \color{blue}{\left(1 - \cos x\right)}\]
   9. Using strategy rm

   10. Applied flip3-- 60.2

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

   11. Applied frac-times 60.2

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

   12. Simplified 60.2

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

   13. Simplified 60.2

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

   14. Taylor expanded around 0 0.1

       \[\leadsto \color{blue}{0.04166666666666663 \cdot {x}^{3} + \left(0.004166666666666624 \cdot {x}^{5} + 0.5 \cdot x\right)}\]

   if -0.0 < (/ (- 1.0 (cos x)) (sin x))

   1. Initial program 1.6

      \[\frac{1 - \cos x}{\sin x}\]
   2. Using strategy rm

   3. Applied add-log-exp 1.6

      \[\leadsto \color{blue}{\log \left(e^{\frac{1 - \cos x}{\sin x}}\right)}\]
   4. Using strategy rm

   5. Applied div-inv 1.7

      \[\leadsto \log \left(e^{\color{blue}{\left(1 - \cos x\right) \cdot \frac{1}{\sin x}}}\right)\]

   6. Applied exp-prod 1.9

      \[\leadsto \log \color{blue}{\left({\left(e^{1 - \cos x}\right)}^{\left(\frac{1}{\sin x}\right)}\right)}\]

   7. Applied log-pow 1.9

      \[\leadsto \color{blue}{\frac{1}{\sin x} \cdot \log \left(e^{1 - \cos x}\right)}\]

   8. Simplified 1.6

      \[\leadsto \frac{1}{\sin x} \cdot \color{blue}{\left(1 - \cos x\right)}\]
   9. Using strategy rm

   10. Applied flip3-- 1.7

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

   11. Applied frac-times 1.7

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

   12. Simplified 1.7

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

   13. Simplified 1.7

       \[\leadsto \frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\left(\cos x \cdot \left(1 + \cos x\right) + 1 \cdot 1\right) \cdot \sin x}}\]
   14. Using strategy rm

   15. Applied flip-+ 1.7

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

   16. Simplified 1.7

       \[\leadsto \frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos x \cdot \frac{\color{blue}{1 \cdot 1 - {\left(\cos x\right)}^{2}}}{1 - \cos x} + 1 \cdot 1\right) \cdot \sin x}\]
3. Recombined 3 regimes into one program.

4. Final simplification 0.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{1 - \cos x}{\sin x} \le -0.0097901793206562754:\\ \;\;\;\;\frac{e^{\log \left({1}^{3} - {\left(\cos x\right)}^{3}\right)}}{\left(\cos x \cdot \left(1 + \cos x\right) + 1 \cdot 1\right) \cdot \sin x}\\ \mathbf{elif}\;\frac{1 - \cos x}{\sin x} \le -0.0:\\ \;\;\;\;0.04166666666666663 \cdot {x}^{3} + \left(0.004166666666666624 \cdot {x}^{5} + 0.5 \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos x \cdot \frac{1 \cdot 1 - {\left(\cos x\right)}^{2}}{1 - \cos x} + 1 \cdot 1\right) \cdot \sin x}\\ \end{array}\]

Reproduce

herbie shell --seed 2020042 
(FPCore (x)
  :name "tanhf (example 3.4)"
  :precision binary64
  :herbie-expected 2

  :herbie-target
  (tan (/ x 2))

  (/ (- 1 (cos x)) (sin x)))