Average Error: 37.4 → 14.2
Time: 1.4m
Precision: 64
Internal Precision: 2368
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l}
\mathbf{if}\;\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right) \le -1.1847356120651231 \cdot 10^{-20}:\\
\;\;\;\;\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x\\
\mathbf{if}\;\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right) \le 1.0087955470724782 \cdot 10^{-19}:\\
\;\;\;\;\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x\\
\end{array}\]
Target
| Original | 37.4 |
|---|
| Target | 15.3 |
|---|
| Herbie | 14.2 |
|---|
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]
Derivation
- Split input into 2 regimes
if (+ eps (+ (* (pow eps 3) (pow x 2)) (* (pow eps 2) x))) < -1.1847356120651231e-20 or 1.0087955470724782e-19 < (+ eps (+ (* (pow eps 3) (pow x 2)) (* (pow eps 2) x)))
Initial program 36.3
\[\tan \left(x + \varepsilon\right) - \tan x\]
- Using strategy
rm Applied tan-sum13.1
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
- Using strategy
rm Applied clear-num13.2
\[\leadsto \color{blue}{\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}}} - \tan x\]
if -1.1847356120651231e-20 < (+ eps (+ (* (pow eps 3) (pow x 2)) (* (pow eps 2) x))) < 1.0087955470724782e-19
Initial program 39.5
\[\tan \left(x + \varepsilon\right) - \tan x\]
Taylor expanded around 0 16.4
\[\leadsto \color{blue}{\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right)}\]
- Recombined 2 regimes into one program.
Runtime
herbie shell --seed '#(1071852389 864846987 1238109217 3425890003 4124793586 650694553)'
(FPCore (x eps)
:name "2tan (problem 3.3.2)"
:herbie-target
(/ (sin eps) (* (cos x) (cos (+ x eps))))
(- (tan (+ x eps)) (tan x)))