Falkner and Boettcher, Appendix B, 1

Average Accuracy: 99.1% → 98.9%

Time: 16.2s

Precision: binary64

Cost: 26560

Math

\[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right) \]

↓

\[\left(\cos^{-1} \left(-1 + 4 \cdot \left(\mathsf{fma}\left(v, v, {v}^{4}\right) + {v}^{6}\right)\right) + 2\right) + -2 \]

FPCore

(FPCore (v)
 :precision binary64
 (acos (/ (- 1.0 (* 5.0 (* v v))) (- (* v v) 1.0))))

↓

(FPCore (v)
 :precision binary64
 (+
  (+ (acos (+ -1.0 (* 4.0 (+ (fma v v (pow v 4.0)) (pow v 6.0))))) 2.0)
  -2.0))

C

double code(double v) {
	return acos(((1.0 - (5.0 * (v * v))) / ((v * v) - 1.0)));
}

↓

double code(double v) {
	return (acos((-1.0 + (4.0 * (fma(v, v, pow(v, 4.0)) + pow(v, 6.0))))) + 2.0) + -2.0;
}

Julia

function code(v)
	return acos(Float64(Float64(1.0 - Float64(5.0 * Float64(v * v))) / Float64(Float64(v * v) - 1.0)))
end

↓

function code(v)
	return Float64(Float64(acos(Float64(-1.0 + Float64(4.0 * Float64(fma(v, v, (v ^ 4.0)) + (v ^ 6.0))))) + 2.0) + -2.0)
end

Wolfram

code[v_] := N[ArcCos[N[(N[(1.0 - N[(5.0 * N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[(v * v), $MachinePrecision] - 1.0), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]

↓

code[v_] := N[(N[(N[ArcCos[N[(-1.0 + N[(4.0 * N[(N[(v * v + N[Power[v, 4.0], $MachinePrecision]), $MachinePrecision] + N[Power[v, 6.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] + 2.0), $MachinePrecision] + -2.0), $MachinePrecision]

Derivation

1. Initial program 99.1%

   \[\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right) \]

2. Applied egg-rr 99.1%

   \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{1 + \left(v \cdot v\right) \cdot -5}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)\right)} \]
   Proof

   [Start] 99.1	\[ \cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right) \]
   expm1-log1p-u [=>] 99.1	\[ \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{1 - 5 \cdot \left(v \cdot v\right)}{v \cdot v - 1}\right)\right)\right)} \]
   cancel-sign-sub-inv [=>] 99.1	\[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\color{blue}{1 + \left(-5\right) \cdot \left(v \cdot v\right)}}{v \cdot v - 1}\right)\right)\right) \]
   *-commutative [=>] 99.1	\[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{1 + \color{blue}{\left(v \cdot v\right) \cdot \left(-5\right)}}{v \cdot v - 1}\right)\right)\right) \]
   metadata-eval [=>] 99.1	\[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{1 + \left(v \cdot v\right) \cdot \color{blue}{-5}}{v \cdot v - 1}\right)\right)\right) \]
   fma-neg [=>] 99.1	\[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{1 + \left(v \cdot v\right) \cdot -5}{\color{blue}{\mathsf{fma}\left(v, v, -1\right)}}\right)\right)\right) \]
   metadata-eval [=>] 99.1	\[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{1 + \left(v \cdot v\right) \cdot -5}{\mathsf{fma}\left(v, v, \color{blue}{-1}\right)}\right)\right)\right) \]

3. Applied egg-rr 94.9%

   \[\leadsto \mathsf{expm1}\left(\color{blue}{{\left(\sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}\right)}^{3}}\right) \]
   Proof

   [Start] 99.1	\[ \mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{1 + \left(v \cdot v\right) \cdot -5}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)\right) \]
   add-cube-cbrt [=>] 94.9	\[ \mathsf{expm1}\left(\color{blue}{\left(\sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{1 + \left(v \cdot v\right) \cdot -5}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)} \cdot \sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{1 + \left(v \cdot v\right) \cdot -5}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}\right) \cdot \sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{1 + \left(v \cdot v\right) \cdot -5}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}}\right) \]
   pow3 [=>] 94.9	\[ \mathsf{expm1}\left(\color{blue}{{\left(\sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{1 + \left(v \cdot v\right) \cdot -5}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}\right)}^{3}}\right) \]
   +-commutative [=>] 94.9	\[ \mathsf{expm1}\left({\left(\sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\color{blue}{\left(v \cdot v\right) \cdot -5 + 1}}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}\right)}^{3}\right) \]
   associate-*l* [=>] 94.9	\[ \mathsf{expm1}\left({\left(\sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\color{blue}{v \cdot \left(v \cdot -5\right)} + 1}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}\right)}^{3}\right) \]
   fma-def [=>] 94.9	\[ \mathsf{expm1}\left({\left(\sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\color{blue}{\mathsf{fma}\left(v, v \cdot -5, 1\right)}}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}\right)}^{3}\right) \]

