ENA, Section 1.4, Exercise 4d

Average Accuracy: 61.6% → 99.5%

Time: 9.3s

Precision: binary64

Cost: 13504

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

↓

\[\frac{\varepsilon}{x + \sqrt{\left(\mathsf{fma}\left(x, x, \varepsilon\right) - \varepsilon\right) - \varepsilon}} \]

FPCore

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

↓

(FPCore (x eps)
 :precision binary64
 (/ eps (+ x (sqrt (- (- (fma x x eps) eps) eps)))))

C

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

↓

double code(double x, double eps) {
	return eps / (x + sqrt(((fma(x, x, eps) - eps) - eps)));
}

Julia

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

↓

function code(x, eps)
	return Float64(eps / Float64(x + sqrt(Float64(Float64(fma(x, x, eps) - eps) - eps))))
end

Wolfram

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

↓

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

Target

Original	61.6%
Target	99.5%
Herbie	99.5%

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

Derivation

1. Initial program 61.6%

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

2. Applied egg-rr 99.4%

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

   [Start] 61.6	\[ x - \sqrt{x \cdot x - \varepsilon} \]
   flip-- [=>] 61.5	\[ \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 [=>] 61.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 [<=] 61.2	\[ \left(x \cdot x - \color{blue}{\left(x \cdot x - \varepsilon\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]
   associate--r- [=>] 99.4	\[ \color{blue}{\left(\left(x \cdot x - x \cdot x\right) + \varepsilon\right)} \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]
   +-commutative [=>] 99.4	\[ \color{blue}{\left(\varepsilon + \left(x \cdot x - x \cdot x\right)\right)} \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]
   distribute-lft-out-- [=>] 99.4	\[ \left(\varepsilon + \color{blue}{x \cdot \left(x - x\right)}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]

3. Simplified 99.4%

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

   [Start] 99.4	\[ \left(\varepsilon + x \cdot \left(x - x\right)\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]
   +-inverses [=>] 99.4	\[ \left(\varepsilon + x \cdot \color{blue}{0}\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]

4. Applied egg-rr 74.5%

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

   [Start] 99.4	\[ \left(\varepsilon + x \cdot 0\right) \cdot \frac{1}{x + \sqrt{x \cdot x - \varepsilon}} \]
   un-div-inv [=>] 99.5	\[ \color{blue}{\frac{\varepsilon + x \cdot 0}{x + \sqrt{x \cdot x - \varepsilon}}} \]
   flip-+ [=>] 49.0	\[ \frac{\color{blue}{\frac{\varepsilon \cdot \varepsilon - \left(x \cdot 0\right) \cdot \left(x \cdot 0\right)}{\varepsilon - x \cdot 0}}}{x + \sqrt{x \cdot x - \varepsilon}} \]
   associate-/l/ [=>] 47.8	\[ \color{blue}{\frac{\varepsilon \cdot \varepsilon - \left(x \cdot 0\right) \cdot \left(x \cdot 0\right)}{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)}} \]
   mul0-rgt [=>] 47.8	\[ \frac{\varepsilon \cdot \varepsilon - \color{blue}{0} \cdot \left(x \cdot 0\right)}{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)} \]
   mul0-rgt [=>] 47.8	\[ \frac{\varepsilon \cdot \varepsilon - 0 \cdot \color{blue}{0}}{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)} \]
   metadata-eval [=>] 47.8	\[ \frac{\varepsilon \cdot \varepsilon - \color{blue}{0}}{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)} \]
   --rgt-identity [=>] 47.8	\[ \frac{\color{blue}{\varepsilon \cdot \varepsilon}}{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)} \]
   +-lft-identity [<=] 47.8	\[ \frac{\varepsilon \cdot \color{blue}{\left(0 + \varepsilon\right)}}{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)} \]
   mul0-rgt [<=] 47.8	\[ \frac{\varepsilon \cdot \left(\color{blue}{x \cdot 0} + \varepsilon\right)}{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)} \]
   +-commutative [<=] 47.8	\[ \frac{\varepsilon \cdot \color{blue}{\left(\varepsilon + x \cdot 0\right)}}{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)} \]
   +-lft-identity [<=] 47.8	\[ \frac{\color{blue}{\left(0 + \varepsilon\right)} \cdot \left(\varepsilon + x \cdot 0\right)}{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)} \]
   mul0-rgt [<=] 47.8	\[ \frac{\left(\color{blue}{x \cdot 0} + \varepsilon\right) \cdot \left(\varepsilon + x \cdot 0\right)}{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)} \]
   +-commutative [<=] 47.8	\[ \frac{\color{blue}{\left(\varepsilon + x \cdot 0\right)} \cdot \left(\varepsilon + x \cdot 0\right)}{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)} \]
   associate-/l* [=>] 74.5	\[ \color{blue}{\frac{\varepsilon + x \cdot 0}{\frac{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)}{\varepsilon + x \cdot 0}}} \]
   +-commutative [=>] 74.5	\[ \frac{\color{blue}{x \cdot 0 + \varepsilon}}{\frac{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)}{\varepsilon + x \cdot 0}} \]
   mul0-rgt [=>] 74.5	\[ \frac{\color{blue}{0} + \varepsilon}{\frac{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)}{\varepsilon + x \cdot 0}} \]
   +-lft-identity [=>] 74.5	\[ \frac{\color{blue}{\varepsilon}}{\frac{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \left(\varepsilon - x \cdot 0\right)}{\varepsilon + x \cdot 0}} \]

