Rust f32::acosh

Percentage Accurate: 52.1% → 98.6%

Time: 4.8s

Precision: binary32

Cost: 7040

\[x \geq 1\]

Math

\[\log \left(x + \sqrt{x \cdot x - 1}\right) \]

↓

\[\log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\frac{\frac{0.125}{x \cdot x}}{x} + 0.0625 \cdot {x}^{-5}\right)\right) \]

FPCore

(FPCore (x) :precision binary32 (log (+ x (sqrt (- (* x x) 1.0)))))

↓

(FPCore (x)
 :precision binary32
 (log
  (-
   (- (* x 2.0) (/ 0.5 x))
   (+ (/ (/ 0.125 (* x x)) x) (* 0.0625 (pow x -5.0))))))

C

float code(float x) {
	return logf((x + sqrtf(((x * x) - 1.0f))));
}

↓

float code(float x) {
	return logf((((x * 2.0f) - (0.5f / x)) - (((0.125f / (x * x)) / x) + (0.0625f * powf(x, -5.0f)))));
}

Fortran

real(4) function code(x)
    real(4), intent (in) :: x
    code = log((x + sqrt(((x * x) - 1.0e0))))
end function

↓

real(4) function code(x)
    real(4), intent (in) :: x
    code = log((((x * 2.0e0) - (0.5e0 / x)) - (((0.125e0 / (x * x)) / x) + (0.0625e0 * (x ** (-5.0e0))))))
end function

Julia

function code(x)
	return log(Float32(x + sqrt(Float32(Float32(x * x) - Float32(1.0)))))
end

↓

function code(x)
	return log(Float32(Float32(Float32(x * Float32(2.0)) - Float32(Float32(0.5) / x)) - Float32(Float32(Float32(Float32(0.125) / Float32(x * x)) / x) + Float32(Float32(0.0625) * (x ^ Float32(-5.0))))))
end

MATLAB

function tmp = code(x)
	tmp = log((x + sqrt(((x * x) - single(1.0)))));
end

↓

function tmp = code(x)
	tmp = log((((x * single(2.0)) - (single(0.5) / x)) - (((single(0.125) / (x * x)) / x) + (single(0.0625) * (x ^ single(-5.0))))));
end

Target

Original	52.1%
Target	99.0%
Herbie	98.6%

\[\log \left(x + \sqrt{x - 1} \cdot \sqrt{x + 1}\right) \]

Derivation

1. Initial program 55.0%

   \[\log \left(x + \sqrt{x \cdot x - 1}\right) \]

2. Taylor expanded in x around inf 99.5%

   \[\leadsto \log \color{blue}{\left(2 \cdot x - \left(0.5 \cdot \frac{1}{x} + \left(0.0625 \cdot \frac{1}{{x}^{5}} + 0.125 \cdot \frac{1}{{x}^{3}}\right)\right)\right)} \]

3. Simplified 99.5%

   \[\leadsto \log \color{blue}{\left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\frac{0.125}{{x}^{3}} + \frac{0.0625}{{x}^{5}}\right)\right)} \]
   Step-by-step derivation

   [Start] 99.5	\[ \log \left(2 \cdot x - \left(0.5 \cdot \frac{1}{x} + \left(0.0625 \cdot \frac{1}{{x}^{5}} + 0.125 \cdot \frac{1}{{x}^{3}}\right)\right)\right) \]
   associate--r+ [=>] 99.5	\[ \log \color{blue}{\left(\left(2 \cdot x - 0.5 \cdot \frac{1}{x}\right) - \left(0.0625 \cdot \frac{1}{{x}^{5}} + 0.125 \cdot \frac{1}{{x}^{3}}\right)\right)} \]
   *-commutative [=>] 99.5	\[ \log \left(\left(\color{blue}{x \cdot 2} - 0.5 \cdot \frac{1}{x}\right) - \left(0.0625 \cdot \frac{1}{{x}^{5}} + 0.125 \cdot \frac{1}{{x}^{3}}\right)\right) \]
   associate-*r/ [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \color{blue}{\frac{0.5 \cdot 1}{x}}\right) - \left(0.0625 \cdot \frac{1}{{x}^{5}} + 0.125 \cdot \frac{1}{{x}^{3}}\right)\right) \]
   metadata-eval [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{\color{blue}{0.5}}{x}\right) - \left(0.0625 \cdot \frac{1}{{x}^{5}} + 0.125 \cdot \frac{1}{{x}^{3}}\right)\right) \]
   +-commutative [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \color{blue}{\left(0.125 \cdot \frac{1}{{x}^{3}} + 0.0625 \cdot \frac{1}{{x}^{5}}\right)}\right) \]
   associate-*r/ [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\color{blue}{\frac{0.125 \cdot 1}{{x}^{3}}} + 0.0625 \cdot \frac{1}{{x}^{5}}\right)\right) \]
   metadata-eval [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\frac{\color{blue}{0.125}}{{x}^{3}} + 0.0625 \cdot \frac{1}{{x}^{5}}\right)\right) \]
   associate-*r/ [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\frac{0.125}{{x}^{3}} + \color{blue}{\frac{0.0625 \cdot 1}{{x}^{5}}}\right)\right) \]
   metadata-eval [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\frac{0.125}{{x}^{3}} + \frac{\color{blue}{0.0625}}{{x}^{5}}\right)\right) \]