4. Applied egg-rr 99.1%

   \[\leadsto \color{blue}{\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right) + 2\right) - 2} \]
   Proof

   [Start] 94.9	\[ \mathsf{expm1}\left({\left(\sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}\right)}^{3}\right) \]
   expm1-udef [=>] 94.9	\[ \color{blue}{e^{{\left(\sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}\right)}^{3}} - 1} \]
   rem-cube-cbrt [=>] 99.1	\[ e^{\color{blue}{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}} - 1 \]
   log1p-udef [=>] 99.1	\[ e^{\color{blue}{\log \left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}} - 1 \]
   add-exp-log [<=] 99.1	\[ \color{blue}{\left(1 + \cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)} - 1 \]
   expm1-log1p-u [=>] 99.1	\[ \left(1 + \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)\right)}\right) - 1 \]
   rem-cube-cbrt [<=] 94.9	\[ \left(1 + \mathsf{expm1}\left(\color{blue}{{\left(\sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}\right)}^{3}}\right)\right) - 1 \]
   expm1-udef [=>] 94.9	\[ \left(1 + \color{blue}{\left(e^{{\left(\sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}\right)}^{3}} - 1\right)}\right) - 1 \]
   associate-+r- [=>] 94.9	\[ \color{blue}{\left(\left(1 + e^{{\left(\sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}\right)}^{3}}\right) - 1\right)} - 1 \]
   associate--l- [=>] 94.9	\[ \color{blue}{\left(1 + e^{{\left(\sqrt[3]{\mathsf{log1p}\left(\cos^{-1} \left(\frac{\mathsf{fma}\left(v, v \cdot -5, 1\right)}{\mathsf{fma}\left(v, v, -1\right)}\right)\right)}\right)}^{3}}\right) - \left(1 + 1\right)} \]

5. Taylor expanded in v around 0 98.9%

   \[\leadsto \left(\cos^{-1} \color{blue}{\left(\left(4 \cdot {v}^{2} + \left(4 \cdot {v}^{4} + 4 \cdot {v}^{6}\right)\right) - 1\right)} + 2\right) - 2 \]

6. Simplified 98.9%

   \[\leadsto \left(\cos^{-1} \color{blue}{\left(-1 + 4 \cdot \left(\mathsf{fma}\left(v, v, {v}^{4}\right) + {v}^{6}\right)\right)} + 2\right) - 2 \]
   Proof

   [Start] 98.9	\[ \left(\cos^{-1} \left(\left(4 \cdot {v}^{2} + \left(4 \cdot {v}^{4} + 4 \cdot {v}^{6}\right)\right) - 1\right) + 2\right) - 2 \]
   sub-neg [=>] 98.9	\[ \left(\cos^{-1} \color{blue}{\left(\left(4 \cdot {v}^{2} + \left(4 \cdot {v}^{4} + 4 \cdot {v}^{6}\right)\right) + \left(-1\right)\right)} + 2\right) - 2 \]
   metadata-eval [=>] 98.9	\[ \left(\cos^{-1} \left(\left(4 \cdot {v}^{2} + \left(4 \cdot {v}^{4} + 4 \cdot {v}^{6}\right)\right) + \color{blue}{-1}\right) + 2\right) - 2 \]
   +-commutative [=>] 98.9	\[ \left(\cos^{-1} \color{blue}{\left(-1 + \left(4 \cdot {v}^{2} + \left(4 \cdot {v}^{4} + 4 \cdot {v}^{6}\right)\right)\right)} + 2\right) - 2 \]
   associate-+r+ [=>] 98.9	\[ \left(\cos^{-1} \left(-1 + \color{blue}{\left(\left(4 \cdot {v}^{2} + 4 \cdot {v}^{4}\right) + 4 \cdot {v}^{6}\right)}\right) + 2\right) - 2 \]
   distribute-lft-out [=>] 98.9	\[ \left(\cos^{-1} \left(-1 + \left(\color{blue}{4 \cdot \left({v}^{2} + {v}^{4}\right)} + 4 \cdot {v}^{6}\right)\right) + 2\right) - 2 \]
   distribute-lft-out [=>] 98.9	\[ \left(\cos^{-1} \left(-1 + \color{blue}{4 \cdot \left(\left({v}^{2} + {v}^{4}\right) + {v}^{6}\right)}\right) + 2\right) - 2 \]
   unpow2 [=>] 98.9	\[ \left(\cos^{-1} \left(-1 + 4 \cdot \left(\left(\color{blue}{v \cdot v} + {v}^{4}\right) + {v}^{6}\right)\right) + 2\right) - 2 \]
   fma-def [=>] 98.9	\[ \left(\cos^{-1} \left(-1 + 4 \cdot \left(\color{blue}{\mathsf{fma}\left(v, v, {v}^{4}\right)} + {v}^{6}\right)\right) + 2\right) - 2 \]

7. Final simplification 98.9%

   \[\leadsto \left(\cos^{-1} \left(-1 + 4 \cdot \left(\mathsf{fma}\left(v, v, {v}^{4}\right) + {v}^{6}\right)\right) + 2\right) + -2 \]

Alternatives

Alternative 1
Accuracy	99.1%
Cost	7488

\[\left(2 + \cos^{-1} \left(\frac{-1 + \left(v \cdot v\right) \cdot 5}{1 - v \cdot v}\right)\right) + -2 \]

Alternative 2
Accuracy	99.1%
Cost	7232

\[\cos^{-1} \left(\frac{1 + \left(v \cdot v\right) \cdot -5}{-1 + v \cdot v}\right) \]

Alternative 3
Accuracy	97.9%
Cost	6464

\[\cos^{-1} -1 \]

Reproduce

herbie shell --seed 2023140 
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 1"
  :precision binary64
  (acos (/ (- 1.0 (* 5.0 (* v v))) (- (* v v) 1.0))))