invcot (example 3.9)

Average Error: 59.8 → 59.8

Time: 16.0s

Precision: binary64

Cost: 122816

\[-0.026 < x \land x < 0.026\]

Math

\[\frac{1}{x} - \frac{1}{\tan x} \]

↓

\[\begin{array}{l} t_0 := \frac{\tan x}{x}\\ t_1 := \sqrt[3]{\log \left(-1 + {t_0}^{2}\right)}\\ \frac{\frac{{e}^{\log \left({\left(e^{{t_1}^{2}}\right)}^{t_1}\right)}}{{e}^{\left(\mathsf{log1p}\left(t_0\right)\right)}}}{\tan x} \end{array} \]

FPCore

(FPCore (x) :precision binary64 (- (/ 1.0 x) (/ 1.0 (tan x))))

↓

(FPCore (x)
 :precision binary64
 (let* ((t_0 (/ (tan x) x)) (t_1 (cbrt (log (+ -1.0 (pow t_0 2.0))))))
   (/
    (/ (pow E (log (pow (exp (pow t_1 2.0)) t_1))) (pow E (log1p t_0)))
    (tan x))))

C

double code(double x) {
	return (1.0 / x) - (1.0 / tan(x));
}

↓

double code(double x) {
	double t_0 = tan(x) / x;
	double t_1 = cbrt(log((-1.0 + pow(t_0, 2.0))));
	return (pow(((double) M_E), log(pow(exp(pow(t_1, 2.0)), t_1))) / pow(((double) M_E), log1p(t_0))) / tan(x);
}

Java

public static double code(double x) {
	return (1.0 / x) - (1.0 / Math.tan(x));
}

↓

public static double code(double x) {
	double t_0 = Math.tan(x) / x;
	double t_1 = Math.cbrt(Math.log((-1.0 + Math.pow(t_0, 2.0))));
	return (Math.pow(Math.E, Math.log(Math.pow(Math.exp(Math.pow(t_1, 2.0)), t_1))) / Math.pow(Math.E, Math.log1p(t_0))) / Math.tan(x);
}

Julia

function code(x)
	return Float64(Float64(1.0 / x) - Float64(1.0 / tan(x)))
end

↓

function code(x)
	t_0 = Float64(tan(x) / x)
	t_1 = cbrt(log(Float64(-1.0 + (t_0 ^ 2.0))))
	return Float64(Float64((exp(1) ^ log((exp((t_1 ^ 2.0)) ^ t_1))) / (exp(1) ^ log1p(t_0))) / tan(x))
end

Wolfram

