2tan (problem 3.3.2)

Average Accuracy: 41.8% → 99.4%

Time: 22.6s

Precision: binary64

Cost: 32969

Math

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

↓

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

FPCore

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

↓

(FPCore (x eps)
 :precision binary64
 (if (or (<= eps -2.1e-9) (not (<= eps 2.7e-9)))
   (- (/ (+ (tan x) (tan eps)) (- 1.0 (* (tan x) (tan eps)))) (tan x))
   (+ eps (* eps (pow (tan x) 2.0)))))

C

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

↓

double code(double x, double eps) {
	double tmp;
	if ((eps <= -2.1e-9) || !(eps <= 2.7e-9)) {
		tmp = ((tan(x) + tan(eps)) / (1.0 - (tan(x) * tan(eps)))) - tan(x);
	} else {
		tmp = eps + (eps * pow(tan(x), 2.0));
	}
	return tmp;
}

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) :: tmp
    if ((eps <= (-2.1d-9)) .or. (.not. (eps <= 2.7d-9))) then
        tmp = ((tan(x) + tan(eps)) / (1.0d0 - (tan(x) * tan(eps)))) - tan(x)
    else
        tmp = eps + (eps * (tan(x) ** 2.0d0))
    end if
    code = tmp
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 tmp;
	if ((eps <= -2.1e-9) || !(eps <= 2.7e-9)) {
		tmp = ((Math.tan(x) + Math.tan(eps)) / (1.0 - (Math.tan(x) * Math.tan(eps)))) - Math.tan(x);
	} else {
		tmp = eps + (eps * Math.pow(Math.tan(x), 2.0));
	}
	return tmp;
}

Python

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

↓

def code(x, eps):
	tmp = 0
	if (eps <= -2.1e-9) or not (eps <= 2.7e-9):
		tmp = ((math.tan(x) + math.tan(eps)) / (1.0 - (math.tan(x) * math.tan(eps)))) - math.tan(x)
	else:
		tmp = eps + (eps * math.pow(math.tan(x), 2.0))
	return tmp

Julia

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

↓

function code(x, eps)
	tmp = 0.0
	if ((eps <= -2.1e-9) || !(eps <= 2.7e-9))
		tmp = Float64(Float64(Float64(tan(x) + tan(eps)) / Float64(1.0 - Float64(tan(x) * tan(eps)))) - tan(x));
	else
		tmp = Float64(eps + Float64(eps * (tan(x) ^ 2.0)));
	end
	return tmp
end

MATLAB

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

↓

function tmp_2 = code(x, eps)
	tmp = 0.0;
	if ((eps <= -2.1e-9) || ~((eps <= 2.7e-9)))
		tmp = ((tan(x) + tan(eps)) / (1.0 - (tan(x) * tan(eps)))) - tan(x);
	else
		tmp = eps + (eps * (tan(x) ^ 2.0));
	end
	tmp_2 = tmp;
end

Wolfram

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

↓

