2tan (problem 3.3.2)

Average Error: 37.0 → 0.6

Time: 12.4s

Precision: binary64

Math

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

↓

\[\begin{array}{l} t_0 := {\cos \varepsilon}^{2}\\ t_1 := {\cos x}^{2}\\ t_2 := {\sin \varepsilon}^{2}\\ t_3 := {\sin x}^{2}\\ t_4 := 1 - \frac{t_2 \cdot t_3}{t_0 \cdot t_1}\\ t_5 := \frac{\sin \varepsilon}{\cos \varepsilon \cdot t_4}\\ \mathsf{fma}\left(t_5, \frac{\mathsf{expm1}\left(\mathsf{log1p}\left(t_3\right)\right)}{t_1}, t_5\right) + \left(\left(1 + \frac{t_2}{t_0}\right) \cdot \frac{\sin x}{\cos x \cdot t_4} - \frac{\sin x}{\cos x}\right) \end{array} \]

FPCore

(FPCore (x eps) :precision binary64 (- (tan (+ x eps)) (tan x)))

↓

(FPCore (x eps)
 :precision binary64
 (let* ((t_0 (pow (cos eps) 2.0))
        (t_1 (pow (cos x) 2.0))
        (t_2 (pow (sin eps) 2.0))
        (t_3 (pow (sin x) 2.0))
        (t_4 (- 1.0 (/ (* t_2 t_3) (* t_0 t_1))))
        (t_5 (/ (sin eps) (* (cos eps) t_4))))
   (+
    (fma t_5 (/ (expm1 (log1p t_3)) t_1) t_5)
    (-
     (* (+ 1.0 (/ t_2 t_0)) (/ (sin x) (* (cos x) t_4)))
     (/ (sin x) (cos x))))))

C

double code(double x, double eps) {
	return tan(x + eps) - tan(x);
}

↓

double code(double x, double eps) {
	double t_0 = pow(cos(eps), 2.0);
	double t_1 = pow(cos(x), 2.0);
	double t_2 = pow(sin(eps), 2.0);
	double t_3 = pow(sin(x), 2.0);
	double t_4 = 1.0 - ((t_2 * t_3) / (t_0 * t_1));
	double t_5 = sin(eps) / (cos(eps) * t_4);
	return fma(t_5, (expm1(log1p(t_3)) / t_1), t_5) + (((1.0 + (t_2 / t_0)) * (sin(x) / (cos(x) * t_4))) - (sin(x) / cos(x)));
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.0
Target	15.2
Herbie	0.6

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

Derivation

1. Initial program 37.0

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

2. Applied tan-sum_binary64 21.7

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

3. Applied flip--_binary64 21.7

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

4. Applied associate-/r/_binary64 21.7

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

5. Applied fma-neg_binary64 21.7

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

6. Taylor expanded in x around inf 21.9

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

7. Simplified 0.6

   \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{{\sin \varepsilon}^{2} \cdot {\sin x}^{2}}{{\cos \varepsilon}^{2} \cdot {\cos x}^{2}}\right)}, \frac{{\sin x}^{2}}{{\cos x}^{2}}, \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{{\sin \varepsilon}^{2} \cdot {\sin x}^{2}}{{\cos \varepsilon}^{2} \cdot {\cos x}^{2}}\right)}\right) + \left(\left(\frac{{\sin \varepsilon}^{2}}{{\cos \varepsilon}^{2}} + 1\right) \cdot \frac{\sin x}{\cos x \cdot \left(1 - \frac{{\sin \varepsilon}^{2} \cdot {\sin x}^{2}}{{\cos \varepsilon}^{2} \cdot {\cos x}^{2}}\right)} - \frac{\sin x}{\cos x}\right)} \]

8. Applied expm1-log1p-u_binary64 0.6

   \[\leadsto \mathsf{fma}\left(\frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{{\sin \varepsilon}^{2} \cdot {\sin x}^{2}}{{\cos \varepsilon}^{2} \cdot {\cos x}^{2}}\right)}, \frac{\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left({\sin x}^{2}\right)\right)}}{{\cos x}^{2}}, \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{{\sin \varepsilon}^{2} \cdot {\sin x}^{2}}{{\cos \varepsilon}^{2} \cdot {\cos x}^{2}}\right)}\right) + \left(\left(\frac{{\sin \varepsilon}^{2}}{{\cos \varepsilon}^{2}} + 1\right) \cdot \frac{\sin x}{\cos x \cdot \left(1 - \frac{{\sin \varepsilon}^{2} \cdot {\sin x}^{2}}{{\cos \varepsilon}^{2} \cdot {\cos x}^{2}}\right)} - \frac{\sin x}{\cos x}\right) \]

9. Final simplification 0.6

   \[\leadsto \mathsf{fma}\left(\frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{{\sin \varepsilon}^{2} \cdot {\sin x}^{2}}{{\cos \varepsilon}^{2} \cdot {\cos x}^{2}}\right)}, \frac{\mathsf{expm1}\left(\mathsf{log1p}\left({\sin x}^{2}\right)\right)}{{\cos x}^{2}}, \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{{\sin \varepsilon}^{2} \cdot {\sin x}^{2}}{{\cos \varepsilon}^{2} \cdot {\cos x}^{2}}\right)}\right) + \left(\left(1 + \frac{{\sin \varepsilon}^{2}}{{\cos \varepsilon}^{2}}\right) \cdot \frac{\sin x}{\cos x \cdot \left(1 - \frac{{\sin \varepsilon}^{2} \cdot {\sin x}^{2}}{{\cos \varepsilon}^{2} \cdot {\cos x}^{2}}\right)} - \frac{\sin x}{\cos x}\right) \]

Reproduce

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