5. Applied egg-rr 99.5%

   \[\leadsto \frac{\varepsilon}{\color{blue}{\sqrt{x \cdot x - \varepsilon} + x}} \]
   Proof

   [Start] 74.5	\[ \frac{\varepsilon}{\frac{\left(x + \sqrt{x \cdot x - \varepsilon}\right) \cdot \varepsilon}{\varepsilon}} \]
   *-commutative [=>] 74.5	\[ \frac{\varepsilon}{\frac{\color{blue}{\varepsilon \cdot \left(x + \sqrt{x \cdot x - \varepsilon}\right)}}{\varepsilon}} \]
   associate-/l* [=>] 99.5	\[ \frac{\varepsilon}{\color{blue}{\frac{\varepsilon}{\frac{\varepsilon}{x + \sqrt{x \cdot x - \varepsilon}}}}} \]
   associate-/r/ [=>] 99.5	\[ \frac{\varepsilon}{\color{blue}{\frac{\varepsilon}{\varepsilon} \cdot \left(x + \sqrt{x \cdot x - \varepsilon}\right)}} \]
   *-inverses [=>] 99.5	\[ \frac{\varepsilon}{\color{blue}{1} \cdot \left(x + \sqrt{x \cdot x - \varepsilon}\right)} \]
   *-un-lft-identity [<=] 99.5	\[ \frac{\varepsilon}{\color{blue}{x + \sqrt{x \cdot x - \varepsilon}}} \]
   +-commutative [=>] 99.5	\[ \frac{\varepsilon}{\color{blue}{\sqrt{x \cdot x - \varepsilon} + x}} \]

6. Applied egg-rr 99.5%

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

   [Start] 99.5	\[ \frac{\varepsilon}{\sqrt{x \cdot x - \varepsilon} + x} \]
   *-un-lft-identity [=>] 99.5	\[ \frac{\varepsilon}{\sqrt{x \cdot x - \color{blue}{1 \cdot \varepsilon}} + x} \]
   prod-diff [=>] 99.5	\[ \frac{\varepsilon}{\sqrt{\color{blue}{\mathsf{fma}\left(x, x, -\varepsilon \cdot 1\right) + \mathsf{fma}\left(-\varepsilon, 1, \varepsilon \cdot 1\right)}} + x} \]
   *-commutative [<=] 99.5	\[ \frac{\varepsilon}{\sqrt{\mathsf{fma}\left(x, x, -\color{blue}{1 \cdot \varepsilon}\right) + \mathsf{fma}\left(-\varepsilon, 1, \varepsilon \cdot 1\right)} + x} \]
   *-un-lft-identity [<=] 99.5	\[ \frac{\varepsilon}{\sqrt{\mathsf{fma}\left(x, x, -\color{blue}{\varepsilon}\right) + \mathsf{fma}\left(-\varepsilon, 1, \varepsilon \cdot 1\right)} + x} \]
   fma-def [<=] 99.5	\[ \frac{\varepsilon}{\sqrt{\color{blue}{\left(x \cdot x + \left(-\varepsilon\right)\right)} + \mathsf{fma}\left(-\varepsilon, 1, \varepsilon \cdot 1\right)} + x} \]
   associate-+l+ [=>] 99.5	\[ \frac{\varepsilon}{\sqrt{\color{blue}{x \cdot x + \left(\left(-\varepsilon\right) + \mathsf{fma}\left(-\varepsilon, 1, \varepsilon \cdot 1\right)\right)}} + x} \]
   *-commutative [<=] 99.5	\[ \frac{\varepsilon}{\sqrt{x \cdot x + \left(\left(-\varepsilon\right) + \mathsf{fma}\left(-\varepsilon, 1, \color{blue}{1 \cdot \varepsilon}\right)\right)} + x} \]
   *-un-lft-identity [<=] 99.5	\[ \frac{\varepsilon}{\sqrt{x \cdot x + \left(\left(-\varepsilon\right) + \mathsf{fma}\left(-\varepsilon, 1, \color{blue}{\varepsilon}\right)\right)} + x} \]

