2tan (problem 3.3.2)

Average Error: 37.3 → 15.7

Time: 15.1s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.546126625120823366227573074396806531005 \cdot 10^{-44}:\\ \;\;\;\;\frac{\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon}{\left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)} - \tan x\\ \mathbf{elif}\;\varepsilon \le 3.567141279375676635666856121536066364286 \cdot 10^{-32}:\\ \;\;\;\;\left(\varepsilon \cdot x\right) \cdot \left(x + \varepsilon\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan x \cdot \tan x - \tan \varepsilon \cdot \tan \varepsilon}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x - \tan \varepsilon\right)} - \tan x\\ \end{array}\]

C

double f(double x, double eps) {
        double r237488 = x;
        double r237489 = eps;
        double r237490 = r237488 + r237489;
        double r237491 = tan(r237490);
        double r237492 = tan(r237488);
        double r237493 = r237491 - r237492;
        return r237493;
}

↓

double f(double x, double eps) {
        double r237494 = eps;
        double r237495 = -2.5461266251208234e-44;
        bool r237496 = r237494 <= r237495;
        double r237497 = x;
        double r237498 = sin(r237497);
        double r237499 = cos(r237494);
        double r237500 = r237498 * r237499;
        double r237501 = cos(r237497);
        double r237502 = sin(r237494);
        double r237503 = r237501 * r237502;
        double r237504 = r237500 + r237503;
        double r237505 = 1.0;
        double r237506 = r237498 * r237502;
        double r237507 = r237501 * r237499;
        double r237508 = r237506 / r237507;
        double r237509 = r237505 - r237508;
        double r237510 = r237509 * r237507;
        double r237511 = r237504 / r237510;
        double r237512 = tan(r237497);
        double r237513 = r237511 - r237512;
        double r237514 = 3.5671412793756766e-32;
        bool r237515 = r237494 <= r237514;
        double r237516 = r237494 * r237497;
        double r237517 = r237497 + r237494;
        double r237518 = r237516 * r237517;
        double r237519 = r237518 + r237494;
        double r237520 = r237512 * r237512;
        double r237521 = tan(r237494);
        double r237522 = r237521 * r237521;
        double r237523 = r237520 - r237522;
        double r237524 = r237512 * r237521;
        double r237525 = r237505 - r237524;
        double r237526 = r237512 - r237521;
        double r237527 = r237525 * r237526;
        double r237528 = r237523 / r237527;
        double r237529 = r237528 - r237512;
        double r237530 = r237515 ? r237519 : r237529;
        double r237531 = r237496 ? r237513 : r237530;
        return r237531;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.3
Target	15.5
Herbie	15.7

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

Derivation

1. Split input into 3 regimes

2. if eps < -2.5461266251208234e-44

   1. Initial program 30.1

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

   3. Applied tan-sum 3.5

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

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

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

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

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

   10. Applied tan-quot 3.6

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

   11. Applied tan-quot 3.6

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

   12. Applied frac-times 3.6

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

   13. Applied cube-div 3.6

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

   14. Applied cbrt-div 3.6

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

   15. Simplified 3.6

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

   16. Simplified 3.6

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

   18. Applied tan-quot 3.7

       \[\leadsto \frac{\tan x + \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} - \tan x\]

   19. Applied tan-quot 3.7

       \[\leadsto \frac{\color{blue}{\frac{\sin x}{\cos x}} + \frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} - \tan x\]

   20. Applied frac-add 3.7

       \[\leadsto \frac{\color{blue}{\frac{\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} - \tan x\]

   21. Applied associate-/l/ 3.8

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

   if -2.5461266251208234e-44 < eps < 3.5671412793756766e-32

   1. Initial program 46.5

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

   2. Taylor expanded around 0 32.4

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

   3. Simplified 32.1

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

   if 3.5671412793756766e-32 < eps

   1. Initial program 30.7

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

   3. Applied tan-sum 2.8

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

   5. Applied flip-+ 2.9

      \[\leadsto \frac{\color{blue}{\frac{\tan x \cdot \tan x - \tan \varepsilon \cdot \tan \varepsilon}{\tan x - \tan \varepsilon}}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\]

   6. Applied associate-/l/ 2.9

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

4. Final simplification 15.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -2.546126625120823366227573074396806531005 \cdot 10^{-44}:\\ \;\;\;\;\frac{\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon}{\left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)} - \tan x\\ \mathbf{elif}\;\varepsilon \le 3.567141279375676635666856121536066364286 \cdot 10^{-32}:\\ \;\;\;\;\left(\varepsilon \cdot x\right) \cdot \left(x + \varepsilon\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan x \cdot \tan x - \tan \varepsilon \cdot \tan \varepsilon}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x - \tan \varepsilon\right)} - \tan x\\ \end{array}\]

Reproduce

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