ENA, Section 1.4, Exercise 4d

Average Accuracy: 61.2% → 98.2%

Time: 8.1s

Precision: binary64

Cost: 20164

\[\left(0 \leq x \land x \leq 1000000000\right) \land \left(-1 \leq \varepsilon \land \varepsilon \leq 1\right)\]

Math

\[x - \sqrt{x \cdot x - \varepsilon} \]

↓

\[\begin{array}{l} \mathbf{if}\;x - \sqrt{x \cdot x - \varepsilon} \leq -2 \cdot 10^{-150}:\\ \;\;\;\;\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(0.125, \frac{\varepsilon}{x \cdot x} \cdot \frac{\varepsilon}{x}, \frac{\varepsilon}{x} \cdot 0.5\right)\\ \end{array} \]

FPCore

(FPCore (x eps) :precision binary64 (- x (sqrt (- (* x x) eps))))

↓

(FPCore (x eps)
 :precision binary64
 (if (<= (- x (sqrt (- (* x x) eps))) -2e-150)
   (/ eps (+ x (hypot x (sqrt (- eps)))))
   (fma 0.125 (* (/ eps (* x x)) (/ eps x)) (* (/ eps x) 0.5))))

C

double code(double x, double eps) {
	return x - sqrt(((x * x) - eps));
}

↓

double code(double x, double eps) {
	double tmp;
	if ((x - sqrt(((x * x) - eps))) <= -2e-150) {
		tmp = eps / (x + hypot(x, sqrt(-eps)));
	} else {
		tmp = fma(0.125, ((eps / (x * x)) * (eps / x)), ((eps / x) * 0.5));
	}
	return tmp;
}

Julia

function code(x, eps)
	return Float64(x - sqrt(Float64(Float64(x * x) - eps)))
end

↓

function code(x, eps)
	tmp = 0.0
	if (Float64(x - sqrt(Float64(Float64(x * x) - eps))) <= -2e-150)
		tmp = Float64(eps / Float64(x + hypot(x, sqrt(Float64(-eps)))));
	else
		tmp = fma(0.125, Float64(Float64(eps / Float64(x * x)) * Float64(eps / x)), Float64(Float64(eps / x) * 0.5));
	end
	return tmp
end

Wolfram

