Rust f32::acosh

Average Accuracy: 49.2% → 99.9%

Time: 7.9s

Precision: binary32

Cost: 13476

\[x \geq 1\]

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x + \sqrt{x \cdot x + -1} \leq 2000000000:\\ \;\;\;\;\log \left(x + \sqrt{\frac{\mathsf{fma}\left(x, x, -1\right) \cdot \left(x + -1\right)}{x + -1}}\right)\\ \mathbf{else}:\\ \;\;\;\;\left|\log \left(\frac{0.5}{x}\right)\right|\\ \end{array} \]

FPCore

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

↓

(FPCore (x)
 :precision binary32
 (if (<= (+ x (sqrt (+ (* x x) -1.0))) 2000000000.0)
   (log (+ x (sqrt (/ (* (fma x x -1.0) (+ x -1.0)) (+ x -1.0)))))
   (fabs (log (/ 0.5 x)))))

C

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

↓

float code(float x) {
	float tmp;
	if ((x + sqrtf(((x * x) + -1.0f))) <= 2000000000.0f) {
		tmp = logf((x + sqrtf(((fmaf(x, x, -1.0f) * (x + -1.0f)) / (x + -1.0f)))));
	} else {
		tmp = fabsf(logf((0.5f / x)));
	}
	return tmp;
}

Julia

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

↓

function code(x)
	tmp = Float32(0.0)
	if (Float32(x + sqrt(Float32(Float32(x * x) + Float32(-1.0)))) <= Float32(2000000000.0))
		tmp = log(Float32(x + sqrt(Float32(Float32(fma(x, x, Float32(-1.0)) * Float32(x + Float32(-1.0))) / Float32(x + Float32(-1.0))))));
	else
		tmp = abs(log(Float32(Float32(0.5) / x)));
	end
	return tmp
end

Target

Original	49.2%
Target	99.1%
Herbie	99.9%

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

Derivation

1. Split input into 2 regimes

2. if (+.f32 x (sqrt.f32 (-.f32 (*.f32 x x) 1))) < 2e9

   1. Initial program 99.8%

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

   2. Applied egg-rr 99.8%

      \[\leadsto \log \left(x + \sqrt{\color{blue}{\frac{\mathsf{fma}\left(x, x, -1\right) \cdot \left(x + -1\right)}{x + -1}}}\right) \]
      Proof

      [Start] 99.8	\[ \log \left(x + \sqrt{x \cdot x - 1}\right) \]
      difference-of-sqr-1 [=>] 99.8	\[ \log \left(x + \sqrt{\color{blue}{\left(x + 1\right) \cdot \left(x - 1\right)}}\right) \]
      flip-+ [=>] 99.8	\[ \log \left(x + \sqrt{\color{blue}{\frac{x \cdot x - 1 \cdot 1}{x - 1}} \cdot \left(x - 1\right)}\right) \]
      metadata-eval [=>] 99.8	\[ \log \left(x + \sqrt{\frac{x \cdot x - \color{blue}{1}}{x - 1} \cdot \left(x - 1\right)}\right) \]
      associate-*l/ [=>] 99.8	\[ \log \left(x + \sqrt{\color{blue}{\frac{\left(x \cdot x - 1\right) \cdot \left(x - 1\right)}{x - 1}}}\right) \]
      fma-neg [=>] 99.8	\[ \log \left(x + \sqrt{\frac{\color{blue}{\mathsf{fma}\left(x, x, -1\right)} \cdot \left(x - 1\right)}{x - 1}}\right) \]
      metadata-eval [=>] 99.8	\[ \log \left(x + \sqrt{\frac{\mathsf{fma}\left(x, x, \color{blue}{-1}\right) \cdot \left(x - 1\right)}{x - 1}}\right) \]
      sub-neg [=>] 99.8	\[ \log \left(x + \sqrt{\frac{\mathsf{fma}\left(x, x, -1\right) \cdot \color{blue}{\left(x + \left(-1\right)\right)}}{x - 1}}\right) \]
      metadata-eval [=>] 99.8	\[ \log \left(x + \sqrt{\frac{\mathsf{fma}\left(x, x, -1\right) \cdot \left(x + \color{blue}{-1}\right)}{x - 1}}\right) \]
      sub-neg [=>] 99.8	\[ \log \left(x + \sqrt{\frac{\mathsf{fma}\left(x, x, -1\right) \cdot \left(x + -1\right)}{\color{blue}{x + \left(-1\right)}}}\right) \]
      metadata-eval [=>] 99.8	\[ \log \left(x + \sqrt{\frac{\mathsf{fma}\left(x, x, -1\right) \cdot \left(x + -1\right)}{x + \color{blue}{-1}}}\right) \]

   if 2e9 < (+.f32 x (sqrt.f32 (-.f32 (*.f32 x x) 1)))

   1. Initial program 34.2%

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

   2. Taylor expanded in x around -inf 3.0%

      \[\leadsto \log \color{blue}{\left(\frac{0.5}{x}\right)} \]

   3. Applied egg-rr 100.0%

      \[\leadsto \color{blue}{\sqrt{{\log \left(\frac{0.5}{x}\right)}^{2}}} \]
      Proof

      [Start] 3.0	\[ \log \left(\frac{0.5}{x}\right) \]
      add-sqr-sqrt [=>] -0.0	\[ \color{blue}{\sqrt{\log \left(\frac{0.5}{x}\right)} \cdot \sqrt{\log \left(\frac{0.5}{x}\right)}} \]
      sqrt-unprod [=>] 100.0	\[ \color{blue}{\sqrt{\log \left(\frac{0.5}{x}\right) \cdot \log \left(\frac{0.5}{x}\right)}} \]
      pow2 [=>] 100.0	\[ \sqrt{\color{blue}{{\log \left(\frac{0.5}{x}\right)}^{2}}} \]

   4. Applied egg-rr 100.0%

      \[\leadsto \color{blue}{\left|\log \left(\frac{0.5}{x}\right)\right|} \]
      Proof

      [Start] 100.0	\[ \sqrt{{\log \left(\frac{0.5}{x}\right)}^{2}} \]
      unpow2 [=>] 100.0	\[ \sqrt{\color{blue}{\log \left(\frac{0.5}{x}\right) \cdot \log \left(\frac{0.5}{x}\right)}} \]
      rem-sqrt-square [=>] 100.0	\[ \color{blue}{\left|\log \left(\frac{0.5}{x}\right)\right|} \]