7. Simplified 99.5%

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

   [Start] 99.5	\[ \frac{\varepsilon}{\sqrt{x \cdot x + \left(\left(-\varepsilon\right) + \mathsf{fma}\left(-\varepsilon, 1, \varepsilon\right)\right)} + x} \]
   associate-+r+ [=>] 99.5	\[ \frac{\varepsilon}{\sqrt{\color{blue}{\left(x \cdot x + \left(-\varepsilon\right)\right) + \mathsf{fma}\left(-\varepsilon, 1, \varepsilon\right)}} + x} \]
   sub-neg [<=] 99.5	\[ \frac{\varepsilon}{\sqrt{\color{blue}{\left(x \cdot x - \varepsilon\right)} + \mathsf{fma}\left(-\varepsilon, 1, \varepsilon\right)} + x} \]
   +-commutative [=>] 99.5	\[ \frac{\varepsilon}{\sqrt{\color{blue}{\mathsf{fma}\left(-\varepsilon, 1, \varepsilon\right) + \left(x \cdot x - \varepsilon\right)}} + x} \]
   fma-udef [=>] 99.5	\[ \frac{\varepsilon}{\sqrt{\color{blue}{\left(\left(-\varepsilon\right) \cdot 1 + \varepsilon\right)} + \left(x \cdot x - \varepsilon\right)} + x} \]
   associate-+l+ [=>] 99.5	\[ \frac{\varepsilon}{\sqrt{\color{blue}{\left(-\varepsilon\right) \cdot 1 + \left(\varepsilon + \left(x \cdot x - \varepsilon\right)\right)}} + x} \]
   *-rgt-identity [=>] 99.5	\[ \frac{\varepsilon}{\sqrt{\color{blue}{\left(-\varepsilon\right)} + \left(\varepsilon + \left(x \cdot x - \varepsilon\right)\right)} + x} \]
   associate-+r- [=>] 99.5	\[ \frac{\varepsilon}{\sqrt{\left(-\varepsilon\right) + \color{blue}{\left(\left(\varepsilon + x \cdot x\right) - \varepsilon\right)}} + x} \]
   +-commutative [<=] 99.5	\[ \frac{\varepsilon}{\sqrt{\left(-\varepsilon\right) + \left(\color{blue}{\left(x \cdot x + \varepsilon\right)} - \varepsilon\right)} + x} \]
   fma-udef [<=] 99.5	\[ \frac{\varepsilon}{\sqrt{\left(-\varepsilon\right) + \left(\color{blue}{\mathsf{fma}\left(x, x, \varepsilon\right)} - \varepsilon\right)} + x} \]

8. Final simplification 99.5%

   \[\leadsto \frac{\varepsilon}{x + \sqrt{\left(\mathsf{fma}\left(x, x, \varepsilon\right) - \varepsilon\right) - \varepsilon}} \]

Alternatives

Alternative 1
Accuracy	99.0%
Cost	13764

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

Alternative 2
Accuracy	99.5%
Cost	6976

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

Alternative 3
Accuracy	87.3%
Cost	6788

\[\begin{array}{l} \mathbf{if}\;x \leq 5.5 \cdot 10^{-111}:\\ \;\;\;\;x - \sqrt{-\varepsilon}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon}{-0.5 \cdot \frac{\varepsilon}{x} + x \cdot 2}\\ \end{array} \]

Alternative 4
Accuracy	45.5%
Cost	704

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

Alternative 5
Accuracy	44.7%
Cost	320

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

Alternative 6
Accuracy	11.4%
Cost	192

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

Alternative 7
Accuracy	3.5%
Cost	64

\[x \]

Reproduce

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