Average Error: 15.5 → 0.2
Time: 33.6s
Precision: binary64
Cost: 72968
\[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]
↓
\[\begin{array}{l} t_0 := \sqrt{\frac{0.5}{\mathsf{hypot}\left(-1, x\right)} + 0.5}\\ t_1 := \sqrt{0.5 + \frac{-0.5}{x}}\\ \mathbf{if}\;x \leq -1.08:\\ \;\;\;\;\frac{1}{\mathsf{fma}\left(1 + t_1, t_1, 1\right)} \cdot \left(1 - {t_1}^{3}\right)\\ \mathbf{elif}\;x \leq 0.0025:\\ \;\;\;\;\frac{1}{1 + \sqrt{0.5 + \left(0.5 + -0.25 \cdot \left(x \cdot x\right)\right)}} \cdot \left(\left(x \cdot x\right) \cdot \left(-0.1875 \cdot \left(x \cdot x\right) + 0.25\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1 - {t_0}^{6}}{\left(1 + t_0\right) \cdot \left(\left(1 + {t_0}^{4}\right) + {t_0}^{2}\right)}\\ \end{array} \]
(FPCore (x)
 :precision binary64
 (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))
↓
(FPCore (x)
 :precision binary64
 (let* ((t_0 (sqrt (+ (/ 0.5 (hypot -1.0 x)) 0.5)))
        (t_1 (sqrt (+ 0.5 (/ -0.5 x)))))
   (if (<= x -1.08)
     (* (/ 1.0 (fma (+ 1.0 t_1) t_1 1.0)) (- 1.0 (pow t_1 3.0)))
     (if (<= x 0.0025)
       (*
        (/ 1.0 (+ 1.0 (sqrt (+ 0.5 (+ 0.5 (* -0.25 (* x x)))))))
        (* (* x x) (+ (* -0.1875 (* x x)) 0.25)))
       (/
        (- 1.0 (pow t_0 6.0))
        (* (+ 1.0 t_0) (+ (+ 1.0 (pow t_0 4.0)) (pow t_0 2.0))))))))
double code(double x) {
	return 1.0 - sqrt((0.5 * (1.0 + (1.0 / hypot(1.0, x)))));
}
↓
double code(double x) {
	double t_0 = sqrt(((0.5 / hypot(-1.0, x)) + 0.5));
	double t_1 = sqrt((0.5 + (-0.5 / x)));
	double tmp;
	if (x <= -1.08) {
		tmp = (1.0 / fma((1.0 + t_1), t_1, 1.0)) * (1.0 - pow(t_1, 3.0));
	} else if (x <= 0.0025) {
		tmp = (1.0 / (1.0 + sqrt((0.5 + (0.5 + (-0.25 * (x * x))))))) * ((x * x) * ((-0.1875 * (x * x)) + 0.25));
	} else {
		tmp = (1.0 - pow(t_0, 6.0)) / ((1.0 + t_0) * ((1.0 + pow(t_0, 4.0)) + pow(t_0, 2.0)));
	}
	return tmp;
}

function code(x)
	return Float64(1.0 - sqrt(Float64(0.5 * Float64(1.0 + Float64(1.0 / hypot(1.0, x))))))
end
↓
function code(x)
	t_0 = sqrt(Float64(Float64(0.5 / hypot(-1.0, x)) + 0.5))
	t_1 = sqrt(Float64(0.5 + Float64(-0.5 / x)))
	tmp = 0.0
	if (x <= -1.08)
		tmp = Float64(Float64(1.0 / fma(Float64(1.0 + t_1), t_1, 1.0)) * Float64(1.0 - (t_1 ^ 3.0)));
	elseif (x <= 0.0025)
		tmp = Float64(Float64(1.0 / Float64(1.0 + sqrt(Float64(0.5 + Float64(0.5 + Float64(-0.25 * Float64(x * x))))))) * Float64(Float64(x * x) * Float64(Float64(-0.1875 * Float64(x * x)) + 0.25)));
	else
		tmp = Float64(Float64(1.0 - (t_0 ^ 6.0)) / Float64(Float64(1.0 + t_0) * Float64(Float64(1.0 + (t_0 ^ 4.0)) + (t_0 ^ 2.0))));
	end
	return tmp
end

code[x_] := N[(1.0 - N[Sqrt[N[(0.5 * N[(1.0 + N[(1.0 / N[Sqrt[1.0 ^ 2 + x ^ 2], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
↓
code[x_] := Block[{t$95$0 = N[Sqrt[N[(N[(0.5 / N[Sqrt[-1.0 ^ 2 + x ^ 2], $MachinePrecision]), $MachinePrecision] + 0.5), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$1 = N[Sqrt[N[(0.5 + N[(-0.5 / x), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[x, -1.08], N[(N[(1.0 / N[(N[(1.0 + t$95$1), $MachinePrecision] * t$95$1 + 1.0), $MachinePrecision]), $MachinePrecision] * N[(1.0 - N[Power[t$95$1, 3.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[x, 0.0025], N[(N[(1.0 / N[(1.0 + N[Sqrt[N[(0.5 + N[(0.5 + N[(-0.25 * N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(N[(x * x), $MachinePrecision] * N[(N[(-0.1875 * N[(x * x), $MachinePrecision]), $MachinePrecision] + 0.25), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(1.0 - N[Power[t$95$0, 6.0], $MachinePrecision]), $MachinePrecision] / N[(N[(1.0 + t$95$0), $MachinePrecision] * N[(N[(1.0 + N[Power[t$95$0, 4.0], $MachinePrecision]), $MachinePrecision] + N[Power[t$95$0, 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]]

1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
↓
\begin{array}{l}
t_0 := \sqrt{\frac{0.5}{\mathsf{hypot}\left(-1, x\right)} + 0.5}\\
t_1 := \sqrt{0.5 + \frac{-0.5}{x}}\\
\mathbf{if}\;x \leq -1.08:\\
\;\;\;\;\frac{1}{\mathsf{fma}\left(1 + t_1, t_1, 1\right)} \cdot \left(1 - {t_1}^{3}\right)\\

\mathbf{elif}\;x \leq 0.0025:\\
\;\;\;\;\frac{1}{1 + \sqrt{0.5 + \left(0.5 + -0.25 \cdot \left(x \cdot x\right)\right)}} \cdot \left(\left(x \cdot x\right) \cdot \left(-0.1875 \cdot \left(x \cdot x\right) + 0.25\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{1 - {t_0}^{6}}{\left(1 + t_0\right) \cdot \left(\left(1 + {t_0}^{4}\right) + {t_0}^{2}\right)}\\


\end{array}

Error

Derivation

  1. Split input into 3 regimes

  2. if x < -1.0800000000000001

    1. Initial program 1.0

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]

    2. Simplified1.0

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

    3. Taylor expanded in x around -inf 1.4

      \[\leadsto 1 - \sqrt{\color{blue}{0.5 - 0.5 \cdot \frac{1}{x}}} \]

    4. Simplified1.4

      \[\leadsto 1 - \sqrt{\color{blue}{0.5 - \frac{0.5}{x}}} \]
      Proof

    5. Applied egg-rr0.5

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

    if -1.0800000000000001 < x < 0.00250000000000000005

    1. Initial program 30.2

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]

    2. Simplified30.2

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

    3. Applied egg-rr30.2

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

    4. Taylor expanded in x around 0 0.1

      \[\leadsto \frac{1}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}} \cdot \color{blue}{\left(0.25 \cdot {x}^{2} + -0.1875 \cdot {x}^{4}\right)} \]

    5. Simplified0.1

      \[\leadsto \frac{1}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}} \cdot \color{blue}{\mathsf{fma}\left(0.25, x \cdot x, -0.1875 \cdot {x}^{4}\right)} \]
      Proof

    6. Applied egg-rr0.1

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

    7. Taylor expanded in x around 0 0.1

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

    8. Simplified0.1

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

    if 0.00250000000000000005 < x

    1. Initial program 1.1

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]

    2. Simplified1.1

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

    3. Applied egg-rr0.1

      \[\leadsto \color{blue}{\frac{\left(1 - {\left(\sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}\right)}^{6}\right) \cdot \frac{1}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}}}{\left(1 + {\left(\sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}\right)}^{4}\right) + {\left(\sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}\right)}^{2}}} \]

    4. Simplified0.1

      \[\leadsto \color{blue}{\frac{1 - {\left(\sqrt{\frac{0.5}{\mathsf{hypot}\left(-1, x\right)} + 0.5}\right)}^{6}}{\left(1 + \sqrt{\frac{0.5}{\mathsf{hypot}\left(-1, x\right)} + 0.5}\right) \cdot \left(\left(1 + {\left(\sqrt{\frac{0.5}{\mathsf{hypot}\left(-1, x\right)} + 0.5}\right)}^{4}\right) + {\left(\sqrt{\frac{0.5}{\mathsf{hypot}\left(-1, x\right)} + 0.5}\right)}^{2}\right)}} \]
      Proof
  3. Recombined 3 regimes into one program.

Alternatives

Alternative 1
Error0.1
Cost59524
\[\begin{array}{l} t_0 := \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}\\ \mathbf{if}\;\mathsf{hypot}\left(1, x\right) \leq 1.2:\\ \;\;\;\;\frac{1}{1 + \sqrt{0.5 + \left(0.5 + -0.25 \cdot \left(x \cdot x\right)\right)}} \cdot \left(\left(x \cdot x\right) \cdot \left(-0.1875 \cdot \left(x \cdot x\right) + 0.25\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\mathsf{fma}\left(1 + t_0, t_0, 1\right)} \cdot \left(1 - {t_0}^{3}\right)\\ \end{array} \]
Alternative 2
Error0.1
Cost46276
\[\begin{array}{l} t_0 := \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}\\ \mathbf{if}\;\mathsf{hypot}\left(1, x\right) \leq 1.2:\\ \;\;\;\;\frac{1}{1 + \sqrt{0.5 + \left(0.5 + -0.25 \cdot \left(x \cdot x\right)\right)}} \cdot \left(\left(x \cdot x\right) \cdot \left(-0.1875 \cdot \left(x \cdot x\right) + 0.25\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{1 + t_0} \cdot \left(1 - \sqrt[3]{{t_0}^{6}}\right)\\ \end{array} \]
Alternative 3
Error0.5
Cost33668
\[\begin{array}{l} t_0 := \sqrt{0.5 + \frac{-0.5}{x}}\\ \mathbf{if}\;x \leq -1.08:\\ \;\;\;\;\frac{1}{\mathsf{fma}\left(1 + t_0, t_0, 1\right)} \cdot \left(1 - {t_0}^{3}\right)\\ \mathbf{elif}\;x \leq 0.0025:\\ \;\;\;\;\frac{1}{1 + \sqrt{0.5 + \left(0.5 + -0.25 \cdot \left(x \cdot x\right)\right)}} \cdot \left(\left(x \cdot x\right) \cdot \left(-0.1875 \cdot \left(x \cdot x\right) + 0.25\right)\right)\\ \mathbf{else}:\\ \;\;\;\;{\left({\left(1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}\right)}^{0.3333333333333333}\right)}^{3}\\ \end{array} \]
Alternative 4
Error0.6
Cost32836
\[\begin{array}{l} \mathbf{if}\;\mathsf{hypot}\left(1, x\right) \leq 1.2:\\ \;\;\;\;\frac{1}{1 + \sqrt{0.5 + \left(0.5 + -0.25 \cdot \left(x \cdot x\right)\right)}} \cdot \left(\left(x \cdot x\right) \cdot \left(-0.1875 \cdot \left(x \cdot x\right) + 0.25\right)\right)\\ \mathbf{else}:\\ \;\;\;\;{\left({\left(1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}\right)}^{0.3333333333333333}\right)}^{3}\\ \end{array} \]
Alternative 5
Error0.7
Cost27268
\[\begin{array}{l} t_0 := \sqrt{0.5 + \frac{-0.5}{x}}\\ \mathbf{if}\;x \leq -1.08:\\ \;\;\;\;\frac{1 - {t_0}^{3}}{1 + t_0 \cdot \left(1 + t_0\right)}\\ \mathbf{elif}\;x \leq 0.0025:\\ \;\;\;\;\frac{1}{1 + \sqrt{0.5 + \left(0.5 + -0.25 \cdot \left(x \cdot x\right)\right)}} \cdot \left(\left(x \cdot x\right) \cdot \left(-0.1875 \cdot \left(x \cdot x\right) + 0.25\right)\right)\\ \mathbf{else}:\\ \;\;\;\;{\left({\left(1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}\right)}^{0.3333333333333333}\right)}^{3}\\ \end{array} \]
Alternative 6
Error0.6
Cost19908
\[\begin{array}{l} \mathbf{if}\;\mathsf{hypot}\left(1, x\right) \leq 1.2:\\ \;\;\;\;\frac{1}{1 + \sqrt{0.5 + \left(0.5 + -0.25 \cdot \left(x \cdot x\right)\right)}} \cdot \left(\left(x \cdot x\right) \cdot \left(-0.1875 \cdot \left(x \cdot x\right) + 0.25\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}\\ \end{array} \]
Alternative 7
Error0.7
Cost19908
\[\begin{array}{l} \mathbf{if}\;x \leq -1.08:\\ \;\;\;\;{\left({\left(1 - \sqrt{0.5 + \frac{-0.5}{x}}\right)}^{0.3333333333333333}\right)}^{3}\\ \mathbf{elif}\;x \leq 0.0025:\\ \;\;\;\;\frac{1}{1 + \sqrt{0.5 + \left(0.5 + -0.25 \cdot \left(x \cdot x\right)\right)}} \cdot \left(\left(x \cdot x\right) \cdot \left(-0.1875 \cdot \left(x \cdot x\right) + 0.25\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(-1, x\right)}}\\ \end{array} \]
Alternative 8
Error0.8
Cost8264
\[\begin{array}{l} \mathbf{if}\;x \leq -1.08:\\ \;\;\;\;1 - \sqrt{0.5 - \frac{0.5}{x}}\\ \mathbf{elif}\;x \leq 1.05:\\ \;\;\;\;\frac{1}{1 + \sqrt{0.5 + \left(0.5 + -0.25 \cdot \left(x \cdot x\right)\right)}} \cdot \left(\left(x \cdot x\right) \cdot \left(-0.1875 \cdot \left(x \cdot x\right) + 0.25\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0.5}{1 + \sqrt{0.5}}\\ \end{array} \]
Alternative 9
Error0.9
Cost7880
\[\begin{array}{l} \mathbf{if}\;x \leq -1.08:\\ \;\;\;\;1 - \sqrt{0.5 - \frac{0.5}{x}}\\ \mathbf{elif}\;x \leq 1.05:\\ \;\;\;\;\frac{1}{1 + \sqrt{0.5 + 0.5}} \cdot \left(\left(x \cdot x\right) \cdot \left(-0.1875 \cdot \left(x \cdot x\right) + 0.25\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0.5}{1 + \sqrt{0.5}}\\ \end{array} \]
Alternative 10
Error0.9
Cost6984
\[\begin{array}{l} t_0 := \frac{0.5}{1 + \sqrt{0.5}}\\ \mathbf{if}\;x \leq -1.55:\\ \;\;\;\;t_0\\ \mathbf{elif}\;x \leq 1.55:\\ \;\;\;\;0.125 \cdot \left(x \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]
Alternative 11
Error0.9
Cost6984
\[\begin{array}{l} \mathbf{if}\;x \leq -1.25:\\ \;\;\;\;1 - \sqrt{0.5 - \frac{0.5}{x}}\\ \mathbf{elif}\;x \leq 1.55:\\ \;\;\;\;0.125 \cdot \left(x \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0.5}{1 + \sqrt{0.5}}\\ \end{array} \]
Alternative 12
Error1.4
Cost6856
\[\begin{array}{l} t_0 := 1 - \sqrt{0.5}\\ \mathbf{if}\;x \leq -1.55:\\ \;\;\;\;t_0\\ \mathbf{elif}\;x \leq 1.55:\\ \;\;\;\;0.125 \cdot \left(x \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]
Alternative 13
Error31.6
Cost320
\[0.125 \cdot \left(x \cdot x\right) \]
Alternative 14
Error46.5
Cost192
\[1 - 1 \]

Error

Reproduce

herbie shell --seed 2023010 
(FPCore (x)
  :name "Given's Rotation SVD example, simplified"
  :precision binary64
  (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))