3. Recombined 2 regimes into one program.

4. Final simplification 99.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x + \sqrt{x \cdot x + -1} \leq 2000000000:\\ \;\;\;\;\log \left(x + \sqrt{\frac{\mathsf{fma}\left(x, x, -1\right) \cdot \left(x + -1\right)}{x + -1}}\right)\\ \mathbf{else}:\\ \;\;\;\;\left|\log \left(\frac{0.5}{x}\right)\right|\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	100.0%
Cost	10148

\[\begin{array}{l} \mathbf{if}\;x + \sqrt{x \cdot x + -1} \leq 7999999895928832:\\ \;\;\;\;\log \left(x + \sqrt{\left(x + -1\right) \cdot \left(x + 1\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\left|\log \left(\frac{0.5}{x}\right)\right|\\ \end{array} \]

Alternative 2
Accuracy	100.0%
Cost	10084

\[\begin{array}{l} t_0 := x + \sqrt{x \cdot x + -1}\\ \mathbf{if}\;t_0 \leq 7999999895928832:\\ \;\;\;\;\log t_0\\ \mathbf{else}:\\ \;\;\;\;\left|\log \left(\frac{0.5}{x}\right)\right|\\ \end{array} \]

Alternative 3
Accuracy	98.2%
Cost	3424

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

Alternative 4
Accuracy	96.8%
Cost	3296

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

Alternative 5
Accuracy	18.7%
Cost	3232

\[\mathsf{log1p}\left(0.125\right) \]

Alternative 6
Accuracy	19.9%
Cost	3232

\[\mathsf{log1p}\left(0.5\right) \]

Alternative 7
Accuracy	21.2%
Cost	3232

\[\mathsf{log1p}\left(2\right) \]

Alternative 8
Accuracy	44.3%
Cost	3232

\[\mathsf{log1p}\left(x\right) \]

Alternative 9
Accuracy	6.1%
Cost	32

\[0 \]

Reproduce

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