code[x_, eps_] := N[(x - N[Sqrt[N[(N[(x * x), $MachinePrecision] - eps), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]

↓

code[x_, eps_] := If[LessEqual[N[(x - N[Sqrt[N[(N[(x * x), $MachinePrecision] - eps), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], -2e-150], N[(eps / N[(x + N[Sqrt[x ^ 2 + N[Sqrt[(-eps)], $MachinePrecision] ^ 2], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(0.125 * N[(N[(eps / N[(x * x), $MachinePrecision]), $MachinePrecision] * N[(eps / x), $MachinePrecision]), $MachinePrecision] + N[(N[(eps / x), $MachinePrecision] * 0.5), $MachinePrecision]), $MachinePrecision]]

Target

Original	61.2%
Target	99.5%
Herbie	98.2%

\[\frac{\varepsilon}{x + \sqrt{x \cdot x - \varepsilon}} \]

Derivation

1. Split input into 2 regimes

2. if (-.f64 x (sqrt.f64 (-.f64 (*.f64 x x) eps))) < -2.00000000000000001e-150

   1. Initial program 98.5%

      \[x - \sqrt{x \cdot x - \varepsilon} \]

   2. Applied egg-rr 97.8%

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

      [Start] 98.5	\[ x - \sqrt{x \cdot x - \varepsilon} \]
      flip-- [=>] 98.3	\[ \color{blue}{\frac{x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}}{x + \sqrt{x \cdot x - \varepsilon}}} \]
      div-inv [=>] 98.1	\[ \color{blue}{\left(x \cdot x - \sqrt{x \cdot x - \varepsilon} \cdot \sqrt{x \cdot x - \varepsilon}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}}} \]
      add-sqr-sqrt [<=] 97.8	\[ \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]
      sub-neg [=>] 97.8	\[ \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{\color{blue}{x \cdot x + \left(-\varepsilon\right)}}} \]
      add-sqr-sqrt [=>] 97.8	\[ \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \sqrt{x \cdot x + \color{blue}{\sqrt{-\varepsilon} \cdot \sqrt{-\varepsilon}}}} \]
      hypot-def [=>] 97.8	\[ \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \color{blue}{\mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]

   3. Simplified 99.2%

      \[\leadsto \color{blue}{\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]
      Proof

      [Start] 97.8	\[ \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]
      associate-*r/ [=>] 97.8	\[ \color{blue}{\frac{\left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot 1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}} \]
      *-rgt-identity [=>] 97.8	\[ \frac{\color{blue}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]
      associate--r- [=>] 99.2	\[ \frac{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]
      +-inverses [=>] 99.2	\[ \frac{\color{blue}{0} + \varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]
      +-lft-identity [=>] 99.2	\[ \frac{\color{blue}{\varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   if -2.00000000000000001e-150 < (-.f64 x (sqrt.f64 (-.f64 (*.f64 x x) eps)))

   1. Initial program 10.1%

      \[x - \sqrt{x \cdot x - \varepsilon} \]

   2. Taylor expanded in x around inf 90.2%

      \[\leadsto \color{blue}{0.125 \cdot \frac{{\varepsilon}^{2}}{{x}^{3}} + 0.5 \cdot \frac{\varepsilon}{x}} \]

   3. Simplified 90.2%

      \[\leadsto \color{blue}{\mathsf{fma}\left(0.125, \frac{\varepsilon \cdot \varepsilon}{{x}^{3}}, 0.5 \cdot \frac{\varepsilon}{x}\right)} \]
      Proof

      [Start] 90.2	\[ 0.125 \cdot \frac{{\varepsilon}^{2}}{{x}^{3}} + 0.5 \cdot \frac{\varepsilon}{x} \]
      fma-def [=>] 90.2	\[ \color{blue}{\mathsf{fma}\left(0.125, \frac{{\varepsilon}^{2}}{{x}^{3}}, 0.5 \cdot \frac{\varepsilon}{x}\right)} \]
      unpow2 [=>] 90.2	\[ \mathsf{fma}\left(0.125, \frac{\color{blue}{\varepsilon \cdot \varepsilon}}{{x}^{3}}, 0.5 \cdot \frac{\varepsilon}{x}\right) \]

   4. Applied egg-rr 96.9%

      \[\leadsto \mathsf{fma}\left(0.125, \color{blue}{\frac{\varepsilon}{x \cdot x} \cdot \frac{\varepsilon}{x}}, 0.5 \cdot \frac{\varepsilon}{x}\right) \]
      Proof

      [Start] 90.2	\[ \mathsf{fma}\left(0.125, \frac{\varepsilon \cdot \varepsilon}{{x}^{3}}, 0.5 \cdot \frac{\varepsilon}{x}\right) \]
      unpow3 [=>] 90.2	\[ \mathsf{fma}\left(0.125, \frac{\varepsilon \cdot \varepsilon}{\color{blue}{\left(x \cdot x\right) \cdot x}}, 0.5 \cdot \frac{\varepsilon}{x}\right) \]
      times-frac [=>] 96.9	\[ \mathsf{fma}\left(0.125, \color{blue}{\frac{\varepsilon}{x \cdot x} \cdot \frac{\varepsilon}{x}}, 0.5 \cdot \frac{\varepsilon}{x}\right) \]

3. Recombined 2 regimes into one program.

4. Final simplification 98.2%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x - \sqrt{x \cdot x - \varepsilon} \leq -2 \cdot 10^{-150}:\\ \;\;\;\;\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(0.125, \frac{\varepsilon}{x \cdot x} \cdot \frac{\varepsilon}{x}, \frac{\varepsilon}{x} \cdot 0.5\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	97.8%
Cost	14276

\[\begin{array}{l} t_0 := x - \sqrt{x \cdot x - \varepsilon}\\ \mathbf{if}\;t_0 \leq -2 \cdot 10^{-150}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(0.125, \frac{\varepsilon}{x \cdot x} \cdot \frac{\varepsilon}{x}, \frac{\varepsilon}{x} \cdot 0.5\right)\\ \end{array} \]

Alternative 2
Accuracy	97.9%
Cost	13764

\[\begin{array}{l} t_0 := x - \sqrt{x \cdot x - \varepsilon}\\ \mathbf{if}\;t_0 \leq -2 \cdot 10^{-150}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon}{x + \left(x + \frac{\varepsilon}{x} \cdot -0.5\right)}\\ \end{array} \]

Alternative 3
Accuracy	77.4%
Cost	7053

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -9.2 \cdot 10^{-270} \lor \neg \left(\varepsilon \leq -5.5 \cdot 10^{-282}\right) \land \varepsilon \leq -9 \cdot 10^{-300}:\\ \;\;\;\;x - \sqrt{-\varepsilon}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon}{x + \left(x + \frac{\varepsilon}{x} \cdot -0.5\right)}\\ \end{array} \]

Alternative 4
Accuracy	46.1%
Cost	704

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

Alternative 5
Accuracy	46.1%
Cost	704

\[\frac{\varepsilon}{\frac{\varepsilon}{x} \cdot -0.5 + x \cdot 2} \]

Alternative 6
Accuracy	45.2%
Cost	320

\[\frac{\varepsilon}{x} \cdot 0.5 \]

Alternative 7
Accuracy	5.4%
Cost	192

\[x \cdot -2 \]

Alternative 8
Accuracy	3.5%
Cost	64

\[x \]

Reproduce

herbie shell --seed 2023147 
(FPCore (x eps)
  :name "ENA, Section 1.4, Exercise 4d"
  :precision binary64
  :pre (and (and (<= 0.0 x) (<= x 1000000000.0)) (and (<= -1.0 eps) (<= eps 1.0)))

  :herbie-target
  (/ eps (+ x (sqrt (- (* x x) eps))))

  (- x (sqrt (- (* x x) eps))))