2tan (problem 3.3.2)

Average Error: 57.04% → 0.49%

Time: 20.2s

Precision: binary64

Cost: 72000

Math

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

↓

\[\begin{array}{l} t_0 := \tan x \cdot \tan \varepsilon\\ \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \sin x\right)} + \tan x \cdot \frac{t_0}{1 - t_0} \end{array} \]

FPCore

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

↓

(FPCore (x eps)
 :precision binary64
 (let* ((t_0 (* (tan x) (tan eps))))
   (+
    (/
     (sin eps)
     (* (cos eps) (- 1.0 (* (/ (sin eps) (* (cos eps) (cos x))) (sin x)))))
    (* (tan x) (/ t_0 (- 1.0 t_0))))))

C

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

↓

double code(double x, double eps) {
	double t_0 = tan(x) * tan(eps);
	return (sin(eps) / (cos(eps) * (1.0 - ((sin(eps) / (cos(eps) * cos(x))) * sin(x))))) + (tan(x) * (t_0 / (1.0 - t_0)));
}

Fortran

real(8) function code(x, eps)
    real(8), intent (in) :: x
    real(8), intent (in) :: eps
    code = tan((x + eps)) - tan(x)
end function

↓

real(8) function code(x, eps)
    real(8), intent (in) :: x
    real(8), intent (in) :: eps
    real(8) :: t_0
    t_0 = tan(x) * tan(eps)
    code = (sin(eps) / (cos(eps) * (1.0d0 - ((sin(eps) / (cos(eps) * cos(x))) * sin(x))))) + (tan(x) * (t_0 / (1.0d0 - t_0)))
end function

Java

public static double code(double x, double eps) {
	return Math.tan((x + eps)) - Math.tan(x);
}

↓

public static double code(double x, double eps) {
	double t_0 = Math.tan(x) * Math.tan(eps);
	return (Math.sin(eps) / (Math.cos(eps) * (1.0 - ((Math.sin(eps) / (Math.cos(eps) * Math.cos(x))) * Math.sin(x))))) + (Math.tan(x) * (t_0 / (1.0 - t_0)));
}

Python

def code(x, eps):
	return math.tan((x + eps)) - math.tan(x)

↓

def code(x, eps):
	t_0 = math.tan(x) * math.tan(eps)
	return (math.sin(eps) / (math.cos(eps) * (1.0 - ((math.sin(eps) / (math.cos(eps) * math.cos(x))) * math.sin(x))))) + (math.tan(x) * (t_0 / (1.0 - t_0)))

Julia

function code(x, eps)
	return Float64(tan(Float64(x + eps)) - tan(x))
end

↓

function code(x, eps)
	t_0 = Float64(tan(x) * tan(eps))
	return Float64(Float64(sin(eps) / Float64(cos(eps) * Float64(1.0 - Float64(Float64(sin(eps) / Float64(cos(eps) * cos(x))) * sin(x))))) + Float64(tan(x) * Float64(t_0 / Float64(1.0 - t_0))))
end

MATLAB

function tmp = code(x, eps)
	tmp = tan((x + eps)) - tan(x);
end

↓

function tmp = code(x, eps)
	t_0 = tan(x) * tan(eps);
	tmp = (sin(eps) / (cos(eps) * (1.0 - ((sin(eps) / (cos(eps) * cos(x))) * sin(x))))) + (tan(x) * (t_0 / (1.0 - t_0)));
end

Wolfram

code[x_, eps_] := N[(N[Tan[N[(x + eps), $MachinePrecision]], $MachinePrecision] - N[Tan[x], $MachinePrecision]), $MachinePrecision]

↓

