Average Error: 60.0 → 0.2
Time: 13.4s
Precision: binary64
Cost: 33536
\[-0.026 < x \land x < 0.026\]
\[\frac{1}{x} - \frac{1}{\tan x} \]
↓
\[\begin{array}{l} t_0 := \mathsf{fma}\left(x, 0.3333333333333333, {x}^{3} \cdot -0.022222222222222223\right)\\ \frac{x}{\frac{t_0}{x \cdot 0.1111111111111111}} + {x}^{6} \cdot \frac{-0.0004938271604938272}{t_0} \end{array} \]
(FPCore (x) :precision binary64 (- (/ 1.0 x) (/ 1.0 (tan x))))
↓
(FPCore (x)
 :precision binary64
 (let* ((t_0 (fma x 0.3333333333333333 (* (pow x 3.0) -0.022222222222222223))))
   (+
    (/ x (/ t_0 (* x 0.1111111111111111)))
    (* (pow x 6.0) (/ -0.0004938271604938272 t_0)))))
double code(double x) {
	return (1.0 / x) - (1.0 / tan(x));
}
↓
double code(double x) {
	double t_0 = fma(x, 0.3333333333333333, (pow(x, 3.0) * -0.022222222222222223));
	return (x / (t_0 / (x * 0.1111111111111111))) + (pow(x, 6.0) * (-0.0004938271604938272 / t_0));
}

function code(x)
	return Float64(Float64(1.0 / x) - Float64(1.0 / tan(x)))
end
↓
function code(x)
	t_0 = fma(x, 0.3333333333333333, Float64((x ^ 3.0) * -0.022222222222222223))
	return Float64(Float64(x / Float64(t_0 / Float64(x * 0.1111111111111111))) + Float64((x ^ 6.0) * Float64(-0.0004938271604938272 / t_0)))
end

