ENA, Section 1.4, Exercise 4d

Average Accuracy: 62.1% → 99.1%

Time: 6.4s

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 -1 \cdot 10^{-153}:\\ \;\;\;\;\frac{\varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon}{x + \left(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))) -1e-153)
   (/ eps (+ x (hypot x (sqrt (- eps)))))
   (/ eps (+ x (+ 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))) <= -1e-153) {
		tmp = eps / (x + hypot(x, sqrt(-eps)));
	} else {
		tmp = eps / (x + (x + ((eps / x) * -0.5)));
	}
	return tmp;
}

Java

public static double code(double x, double eps) {
	return x - Math.sqrt(((x * x) - eps));
}

↓

public static double code(double x, double eps) {
	double tmp;
	if ((x - Math.sqrt(((x * x) - eps))) <= -1e-153) {
		tmp = eps / (x + Math.hypot(x, Math.sqrt(-eps)));
	} else {
		tmp = eps / (x + (x + ((eps / x) * -0.5)));
	}
	return tmp;
}

Python

def code(x, eps):
	return x - math.sqrt(((x * x) - eps))

↓

def code(x, eps):
	tmp = 0
	if (x - math.sqrt(((x * x) - eps))) <= -1e-153:
		tmp = eps / (x + math.hypot(x, math.sqrt(-eps)))
	else:
		tmp = eps / (x + (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))) <= -1e-153)
		tmp = Float64(eps / Float64(x + hypot(x, sqrt(Float64(-eps)))));
	else
		tmp = Float64(eps / Float64(x + Float64(x + Float64(Float64(eps / x) * -0.5))));
	end
	return tmp
end

MATLAB

function tmp = code(x, eps)
	tmp = x - sqrt(((x * x) - eps));
end

↓

function tmp_2 = code(x, eps)
	tmp = 0.0;
	if ((x - sqrt(((x * x) - eps))) <= -1e-153)
		tmp = eps / (x + hypot(x, sqrt(-eps)));
	else
		tmp = eps / (x + (x + ((eps / x) * -0.5)));
	end
	tmp_2 = 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], -1e-153], N[(eps / N[(x + N[Sqrt[x ^ 2 + N[Sqrt[(-eps)], $MachinePrecision] ^ 2], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(eps / N[(x + N[(x + N[(N[(eps / x), $MachinePrecision] * -0.5), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

Target

Original	62.1%
Target	99.5%
Herbie	99.1%

\[\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))) < -1.00000000000000004e-153

   1. Initial program 98.6%

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

   2. Applied egg-rr 97.9%

      \[\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.6	\[ x - \sqrt{x \cdot x - \varepsilon} \]
      flip-- [=>] 98.4	\[ \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.9	\[ \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.9	\[ \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.9	\[ \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.9	\[ \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.3%

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

      [Start] 97.9	\[ \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.9	\[ \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.9	\[ \frac{\color{blue}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]
      associate--r- [=>] 99.3	\[ \frac{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]
      +-inverses [=>] 99.3	\[ \frac{\color{blue}{0} + \varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]
      +-lft-identity [=>] 99.3	\[ \frac{\color{blue}{\varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   if -1.00000000000000004e-153 < (-.f64 x (sqrt.f64 (-.f64 (*.f64 x x) eps)))

   1. Initial program 8.4%

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

   2. Applied egg-rr 3.0%

      \[\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] 8.4	\[ x - \sqrt{x \cdot x - \varepsilon} \]
      flip-- [=>] 8.4	\[ \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 [=>] 8.4	\[ \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 [<=] 8.5	\[ \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]
      sub-neg [=>] 8.5	\[ \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 [=>] 3.0	\[ \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 [=>] 3.0	\[ \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 48.2%

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

      [Start] 3.0	\[ \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]
      associate-*r/ [=>] 3.0	\[ \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 [=>] 3.0	\[ \frac{\color{blue}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]
      associate--r- [=>] 48.2	\[ \frac{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]
      +-inverses [=>] 48.2	\[ \frac{\color{blue}{0} + \varepsilon}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]
      +-lft-identity [=>] 48.2	\[ \frac{\color{blue}{\varepsilon}}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]

   4. Taylor expanded in x around inf 0.0%

      \[\leadsto \frac{\varepsilon}{x + \color{blue}{\left(0.5 \cdot \frac{\varepsilon \cdot {\left(\sqrt{-1}\right)}^{2}}{x} + x\right)}} \]

   5. Simplified 98.8%

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

      [Start] 0.0	\[ \frac{\varepsilon}{x + \left(0.5 \cdot \frac{\varepsilon \cdot {\left(\sqrt{-1}\right)}^{2}}{x} + x\right)} \]
      +-commutative [=>] 0.0	\[ \frac{\varepsilon}{x + \color{blue}{\left(x + 0.5 \cdot \frac{\varepsilon \cdot {\left(\sqrt{-1}\right)}^{2}}{x}\right)}} \]
      associate-*r/ [=>] 0.0	\[ \frac{\varepsilon}{x + \left(x + \color{blue}{\frac{0.5 \cdot \left(\varepsilon \cdot {\left(\sqrt{-1}\right)}^{2}\right)}{x}}\right)} \]
      unpow2 [=>] 0.0	\[ \frac{\varepsilon}{x + \left(x + \frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{\left(\sqrt{-1} \cdot \sqrt{-1}\right)}\right)}{x}\right)} \]
      rem-square-sqrt [=>] 98.8	\[ \frac{\varepsilon}{x + \left(x + \frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{-1}\right)}{x}\right)} \]
      *-commutative [=>] 98.8	\[ \frac{\varepsilon}{x + \left(x + \frac{0.5 \cdot \color{blue}{\left(-1 \cdot \varepsilon\right)}}{x}\right)} \]
      associate-*r* [=>] 98.8	\[ \frac{\varepsilon}{x + \left(x + \frac{\color{blue}{\left(0.5 \cdot -1\right) \cdot \varepsilon}}{x}\right)} \]
      metadata-eval [=>] 98.8	\[ \frac{\varepsilon}{x + \left(x + \frac{\color{blue}{-0.5} \cdot \varepsilon}{x}\right)} \]
      associate-*r/ [<=] 98.8	\[ \frac{\varepsilon}{x + \left(x + \color{blue}{-0.5 \cdot \frac{\varepsilon}{x}}\right)} \]
      *-commutative [=>] 98.8	\[ \frac{\varepsilon}{x + \left(x + \color{blue}{\frac{\varepsilon}{x} \cdot -0.5}\right)} \]

3. Recombined 2 regimes into one program.

4. Final simplification 99.1%

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

Alternatives

Alternative 1
Accuracy	98.6%
Cost	13764

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

Alternative 2
Accuracy	87.3%
Cost	6788

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

Alternative 3
Accuracy	45.1%
Cost	704

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

Alternative 4
Accuracy	45.1%
Cost	704

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

Alternative 5
Accuracy	44.2%
Cost	320

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

Alternative 6
Accuracy	5.3%
Cost	192

\[x \cdot -2 \]

Alternative 7
Accuracy	3.5%
Cost	64

\[x \]

Reproduce

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