code[x_, eps_] := Block[{t$95$0 = N[(N[Tan[x], $MachinePrecision] * N[Tan[eps], $MachinePrecision]), $MachinePrecision]}, N[(N[(N[Sin[eps], $MachinePrecision] / N[(N[Cos[eps], $MachinePrecision] * N[(1.0 - N[(N[(N[Sin[eps], $MachinePrecision] / N[(N[Cos[eps], $MachinePrecision] * N[Cos[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[Sin[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Tan[x], $MachinePrecision] * N[(t$95$0 / N[(1.0 - t$95$0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

Target

Original	57.04%
Target	23.67%
Herbie	0.49%

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

Derivation

1. Initial program 57.04

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

2. Applied egg-rr 33.31

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

3. Simplified 33.28

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

   [Start] 33.31	\[ \left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x \]
   associate-*r/ [=>] 33.28	\[ \color{blue}{\frac{\left(\tan x + \tan \varepsilon\right) \cdot 1}{1 - \tan x \cdot \tan \varepsilon}} - \tan x \]
   *-rgt-identity [=>] 33.28	\[ \frac{\color{blue}{\tan x + \tan \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x \]

4. Taylor expanded in x around inf 33.48

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

5. Simplified 19.81

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

   [Start] 33.48	\[ \left(\frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} + \frac{\sin x}{\cos x \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}\right) - \frac{\sin x}{\cos x} \]
   associate--l+ [=>] 19.83	\[ \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} + \left(\frac{\sin x}{\cos x \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} - \frac{\sin x}{\cos x}\right)} \]
   associate-/r* [=>] 19.83	\[ \color{blue}{\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}}} + \left(\frac{\sin x}{\cos x \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} - \frac{\sin x}{\cos x}\right) \]
   *-commutative [<=] 19.83	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\color{blue}{\cos x \cdot \cos \varepsilon}}} + \left(\frac{\sin x}{\cos x \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} - \frac{\sin x}{\cos x}\right) \]
   associate-/r* [<=] 19.83	\[ \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right)}} + \left(\frac{\sin x}{\cos x \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} - \frac{\sin x}{\cos x}\right) \]

6. Applied egg-rr 21.89

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

7. Simplified 0.49

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

   [Start] 21.89	\[ \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \sin x\right)} + \frac{\tan x \cdot \frac{1}{\tan x} - \left(1 - \tan \varepsilon \cdot \tan x\right)}{\frac{1 - \tan \varepsilon \cdot \tan x}{\tan x}} \]
   associate-/r/ [=>] 21.89	\[ \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \sin x\right)} + \color{blue}{\frac{\tan x \cdot \frac{1}{\tan x} - \left(1 - \tan \varepsilon \cdot \tan x\right)}{1 - \tan \varepsilon \cdot \tan x} \cdot \tan x} \]
   associate--r- [=>] 5.17	\[ \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \sin x\right)} + \frac{\color{blue}{\left(\tan x \cdot \frac{1}{\tan x} - 1\right) + \tan \varepsilon \cdot \tan x}}{1 - \tan \varepsilon \cdot \tan x} \cdot \tan x \]
   rgt-mult-inverse [=>] 0.49	\[ \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \sin x\right)} + \frac{\left(\color{blue}{1} - 1\right) + \tan \varepsilon \cdot \tan x}{1 - \tan \varepsilon \cdot \tan x} \cdot \tan x \]
   metadata-eval [=>] 0.49	\[ \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \sin x\right)} + \frac{\color{blue}{0} + \tan \varepsilon \cdot \tan x}{1 - \tan \varepsilon \cdot \tan x} \cdot \tan x \]
   +-lft-identity [=>] 0.49	\[ \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \sin x\right)} + \frac{\color{blue}{\tan \varepsilon \cdot \tan x}}{1 - \tan \varepsilon \cdot \tan x} \cdot \tan x \]
   *-rgt-identity [<=] 0.49	\[ \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \sin x\right)} + \frac{\tan \varepsilon \cdot \tan x}{\color{blue}{\left(1 - \tan \varepsilon \cdot \tan x\right) \cdot 1}} \cdot \tan x \]
   *-commutative [=>] 0.49	\[ \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \sin x\right)} + \frac{\color{blue}{\tan x \cdot \tan \varepsilon}}{\left(1 - \tan \varepsilon \cdot \tan x\right) \cdot 1} \cdot \tan x \]
   *-rgt-identity [=>] 0.49	\[ \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \sin x\right)} + \frac{\tan x \cdot \tan \varepsilon}{\color{blue}{1 - \tan \varepsilon \cdot \tan x}} \cdot \tan x \]
   *-commutative [=>] 0.49	\[ \frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \sin x\right)} + \frac{\tan x \cdot \tan \varepsilon}{1 - \color{blue}{\tan x \cdot \tan \varepsilon}} \cdot \tan x \]

8. Final simplification 0.49

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

Alternatives

Alternative 1
Error	0.49%
Cost	58944

\[\begin{array}{l} t_0 := \tan x \cdot \tan \varepsilon\\ t_1 := 1 - t_0\\ \tan x \cdot \frac{t_0}{t_1} + \frac{\sin \varepsilon}{\cos \varepsilon \cdot t_1} \end{array} \]

Alternative 2
Error	0.66%
Cost	33097

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -4 \cdot 10^{-9} \lor \neg \left(\varepsilon \leq 4 \cdot 10^{-9}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{\tan \varepsilon}{\frac{1}{\tan x}}} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\varepsilon + \frac{\frac{\varepsilon}{2} \cdot \left(1 - \cos \left(x + x\right)\right)}{{\cos x}^{2}}\\ \end{array} \]

Alternative 3
Error	0.66%
Cost	33096

\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ t_1 := 1 - \tan x \cdot \tan \varepsilon\\ \mathbf{if}\;\varepsilon \leq -3.35 \cdot 10^{-9}:\\ \;\;\;\;\frac{t_0}{t_1} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 5.2 \cdot 10^{-9}:\\ \;\;\;\;\varepsilon + \frac{\frac{\varepsilon}{2} \cdot \left(1 - \cos \left(x + x\right)\right)}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;t_0 \cdot \frac{1}{t_1} - \tan x\\ \end{array} \]

Alternative 4
Error	0.65%
Cost	32969

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -5.3 \cdot 10^{-9} \lor \neg \left(\varepsilon \leq 4.3 \cdot 10^{-9}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\varepsilon + \frac{\frac{\varepsilon}{2} \cdot \left(1 - \cos \left(x + x\right)\right)}{{\cos x}^{2}}\\ \end{array} \]

Alternative 5
Error	22.49%
Cost	26440

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.00025:\\ \;\;\;\;\tan \varepsilon\\ \mathbf{elif}\;\varepsilon \leq 2.45 \cdot 10^{-5}:\\ \;\;\;\;\varepsilon + \frac{\frac{\varepsilon}{2} \cdot \left(1 - \cos \left(x + x\right)\right)}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}\\ \end{array} \]

Alternative 6
Error	22.56%
Cost	20360

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -1.8 \cdot 10^{-5}:\\ \;\;\;\;\tan \varepsilon\\ \mathbf{elif}\;\varepsilon \leq 10^{-5}:\\ \;\;\;\;\varepsilon + \frac{\frac{\varepsilon}{2} \cdot \left(1 - \cos \left(x + x\right)\right)}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\tan \varepsilon\\ \end{array} \]

Alternative 7
Error	41.77%
Cost	6464

\[\tan \varepsilon \]

Alternative 8
Error	95.78%
Cost	64

\[0 \]

Alternative 9
Error	69.17%
Cost	64

\[\varepsilon \]

Reproduce

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