4. Applied egg-rr 99.5%

   \[\leadsto \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \color{blue}{\mathsf{fma}\left(\frac{0.25}{x \cdot x}, \frac{0.5}{x}, 0.0625 \cdot {x}^{-5}\right)}\right) \]
   Step-by-step derivation

   [Start] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\frac{0.125}{{x}^{3}} + \frac{0.0625}{{x}^{5}}\right)\right) \]
   add-cube-cbrt [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\color{blue}{\left(\sqrt[3]{\frac{0.125}{{x}^{3}}} \cdot \sqrt[3]{\frac{0.125}{{x}^{3}}}\right) \cdot \sqrt[3]{\frac{0.125}{{x}^{3}}}} + \frac{0.0625}{{x}^{5}}\right)\right) \]
   fma-def [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \color{blue}{\mathsf{fma}\left(\sqrt[3]{\frac{0.125}{{x}^{3}}} \cdot \sqrt[3]{\frac{0.125}{{x}^{3}}}, \sqrt[3]{\frac{0.125}{{x}^{3}}}, \frac{0.0625}{{x}^{5}}\right)}\right) \]
   pow2 [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left(\color{blue}{{\left(\sqrt[3]{\frac{0.125}{{x}^{3}}}\right)}^{2}}, \sqrt[3]{\frac{0.125}{{x}^{3}}}, \frac{0.0625}{{x}^{5}}\right)\right) \]
   metadata-eval [<=] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left({\left(\sqrt[3]{\frac{\color{blue}{{0.5}^{3}}}{{x}^{3}}}\right)}^{2}, \sqrt[3]{\frac{0.125}{{x}^{3}}}, \frac{0.0625}{{x}^{5}}\right)\right) \]
   cube-div [<=] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left({\left(\sqrt[3]{\color{blue}{{\left(\frac{0.5}{x}\right)}^{3}}}\right)}^{2}, \sqrt[3]{\frac{0.125}{{x}^{3}}}, \frac{0.0625}{{x}^{5}}\right)\right) \]
   pow3 [<=] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left({\left(\sqrt[3]{\color{blue}{\left(\frac{0.5}{x} \cdot \frac{0.5}{x}\right) \cdot \frac{0.5}{x}}}\right)}^{2}, \sqrt[3]{\frac{0.125}{{x}^{3}}}, \frac{0.0625}{{x}^{5}}\right)\right) \]
   add-cbrt-cube [<=] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left({\color{blue}{\left(\frac{0.5}{x}\right)}}^{2}, \sqrt[3]{\frac{0.125}{{x}^{3}}}, \frac{0.0625}{{x}^{5}}\right)\right) \]
   pow2 [<=] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left(\color{blue}{\frac{0.5}{x} \cdot \frac{0.5}{x}}, \sqrt[3]{\frac{0.125}{{x}^{3}}}, \frac{0.0625}{{x}^{5}}\right)\right) \]
   frac-times [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left(\color{blue}{\frac{0.5 \cdot 0.5}{x \cdot x}}, \sqrt[3]{\frac{0.125}{{x}^{3}}}, \frac{0.0625}{{x}^{5}}\right)\right) \]
   metadata-eval [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left(\frac{\color{blue}{0.25}}{x \cdot x}, \sqrt[3]{\frac{0.125}{{x}^{3}}}, \frac{0.0625}{{x}^{5}}\right)\right) \]
   metadata-eval [<=] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left(\frac{0.25}{x \cdot x}, \sqrt[3]{\frac{\color{blue}{{0.5}^{3}}}{{x}^{3}}}, \frac{0.0625}{{x}^{5}}\right)\right) \]
   cube-div [<=] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left(\frac{0.25}{x \cdot x}, \sqrt[3]{\color{blue}{{\left(\frac{0.5}{x}\right)}^{3}}}, \frac{0.0625}{{x}^{5}}\right)\right) \]
   pow3 [<=] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left(\frac{0.25}{x \cdot x}, \sqrt[3]{\color{blue}{\left(\frac{0.5}{x} \cdot \frac{0.5}{x}\right) \cdot \frac{0.5}{x}}}, \frac{0.0625}{{x}^{5}}\right)\right) \]
   add-cbrt-cube [<=] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left(\frac{0.25}{x \cdot x}, \color{blue}{\frac{0.5}{x}}, \frac{0.0625}{{x}^{5}}\right)\right) \]
   div-inv [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left(\frac{0.25}{x \cdot x}, \frac{0.5}{x}, \color{blue}{0.0625 \cdot \frac{1}{{x}^{5}}}\right)\right) \]
   pow-flip [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left(\frac{0.25}{x \cdot x}, \frac{0.5}{x}, 0.0625 \cdot \color{blue}{{x}^{\left(-5\right)}}\right)\right) \]
   metadata-eval [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left(\frac{0.25}{x \cdot x}, \frac{0.5}{x}, 0.0625 \cdot {x}^{\color{blue}{-5}}\right)\right) \]

