2tan (problem 3.3.2)

Average Error: 37.1 → 15.6

Time: 19.2s

Precision: 64

Math

\[\tan \left(x + \varepsilon\right) - \tan x\]

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.029764410213285732202184952592542832375 \cdot 10^{-63}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \sqrt[3]{{\left(\tan x \cdot \tan \varepsilon\right)}^{3}}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 1.132620102760092490884084281497646648791 \cdot 10^{-37}:\\ \;\;\;\;\left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\frac{\tan x + \tan \varepsilon}{\log \left(e^{1 - \tan x \cdot \tan \varepsilon}\right)} \cdot \left(\tan x + \tan \varepsilon\right)}{1 - \tan x \cdot \tan \varepsilon} + \left(-\tan x \cdot \tan x\right)}{\frac{\tan x + \tan \varepsilon}{\log \left(e^{1 - \tan x \cdot \tan \varepsilon}\right)} + \tan x}\\ \end{array}\]

C

double f(double x, double eps) {
        double r73766 = x;
        double r73767 = eps;
        double r73768 = r73766 + r73767;
        double r73769 = tan(r73768);
        double r73770 = tan(r73766);
        double r73771 = r73769 - r73770;
        return r73771;
}

↓

double f(double x, double eps) {
        double r73772 = eps;
        double r73773 = -1.0297644102132857e-63;
        bool r73774 = r73772 <= r73773;
        double r73775 = x;
        double r73776 = tan(r73775);
        double r73777 = tan(r73772);
        double r73778 = r73776 + r73777;
        double r73779 = 1.0;
        double r73780 = r73776 * r73777;
        double r73781 = 3.0;
        double r73782 = pow(r73780, r73781);
        double r73783 = cbrt(r73782);
        double r73784 = r73779 - r73783;
        double r73785 = r73778 / r73784;
        double r73786 = r73785 - r73776;
        double r73787 = 1.1326201027600925e-37;
        bool r73788 = r73772 <= r73787;
        double r73789 = r73775 * r73772;
        double r73790 = r73772 + r73775;
        double r73791 = r73789 * r73790;
        double r73792 = r73791 + r73772;
        double r73793 = r73779 - r73780;
        double r73794 = exp(r73793);
        double r73795 = log(r73794);
        double r73796 = r73778 / r73795;
        double r73797 = r73796 * r73778;
        double r73798 = r73797 / r73793;
        double r73799 = r73776 * r73776;
        double r73800 = -r73799;
        double r73801 = r73798 + r73800;
        double r73802 = r73796 + r73776;
        double r73803 = r73801 / r73802;
        double r73804 = r73788 ? r73792 : r73803;
        double r73805 = r73774 ? r73786 : r73804;
        return r73805;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.1
Target	15.0
Herbie	15.6

\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

1. Split input into 3 regimes

2. if eps < -1.0297644102132857e-63

   1. Initial program 29.7

      \[\tan \left(x + \varepsilon\right) - \tan x\]
   2. Using strategy rm

   3. Applied tan-sum 4.8

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
   4. Using strategy rm

   5. Applied add-cbrt-cube 4.8

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \color{blue}{\sqrt[3]{\left(\tan \varepsilon \cdot \tan \varepsilon\right) \cdot \tan \varepsilon}}} - \tan x\]

   6. Applied add-cbrt-cube 4.9

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\sqrt[3]{\left(\tan x \cdot \tan x\right) \cdot \tan x}} \cdot \sqrt[3]{\left(\tan \varepsilon \cdot \tan \varepsilon\right) \cdot \tan \varepsilon}} - \tan x\]

   7. Applied cbrt-unprod 4.8

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\sqrt[3]{\left(\left(\tan x \cdot \tan x\right) \cdot \tan x\right) \cdot \left(\left(\tan \varepsilon \cdot \tan \varepsilon\right) \cdot \tan \varepsilon\right)}}} - \tan x\]

   8. Simplified 4.8

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

   if -1.0297644102132857e-63 < eps < 1.1326201027600925e-37

   1. Initial program 46.9

      \[\tan \left(x + \varepsilon\right) - \tan x\]
   2. Using strategy rm

   3. Applied tan-sum 46.9

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
   4. Using strategy rm

   5. Applied add-log-exp 46.9

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

   6. Applied add-log-exp 46.9

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

   7. Applied diff-log 46.9

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

   8. Simplified 46.9

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\log \color{blue}{\left(e^{1 - \tan x \cdot \tan \varepsilon}\right)}} - \tan x\]
   9. Using strategy rm

   10. Applied tan-quot 46.9

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

   11. Applied associate-*r/ 46.9

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

   12. Taylor expanded around 0 31.9

       \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]

   13. Simplified 31.7

       \[\leadsto \color{blue}{\left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right) + \varepsilon}\]

   if 1.1326201027600925e-37 < eps

   1. Initial program 30.1

      \[\tan \left(x + \varepsilon\right) - \tan x\]
   2. Using strategy rm

   3. Applied tan-sum 2.5

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
   4. Using strategy rm

   5. Applied add-log-exp 2.6

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

   6. Applied add-log-exp 2.6

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

   7. Applied diff-log 2.6

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

   8. Simplified 2.6

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\log \color{blue}{\left(e^{1 - \tan x \cdot \tan \varepsilon}\right)}} - \tan x\]
   9. Using strategy rm

   10. Applied flip-- 2.7

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

   11. Simplified 2.7

       \[\leadsto \frac{\color{blue}{\frac{\frac{\tan x + \tan \varepsilon}{\log \left(e^{1 - \tan x \cdot \tan \varepsilon}\right)} \cdot \left(\tan x + \tan \varepsilon\right)}{1 - \tan x \cdot \tan \varepsilon} + \left(-\tan x \cdot \tan x\right)}}{\frac{\tan x + \tan \varepsilon}{\log \left(e^{1 - \tan x \cdot \tan \varepsilon}\right)} + \tan x}\]
3. Recombined 3 regimes into one program.

4. Final simplification 15.6

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.029764410213285732202184952592542832375 \cdot 10^{-63}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \sqrt[3]{{\left(\tan x \cdot \tan \varepsilon\right)}^{3}}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 1.132620102760092490884084281497646648791 \cdot 10^{-37}:\\ \;\;\;\;\left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\frac{\tan x + \tan \varepsilon}{\log \left(e^{1 - \tan x \cdot \tan \varepsilon}\right)} \cdot \left(\tan x + \tan \varepsilon\right)}{1 - \tan x \cdot \tan \varepsilon} + \left(-\tan x \cdot \tan x\right)}{\frac{\tan x + \tan \varepsilon}{\log \left(e^{1 - \tan x \cdot \tan \varepsilon}\right)} + \tan x}\\ \end{array}\]

Reproduce

herbie shell --seed 2019308 
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"
  :precision binary64

  :herbie-target
  (/ (sin eps) (* (cos x) (cos (+ x eps))))

  (- (tan (+ x eps)) (tan x)))