code[x_] := N[(N[(1.0 / x), $MachinePrecision] - N[(1.0 / N[Tan[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

↓

code[x_] := Block[{t$95$0 = N[(N[Tan[x], $MachinePrecision] / x), $MachinePrecision]}, Block[{t$95$1 = N[Power[N[Log[N[(-1.0 + N[Power[t$95$0, 2.0], $MachinePrecision]), $MachinePrecision]], $MachinePrecision], 1/3], $MachinePrecision]}, N[(N[(N[Power[E, N[Log[N[Power[N[Exp[N[Power[t$95$1, 2.0], $MachinePrecision]], $MachinePrecision], t$95$1], $MachinePrecision]], $MachinePrecision]], $MachinePrecision] / N[Power[E, N[Log[1 + t$95$0], $MachinePrecision]], $MachinePrecision]), $MachinePrecision] / N[Tan[x], $MachinePrecision]), $MachinePrecision]]]

Target

Original	59.8
Target	0.1
Herbie	59.8

\[\begin{array}{l} \mathbf{if}\;\left|x\right| < 0.026:\\ \;\;\;\;\frac{x}{3} \cdot \left(1 + \frac{x \cdot x}{15}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{x} - \frac{1}{\tan x}\\ \end{array} \]

Derivation

1. Initial program 59.8

   \[\frac{1}{x} - \frac{1}{\tan x} \]

2. Applied egg-rr 59.8

   \[\leadsto \color{blue}{\frac{\frac{\tan x - x}{x}}{\tan x}} \]

3. Applied egg-rr 59.8

   \[\leadsto \frac{\color{blue}{e^{\log \left(\frac{\tan x}{x} + -1\right)}}}{\tan x} \]

4. Applied egg-rr 59.8

   \[\leadsto \frac{\color{blue}{\frac{{\left(e^{1}\right)}^{\log \left({\left(\frac{\tan x}{x}\right)}^{2} + -1\right)}}{{\left(e^{1}\right)}^{\log \left(\frac{\tan x}{x} + 1\right)}}}}{\tan x} \]

5. Simplified 59.8

   \[\leadsto \frac{\color{blue}{\frac{{e}^{\log \left(-1 + {\left(\frac{\tan x}{x}\right)}^{2}\right)}}{{e}^{\left(\mathsf{log1p}\left(\frac{\tan x}{x}\right)\right)}}}}{\tan x} \]
   Proof
   (/.f64 (pow.f64 (E.f64) (log.f64 (+.f64 -1 (pow.f64 (/.f64 (tan.f64 x) x) 2)))) (pow.f64 (E.f64) (log1p.f64 (/.f64 (tan.f64 x) x)))): 0 points increase in error, 0 points decrease in error
   (/.f64 (pow.f64 (Rewrite<= exp-1-e_binary64 (exp.f64 1)) (log.f64 (+.f64 -1 (pow.f64 (/.f64 (tan.f64 x) x) 2)))) (pow.f64 (E.f64) (log1p.f64 (/.f64 (tan.f64 x) x)))): 0 points increase in error, 0 points decrease in error
   (/.f64 (pow.f64 (exp.f64 1) (log.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (/.f64 (tan.f64 x) x) 2) -1)))) (pow.f64 (E.f64) (log1p.f64 (/.f64 (tan.f64 x) x)))): 0 points increase in error, 0 points decrease in error
   (/.f64 (pow.f64 (exp.f64 1) (log.f64 (+.f64 (pow.f64 (/.f64 (tan.f64 x) x) 2) -1))) (pow.f64 (Rewrite<= exp-1-e_binary64 (exp.f64 1)) (log1p.f64 (/.f64 (tan.f64 x) x)))): 0 points increase in error, 0 points decrease in error
   (/.f64 (pow.f64 (exp.f64 1) (log.f64 (+.f64 (pow.f64 (/.f64 (tan.f64 x) x) 2) -1))) (pow.f64 (exp.f64 1) (Rewrite<= log1p-def_binary64 (log.f64 (+.f64 1 (/.f64 (tan.f64 x) x)))))): 2 points increase in error, 0 points decrease in error
   (/.f64 (pow.f64 (exp.f64 1) (log.f64 (+.f64 (pow.f64 (/.f64 (tan.f64 x) x) 2) -1))) (pow.f64 (exp.f64 1) (log.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (tan.f64 x) x) 1))))): 0 points increase in error, 0 points decrease in error

6. Applied egg-rr 59.8

   \[\leadsto \frac{\frac{{e}^{\log \color{blue}{\left({\left(e^{{\left(\sqrt[3]{\log \left(-1 + {\left(\frac{\tan x}{x}\right)}^{2}\right)}\right)}^{2}}\right)}^{\left(\sqrt[3]{\log \left(-1 + {\left(\frac{\tan x}{x}\right)}^{2}\right)}\right)}\right)}}}{{e}^{\left(\mathsf{log1p}\left(\frac{\tan x}{x}\right)\right)}}}{\tan x} \]

7. Final simplification 59.8

   \[\leadsto \frac{\frac{{e}^{\log \left({\left(e^{{\left(\sqrt[3]{\log \left(-1 + {\left(\frac{\tan x}{x}\right)}^{2}\right)}\right)}^{2}}\right)}^{\left(\sqrt[3]{\log \left(-1 + {\left(\frac{\tan x}{x}\right)}^{2}\right)}\right)}\right)}}{{e}^{\left(\mathsf{log1p}\left(\frac{\tan x}{x}\right)\right)}}}{\tan x} \]

Alternatives

Alternative 1
Error	59.8
Cost	65280

\[\begin{array}{l} t_0 := \frac{\tan x}{x}\\ t_1 := \sqrt{t_0 + 1}\\ \frac{\frac{{e}^{\log \left(-1 + {t_0}^{2}\right)}}{t_1 \cdot t_1}}{\tan x} \end{array} \]

Alternative 2
Error	59.8
Cost	45696

\[\begin{array}{l} t_0 := \frac{\tan x}{x}\\ \frac{\frac{{e}^{\log \left(-1 + {t_0}^{2}\right)}}{t_0 + 1}}{\tan x} \end{array} \]

Alternative 3
Error	59.8
Cost	33024

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

Alternative 4
Error	59.8
Cost	26496

\[\begin{array}{l} t_0 := \frac{\tan x}{x}\\ \frac{\frac{1 - {t_0}^{2}}{-1 - t_0}}{\tan x} \end{array} \]

Alternative 5
Error	59.8
Cost	26048

\[\frac{\log \left(e^{-1 + \frac{\tan x}{x}}\right)}{\tan x} \]

Alternative 6
Error	59.8
Cost	19712

\[\frac{1}{\frac{x}{e^{\mathsf{log1p}\left(\frac{-x}{\tan x}\right)}}} \]

Alternative 7
Error	59.8
Cost	6976

\[\frac{1}{\frac{x}{1 - \frac{x}{\tan x}}} \]

Alternative 8
Error	61.6
Cost	6848

\[\frac{1}{x} + \frac{1}{\tan x} \]

Alternative 9
Error	59.8
Cost	6848

\[\frac{1}{x} + \frac{-1}{\tan x} \]

Reproduce

herbie shell --seed 2022334 
(FPCore (x)
  :name "invcot (example 3.9)"
  :precision binary64
  :pre (and (< -0.026 x) (< x 0.026))

  :herbie-target
  (if (< (fabs x) 0.026) (* (/ x 3.0) (+ 1.0 (/ (* x x) 15.0))) (- (/ 1.0 x) (/ 1.0 (tan x))))

  (- (/ 1.0 x) (/ 1.0 (tan x))))