ENA, Section 1.4, Exercise 4d

Percentage Accurate: 61.0% → 99.0%

Time: 5.7s

Precision: binary64

Cost: 20804

• Unsound rule application detected in e-graph. Results may not be sound.

\[\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{1}{\frac{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}{\varepsilon + \left(x \cdot x - x \cdot x\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)
   (/ 1.0 (/ (+ x (hypot x (sqrt (- eps)))) (+ eps (- (* x x) (* x x)))))
   (/ 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 = 1.0 / ((x + hypot(x, sqrt(-eps))) / (eps + ((x * x) - (x * x))));
	} 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 = 1.0 / ((x + Math.hypot(x, Math.sqrt(-eps))) / (eps + ((x * x) - (x * x))));
	} 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 = 1.0 / ((x + math.hypot(x, math.sqrt(-eps))) / (eps + ((x * x) - (x * x))))
	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(1.0 / Float64(Float64(x + hypot(x, sqrt(Float64(-eps)))) / Float64(eps + Float64(Float64(x * x) - Float64(x * x)))));
	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 = 1.0 / ((x + hypot(x, sqrt(-eps))) / (eps + ((x * x) - (x * x))));
	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[(1.0 / N[(N[(x + N[Sqrt[x ^ 2 + N[Sqrt[(-eps)], $MachinePrecision] ^ 2], $MachinePrecision]), $MachinePrecision] / N[(eps + N[(N[(x * x), $MachinePrecision] - N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(eps / N[(x + N[(x + N[(N[(eps / x), $MachinePrecision] * -0.5), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

Target

Original	61.0%
Target	99.6%
Herbie	99.0%

\[\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 98.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)}} \]
      Step-by-step derivation

      [Start] 98.6%	\[ x - \sqrt{x \cdot x - \varepsilon} \]
      flip-- [=>] 98.6%	\[ \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.2%	\[ \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 [<=] 98.0%	\[ \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]
      sub-neg [=>] 98.0%	\[ \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 [=>] 98.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 [=>] 98.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 99.3%

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

      [Start] 98.0%	\[ \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right) \cdot \frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \]
      *-commutative [=>] 98.0%	\[ \color{blue}{\frac{1}{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)} \cdot \left(x \cdot x - \left(x \cdot x - \varepsilon\right)\right)} \]
      associate-/r/ [<=] 98.0%	\[ \color{blue}{\frac{1}{\frac{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}{x \cdot x - \left(x \cdot x - \varepsilon\right)}}} \]
      associate--r- [=>] 99.3%	\[ \frac{1}{\frac{x + \mathsf{hypot}\left(x, \sqrt{-\varepsilon}\right)}{\color{blue}{\left(x \cdot x - x \cdot x\right) + \varepsilon}}} \]

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

   1. Initial program 7.3%

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

   2. Applied egg-rr 2.4%

      \[\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)}} \]
      Step-by-step derivation

      [Start] 7.3%	\[ x - \sqrt{x \cdot x - \varepsilon} \]
      flip-- [=>] 7.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 [=>] 7.3%	\[ \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 [<=] 7.4%	\[ \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]
      sub-neg [=>] 7.4%	\[ \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 [=>] 2.4%	\[ \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 [=>] 2.4%	\[ \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.6%

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

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

      \[\leadsto \frac{\varepsilon}{x + \color{blue}{\left(x + \frac{\varepsilon}{x} \cdot -0.5\right)}} \]
      Step-by-step derivation

      [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 [=>] 99.4%	\[ \frac{\varepsilon}{x + \left(x + \frac{0.5 \cdot \left(\varepsilon \cdot \color{blue}{-1}\right)}{x}\right)} \]
      *-commutative [=>] 99.4%	\[ \frac{\varepsilon}{x + \left(x + \frac{0.5 \cdot \color{blue}{\left(-1 \cdot \varepsilon\right)}}{x}\right)} \]
      associate-*r* [=>] 99.4%	\[ \frac{\varepsilon}{x + \left(x + \frac{\color{blue}{\left(0.5 \cdot -1\right) \cdot \varepsilon}}{x}\right)} \]
      metadata-eval [=>] 99.4%	\[ \frac{\varepsilon}{x + \left(x + \frac{\color{blue}{-0.5} \cdot \varepsilon}{x}\right)} \]
      associate-*r/ [<=] 99.4%	\[ \frac{\varepsilon}{x + \left(x + \color{blue}{-0.5 \cdot \frac{\varepsilon}{x}}\right)} \]
      *-commutative [=>] 99.4%	\[ \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.3%

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

Alternatives

Alternative 1
Accuracy	99.0%
Cost	20804

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

Alternative 2
Accuracy	99.0%
Cost	20164

\[\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} \]

Alternative 3
Accuracy	98.7%
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 4
Accuracy	86.9%
Cost	6788

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

Alternative 5
Accuracy	45.9%
Cost	704

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

Alternative 6
Accuracy	46.1%
Cost	704

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

Alternative 7
Accuracy	45.3%
Cost	320

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

Alternative 8
Accuracy	5.3%
Cost	192

\[x \cdot -2 \]

Reproduce

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