code[x_] := N[(N[(1.0 / x), $MachinePrecision] - N[(1.0 / N[Tan[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
↓
code[x_] := Block[{t$95$0 = N[(x * 0.3333333333333333 + N[(N[Power[x, 3.0], $MachinePrecision] * -0.022222222222222223), $MachinePrecision]), $MachinePrecision]}, N[(N[(x / N[(t$95$0 / N[(x * 0.1111111111111111), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Power[x, 6.0], $MachinePrecision] * N[(-0.0004938271604938272 / t$95$0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

\frac{1}{x} - \frac{1}{\tan x}
↓
\begin{array}{l}
t_0 := \mathsf{fma}\left(x, 0.3333333333333333, {x}^{3} \cdot -0.022222222222222223\right)\\
\frac{x}{\frac{t_0}{x \cdot 0.1111111111111111}} + {x}^{6} \cdot \frac{-0.0004938271604938272}{t_0}
\end{array}

Error

Target

Original60.0
Target0.1
Herbie0.2
\[\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 60.0

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

  2. Taylor expanded in x around 0 0.4

    \[\leadsto \color{blue}{0.3333333333333333 \cdot x + 0.022222222222222223 \cdot {x}^{3}} \]

  3. Applied egg-rr29.0

    \[\leadsto \color{blue}{\frac{1}{\frac{x \cdot 0.3333333333333333 + -0.022222222222222223 \cdot {x}^{3}}{\left(x \cdot x\right) \cdot 0.1111111111111111 - {x}^{6} \cdot 0.0004938271604938272}}} \]

  4. Applied egg-rr29.0

    \[\leadsto \color{blue}{\frac{\left(x \cdot x\right) \cdot 0.1111111111111111}{\mathsf{fma}\left(-0.022222222222222223, {x}^{3}, x \cdot 0.3333333333333333\right)} - \frac{{x}^{6} \cdot 0.0004938271604938272}{\mathsf{fma}\left(-0.022222222222222223, {x}^{3}, x \cdot 0.3333333333333333\right)}} \]

  5. Simplified0.3

    \[\leadsto \color{blue}{x \cdot \frac{x \cdot 0.1111111111111111}{\mathsf{fma}\left(x, 0.3333333333333333, {x}^{3} \cdot -0.022222222222222223\right)} - {x}^{6} \cdot \frac{0.0004938271604938272}{\mathsf{fma}\left(x, 0.3333333333333333, {x}^{3} \cdot -0.022222222222222223\right)}} \]
    Proof
    (-.f64 (*.f64 x (/.f64 (*.f64 x 1/9) (fma.f64 x 1/3 (*.f64 (pow.f64 x 3) -1/45)))) (*.f64 (pow.f64 x 6) (/.f64 1/2025 (fma.f64 x 1/3 (*.f64 (pow.f64 x 3) -1/45))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 x 1)) (/.f64 (*.f64 x 1/9) (fma.f64 x 1/3 (*.f64 (pow.f64 x 3) -1/45)))) (*.f64 (pow.f64 x 6) (/.f64 1/2025 (fma.f64 x 1/3 (*.f64 (pow.f64 x 3) -1/45))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (/.f64 x 1) (/.f64 (*.f64 x 1/9) (fma.f64 x 1/3 (Rewrite<= *-commutative_binary64 (*.f64 -1/45 (pow.f64 x 3)))))) (*.f64 (pow.f64 x 6) (/.f64 1/2025 (fma.f64 x 1/3 (*.f64 (pow.f64 x 3) -1/45))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (/.f64 x 1) (/.f64 (*.f64 x 1/9) (Rewrite=> fma-udef_binary64 (+.f64 (*.f64 x 1/3) (*.f64 -1/45 (pow.f64 x 3)))))) (*.f64 (pow.f64 x 6) (/.f64 1/2025 (fma.f64 x 1/3 (*.f64 (pow.f64 x 3) -1/45))))): 0 points increase in error, 2 points decrease in error
    (-.f64 (*.f64 (/.f64 x 1) (/.f64 (*.f64 x 1/9) (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1/45 (pow.f64 x 3)) (*.f64 x 1/3))))) (*.f64 (pow.f64 x 6) (/.f64 1/2025 (fma.f64 x 1/3 (*.f64 (pow.f64 x 3) -1/45))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 (/.f64 x 1) (/.f64 (*.f64 x 1/9) (Rewrite<= fma-udef_binary64 (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3))))) (*.f64 (pow.f64 x 6) (/.f64 1/2025 (fma.f64 x 1/3 (*.f64 (pow.f64 x 3) -1/45))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 x (*.f64 x 1/9)) (*.f64 1 (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3))))) (*.f64 (pow.f64 x 6) (/.f64 1/2025 (fma.f64 x 1/3 (*.f64 (pow.f64 x 3) -1/45))))): 156 points increase in error, 17 points decrease in error
    (-.f64 (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x x) 1/9)) (*.f64 1 (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3)))) (*.f64 (pow.f64 x 6) (/.f64 1/2025 (fma.f64 x 1/3 (*.f64 (pow.f64 x 3) -1/45))))): 19 points increase in error, 12 points decrease in error
    (-.f64 (/.f64 (*.f64 (*.f64 x x) 1/9) (Rewrite=> *-lft-identity_binary64 (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3)))) (*.f64 (pow.f64 x 6) (/.f64 1/2025 (fma.f64 x 1/3 (*.f64 (pow.f64 x 3) -1/45))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (/.f64 (*.f64 (*.f64 x x) 1/9) (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3))) (*.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (pow.f64 x 6) 1)) (/.f64 1/2025 (fma.f64 x 1/3 (*.f64 (pow.f64 x 3) -1/45))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (/.f64 (*.f64 (*.f64 x x) 1/9) (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3))) (*.f64 (/.f64 (pow.f64 x 6) 1) (/.f64 1/2025 (fma.f64 x 1/3 (Rewrite<= *-commutative_binary64 (*.f64 -1/45 (pow.f64 x 3))))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (/.f64 (*.f64 (*.f64 x x) 1/9) (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3))) (*.f64 (/.f64 (pow.f64 x 6) 1) (/.f64 1/2025 (Rewrite=> fma-udef_binary64 (+.f64 (*.f64 x 1/3) (*.f64 -1/45 (pow.f64 x 3))))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (/.f64 (*.f64 (*.f64 x x) 1/9) (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3))) (*.f64 (/.f64 (pow.f64 x 6) 1) (/.f64 1/2025 (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1/45 (pow.f64 x 3)) (*.f64 x 1/3)))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (/.f64 (*.f64 (*.f64 x x) 1/9) (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3))) (*.f64 (/.f64 (pow.f64 x 6) 1) (/.f64 1/2025 (Rewrite<= fma-udef_binary64 (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3)))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (/.f64 (*.f64 (*.f64 x x) 1/9) (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3))) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (pow.f64 x 6) 1/2025) (*.f64 1 (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3)))))): 0 points increase in error, 0 points decrease in error
    (-.f64 (/.f64 (*.f64 (*.f64 x x) 1/9) (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3))) (/.f64 (*.f64 (pow.f64 x 6) 1/2025) (Rewrite=> *-lft-identity_binary64 (fma.f64 -1/45 (pow.f64 x 3) (*.f64 x 1/3))))): 0 points increase in error, 0 points decrease in error

  6. Applied egg-rr0.2

    \[\leadsto \color{blue}{\frac{x}{\frac{\mathsf{fma}\left(x, 0.3333333333333333, {x}^{3} \cdot -0.022222222222222223\right)}{x \cdot 0.1111111111111111}}} - {x}^{6} \cdot \frac{0.0004938271604938272}{\mathsf{fma}\left(x, 0.3333333333333333, {x}^{3} \cdot -0.022222222222222223\right)} \]

  7. Final simplification0.2

    \[\leadsto \frac{x}{\frac{\mathsf{fma}\left(x, 0.3333333333333333, {x}^{3} \cdot -0.022222222222222223\right)}{x \cdot 0.1111111111111111}} + {x}^{6} \cdot \frac{-0.0004938271604938272}{\mathsf{fma}\left(x, 0.3333333333333333, {x}^{3} \cdot -0.022222222222222223\right)} \]

Alternatives

Alternative 1
Error0.3
Cost20288
\[x \cdot \frac{x \cdot 0.1111111111111111}{\mathsf{fma}\left(x, 0.3333333333333333, {x}^{3} \cdot -0.022222222222222223\right)} + {x}^{5} \cdot -0.0014814814814814814 \]
Alternative 2
Error0.4
Cost19904
\[\mathsf{fma}\left(0.3333333333333333, x, {x}^{3} \cdot 0.022222222222222223 + {x}^{5} \cdot 0.0021164021164021165\right) \]
Alternative 3
Error0.4
Cost13632
\[x \cdot 0.3333333333333333 + \left({x}^{3} \cdot 0.022222222222222223 + {x}^{5} \cdot 0.0021164021164021165\right) \]
Alternative 4
Error0.6
Cost320
\[\frac{1}{\frac{3}{x}} \]
Alternative 5
Error0.7
Cost192
\[x \cdot 0.3333333333333333 \]

Error

Reproduce

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