5. Simplified 99.5%

   \[\leadsto \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \color{blue}{\left(\frac{\frac{0.125}{x \cdot x}}{x} + 0.0625 \cdot {x}^{-5}\right)}\right) \]
   Step-by-step derivation

   [Start] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \mathsf{fma}\left(\frac{0.25}{x \cdot x}, \frac{0.5}{x}, 0.0625 \cdot {x}^{-5}\right)\right) \]
   fma-udef [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \color{blue}{\left(\frac{0.25}{x \cdot x} \cdot \frac{0.5}{x} + 0.0625 \cdot {x}^{-5}\right)}\right) \]
   associate-*r/ [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\color{blue}{\frac{\frac{0.25}{x \cdot x} \cdot 0.5}{x}} + 0.0625 \cdot {x}^{-5}\right)\right) \]
   unpow2 [<=] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\frac{\frac{0.25}{\color{blue}{{x}^{2}}} \cdot 0.5}{x} + 0.0625 \cdot {x}^{-5}\right)\right) \]
   associate-*l/ [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\frac{\color{blue}{\frac{0.25 \cdot 0.5}{{x}^{2}}}}{x} + 0.0625 \cdot {x}^{-5}\right)\right) \]
   metadata-eval [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\frac{\frac{\color{blue}{0.125}}{{x}^{2}}}{x} + 0.0625 \cdot {x}^{-5}\right)\right) \]
   unpow2 [=>] 99.5	\[ \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\frac{\frac{0.125}{\color{blue}{x \cdot x}}}{x} + 0.0625 \cdot {x}^{-5}\right)\right) \]

6. Final simplification 99.5%

   \[\leadsto \log \left(\left(x \cdot 2 - \frac{0.5}{x}\right) - \left(\frac{\frac{0.125}{x \cdot x}}{x} + 0.0625 \cdot {x}^{-5}\right)\right) \]

Alternatives

Alternative 1
Accuracy	98.0%
Cost	3424

\[\log \left(x \cdot 2 - \frac{0.5}{x}\right) \]

Alternative 2
Accuracy	96.8%
Cost	3296

\[\log \left(x + x\right) \]

Alternative 3
Accuracy	6.1%
Cost	32

\[0 \]

Reproduce

herbie shell --seed 2023160 
(FPCore (x)
  :name "Rust f32::acosh"
  :precision binary32
  :pre (>= x 1.0)

  :herbie-target
  (log (+ x (* (sqrt (- x 1.0)) (sqrt (+ x 1.0)))))

  (log (+ x (sqrt (- (* x x) 1.0)))))