code[x_, eps_] := If[Or[LessEqual[eps, -2.1e-9], N[Not[LessEqual[eps, 2.7e-9]], $MachinePrecision]], N[(N[(N[(N[Tan[x], $MachinePrecision] + N[Tan[eps], $MachinePrecision]), $MachinePrecision] / N[(1.0 - N[(N[Tan[x], $MachinePrecision] * N[Tan[eps], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Tan[x], $MachinePrecision]), $MachinePrecision], N[(eps + N[(eps * N[Power[N[Tan[x], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

Target

Original	41.8%
Target	76.4%
Herbie	99.4%

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

Derivation

1. Split input into 2 regimes

2. if eps < -2.10000000000000019e-9 or 2.7000000000000002e-9 < eps

   1. Initial program 53.5%

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

   2. Applied egg-rr 99.2%

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

      [Start] 53.5	\[ \tan \left(x + \varepsilon\right) - \tan x \]
      tan-sum [=>] 99.2	\[ \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x \]
      div-inv [=>] 99.2	\[ \color{blue}{\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon}} - \tan x \]

   3. Simplified 99.2%

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

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

   if -2.10000000000000019e-9 < eps < 2.7000000000000002e-9

   1. Initial program 29.4%

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

   2. Applied egg-rr 30.0%

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

      [Start] 29.4	\[ \tan \left(x + \varepsilon\right) - \tan x \]
      tan-sum [=>] 30.0	\[ \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x \]
      flip3-- [=>] 29.9	\[ \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}{1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)}}} - \tan x \]
      associate-/r/ [=>] 30.0	\[ \color{blue}{\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right)} - \tan x \]
      metadata-eval [=>] 30.0	\[ \frac{\tan x + \tan \varepsilon}{\color{blue}{1} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) - \tan x \]
      metadata-eval [=>] 30.0	\[ \frac{\tan x + \tan \varepsilon}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(\color{blue}{1} + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) - \tan x \]
      *-un-lft-identity [<=] 30.0	\[ \frac{\tan x + \tan \varepsilon}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + \color{blue}{\tan x \cdot \tan \varepsilon}\right)\right) - \tan x \]
      +-commutative [=>] 30.0	\[ \frac{\tan x + \tan \varepsilon}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 + \color{blue}{\left(\tan x \cdot \tan \varepsilon + \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)}\right) - \tan x \]

   3. Simplified 30.0%

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

      [Start] 30.0	\[ \frac{\tan x + \tan \varepsilon}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 + \left(\tan x \cdot \tan \varepsilon + \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) - \tan x \]
      distribute-rgt1-in [=>] 30.0	\[ \frac{\tan x + \tan \varepsilon}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 + \color{blue}{\left(\tan x \cdot \tan \varepsilon + 1\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) - \tan x \]
      +-commutative [<=] 30.0	\[ \frac{\tan x + \tan \varepsilon}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 + \color{blue}{\left(1 + \tan x \cdot \tan \varepsilon\right)} \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) - \tan x \]

   4. Taylor expanded in eps around 0 99.3%

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

   5. Applied egg-rr 99.3%

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

      [Start] 99.3	\[ \varepsilon \cdot \left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right) \]
      expm1-log1p-u [=>] 99.3	\[ \varepsilon \cdot \left(1 + \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\right)}\right) \]
      log1p-def [<=] 99.3	\[ \varepsilon \cdot \left(1 + \mathsf{expm1}\left(\color{blue}{\log \left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)}\right)\right) \]
      expm1-udef [=>] 99.3	\[ \varepsilon \cdot \left(1 + \color{blue}{\left(e^{\log \left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)} - 1\right)}\right) \]
      add-exp-log [<=] 99.3	\[ \varepsilon \cdot \left(1 + \left(\color{blue}{\left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)} - 1\right)\right) \]
      +-commutative [=>] 99.3	\[ \varepsilon \cdot \left(1 + \left(\color{blue}{\left(\frac{{\sin x}^{2}}{{\cos x}^{2}} + 1\right)} - 1\right)\right) \]
      associate--l+ [=>] 99.3	\[ \varepsilon \cdot \left(1 + \color{blue}{\left(\frac{{\sin x}^{2}}{{\cos x}^{2}} + \left(1 - 1\right)\right)}\right) \]
      add-sqr-sqrt [=>] 99.3	\[ \varepsilon \cdot \left(1 + \left(\color{blue}{\sqrt{\frac{{\sin x}^{2}}{{\cos x}^{2}}} \cdot \sqrt{\frac{{\sin x}^{2}}{{\cos x}^{2}}}} + \left(1 - 1\right)\right)\right) \]
      pow2 [=>] 99.3	\[ \varepsilon \cdot \left(1 + \left(\color{blue}{{\left(\sqrt{\frac{{\sin x}^{2}}{{\cos x}^{2}}}\right)}^{2}} + \left(1 - 1\right)\right)\right) \]
      sqrt-div [=>] 99.3	\[ \varepsilon \cdot \left(1 + \left({\color{blue}{\left(\frac{\sqrt{{\sin x}^{2}}}{\sqrt{{\cos x}^{2}}}\right)}}^{2} + \left(1 - 1\right)\right)\right) \]
      sqrt-pow1 [=>] 99.3	\[ \varepsilon \cdot \left(1 + \left({\left(\frac{\color{blue}{{\sin x}^{\left(\frac{2}{2}\right)}}}{\sqrt{{\cos x}^{2}}}\right)}^{2} + \left(1 - 1\right)\right)\right) \]
      metadata-eval [=>] 99.3	\[ \varepsilon \cdot \left(1 + \left({\left(\frac{{\sin x}^{\color{blue}{1}}}{\sqrt{{\cos x}^{2}}}\right)}^{2} + \left(1 - 1\right)\right)\right) \]
      pow1 [<=] 99.3	\[ \varepsilon \cdot \left(1 + \left({\left(\frac{\color{blue}{\sin x}}{\sqrt{{\cos x}^{2}}}\right)}^{2} + \left(1 - 1\right)\right)\right) \]
      sqrt-pow1 [=>] 99.3	\[ \varepsilon \cdot \left(1 + \left({\left(\frac{\sin x}{\color{blue}{{\cos x}^{\left(\frac{2}{2}\right)}}}\right)}^{2} + \left(1 - 1\right)\right)\right) \]
      metadata-eval [=>] 99.3	\[ \varepsilon \cdot \left(1 + \left({\left(\frac{\sin x}{{\cos x}^{\color{blue}{1}}}\right)}^{2} + \left(1 - 1\right)\right)\right) \]
      pow1 [<=] 99.3	\[ \varepsilon \cdot \left(1 + \left({\left(\frac{\sin x}{\color{blue}{\cos x}}\right)}^{2} + \left(1 - 1\right)\right)\right) \]
      metadata-eval [=>] 99.3	\[ \varepsilon \cdot \left(1 + \left({\left(\frac{\sin x}{\cos x}\right)}^{2} + \color{blue}{0}\right)\right) \]

   6. Simplified 99.3%

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

      [Start] 99.3	\[ \varepsilon \cdot \left(1 + \left({\left(\frac{\sin x}{\cos x}\right)}^{2} + 0\right)\right) \]
      +-rgt-identity [=>] 99.3	\[ \varepsilon \cdot \left(1 + \color{blue}{{\left(\frac{\sin x}{\cos x}\right)}^{2}}\right) \]

   7. Applied egg-rr 99.5%

      \[\leadsto \color{blue}{{\tan x}^{2} \cdot \varepsilon + \varepsilon} \]
      Proof

      [Start] 99.3	\[ \varepsilon \cdot \left(1 + {\left(\frac{\sin x}{\cos x}\right)}^{2}\right) \]
      distribute-rgt-in [=>] 99.4	\[ \color{blue}{1 \cdot \varepsilon + {\left(\frac{\sin x}{\cos x}\right)}^{2} \cdot \varepsilon} \]
      *-un-lft-identity [<=] 99.4	\[ \color{blue}{\varepsilon} + {\left(\frac{\sin x}{\cos x}\right)}^{2} \cdot \varepsilon \]
      +-commutative [=>] 99.4	\[ \color{blue}{{\left(\frac{\sin x}{\cos x}\right)}^{2} \cdot \varepsilon + \varepsilon} \]
      quot-tan [=>] 99.5	\[ {\color{blue}{\tan x}}^{2} \cdot \varepsilon + \varepsilon \]

3. Recombined 2 regimes into one program.

4. Final simplification 99.4%

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

Alternatives

Alternative 1
Accuracy	99.5%
Cost	59072

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

Alternative 2
Accuracy	99.5%
Cost	52416

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

Alternative 3
Accuracy	77.5%
Cost	13448

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

Alternative 4
Accuracy	77.5%
Cost	13448

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -5.4 \cdot 10^{-6}:\\ \;\;\;\;\tan \varepsilon\\ \mathbf{elif}\;\varepsilon \leq 0.00021:\\ \;\;\;\;\varepsilon + \varepsilon \cdot {\tan x}^{2}\\ \mathbf{else}:\\ \;\;\;\;\tan \varepsilon\\ \end{array} \]

Alternative 5
Accuracy	57.6%
Cost	6464

\[\tan \varepsilon \]

Alternative 6
Accuracy	30.8%
Cost	64

\[\varepsilon \]

Reproduce

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