Average Error: 36.4 → 14.1
Time: 1.2m
Precision: 64
Internal Precision: 2432
\[\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 -5.014916503528812 \cdot 10^{-14}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \log \left(e^{\tan x \cdot \tan \varepsilon}\right)} - \tan x\\
\mathbf{if}\;\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right) \le 188614067453064.38:\\
\;\;\;\;\varepsilon + \left({\varepsilon}^{3} \cdot {x}^{2} + {\varepsilon}^{2} \cdot x\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \log \left(e^{\tan x \cdot \tan \varepsilon}\right)} - \tan x\\
\end{array}\]
Target
| Original | 36.4 |
|---|
| Target | 14.9 |
|---|
| Herbie | 14.1 |
|---|
\[\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))) < -5.014916503528812e-14 or 188614067453064.38 < (+ eps (+ (* (pow eps 3) (pow x 2)) (* (pow eps 2) x)))
Initial program 36.2
\[\tan \left(x + \varepsilon\right) - \tan x\]
- Using strategy
rm Applied tan-sum12.9
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
- Using strategy
rm Applied add-log-exp13.0
\[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\log \left(e^{\tan x \cdot \tan \varepsilon}\right)}} - \tan x\]
if -5.014916503528812e-14 < (+ eps (+ (* (pow eps 3) (pow x 2)) (* (pow eps 2) x))) < 188614067453064.38
Initial program 36.7
\[\tan \left(x + \varepsilon\right) - \tan x\]
Taylor expanded around 0 16.3
\[\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 '#(1070706311 3771791028 4128836681 4194990999 2341756049 504035650)'
(FPCore (x eps)
:name "2tan (problem 3.3.2)"
:herbie-target
(/ (sin eps) (* (cos x) (cos (+ x eps))))
(- (tan (+ x eps)) (tan x)))