| Alternative 1 | |
|---|---|
| Accuracy | 99.9% |
| Cost | 40516 |

(FPCore (x) :precision binary64 (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))
(FPCore (x)
:precision binary64
(let* ((t_0 (+ 0.5 (/ 0.5 (hypot 1.0 x)))))
(if (<= (hypot 1.0 x) 1.0002)
(+ (* (pow x 4.0) -0.0859375) (* x (* x 0.125)))
(/ (- (/ 0.25 t_0) (/ (/ 0.25 (fma x x 1.0)) t_0)) (+ 1.0 (sqrt t_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 = 0.5 + (0.5 / hypot(1.0, x));
double tmp;
if (hypot(1.0, x) <= 1.0002) {
tmp = (pow(x, 4.0) * -0.0859375) + (x * (x * 0.125));
} else {
tmp = ((0.25 / t_0) - ((0.25 / fma(x, x, 1.0)) / t_0)) / (1.0 + sqrt(t_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 = Float64(0.5 + Float64(0.5 / hypot(1.0, x))) tmp = 0.0 if (hypot(1.0, x) <= 1.0002) tmp = Float64(Float64((x ^ 4.0) * -0.0859375) + Float64(x * Float64(x * 0.125))); else tmp = Float64(Float64(Float64(0.25 / t_0) - Float64(Float64(0.25 / fma(x, x, 1.0)) / t_0)) / Float64(1.0 + sqrt(t_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[(0.5 + N[(0.5 / N[Sqrt[1.0 ^ 2 + x ^ 2], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[Sqrt[1.0 ^ 2 + x ^ 2], $MachinePrecision], 1.0002], N[(N[(N[Power[x, 4.0], $MachinePrecision] * -0.0859375), $MachinePrecision] + N[(x * N[(x * 0.125), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(N[(0.25 / t$95$0), $MachinePrecision] - N[(N[(0.25 / N[(x * x + 1.0), $MachinePrecision]), $MachinePrecision] / t$95$0), $MachinePrecision]), $MachinePrecision] / N[(1.0 + N[Sqrt[t$95$0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
\begin{array}{l}
t_0 := 0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}\\
\mathbf{if}\;\mathsf{hypot}\left(1, x\right) \leq 1.0002:\\
\;\;\;\;{x}^{4} \cdot -0.0859375 + x \cdot \left(x \cdot 0.125\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{\frac{0.25}{t_0} - \frac{\frac{0.25}{\mathsf{fma}\left(x, x, 1\right)}}{t_0}}{1 + \sqrt{t_0}}\\
\end{array}
Herbie found 13 alternatives:
| Alternative | Accuracy | Speedup |
|---|
if (hypot.f64 1 x) < 1.0002Initial program 48.0%
Simplified48.0%
[Start]48.0% | \[ 1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
\] |
|---|---|
distribute-lft-in [=>]48.0% | \[ 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}}
\] |
metadata-eval [=>]48.0% | \[ 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}
\] |
associate-*r/ [=>]48.0% | \[ 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}}
\] |
metadata-eval [=>]48.0% | \[ 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}}
\] |
Applied egg-rr48.1%
[Start]48.0% | \[ 1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}
\] |
|---|---|
flip-- [=>]48.0% | \[ \color{blue}{\frac{1 \cdot 1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}} \cdot \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}}
\] |
metadata-eval [=>]48.0% | \[ \frac{\color{blue}{1} - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}} \cdot \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
add-sqr-sqrt [<=]48.1% | \[ \frac{1 - \color{blue}{\left(0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}\right)}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
associate--r+ [=>]48.1% | \[ \frac{\color{blue}{\left(1 - 0.5\right) - \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
metadata-eval [=>]48.1% | \[ \frac{\color{blue}{0.5} - \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
Taylor expanded in x around 0 100.0%
Simplified100.0%
[Start]100.0% | \[ 0.125 \cdot {x}^{2} + -0.0859375 \cdot {x}^{4}
\] |
|---|---|
+-commutative [=>]100.0% | \[ \color{blue}{-0.0859375 \cdot {x}^{4} + 0.125 \cdot {x}^{2}}
\] |
*-commutative [=>]100.0% | \[ \color{blue}{{x}^{4} \cdot -0.0859375} + 0.125 \cdot {x}^{2}
\] |
fma-def [=>]100.0% | \[ \color{blue}{\mathsf{fma}\left({x}^{4}, -0.0859375, 0.125 \cdot {x}^{2}\right)}
\] |
*-commutative [=>]100.0% | \[ \mathsf{fma}\left({x}^{4}, -0.0859375, \color{blue}{{x}^{2} \cdot 0.125}\right)
\] |
unpow2 [=>]100.0% | \[ \mathsf{fma}\left({x}^{4}, -0.0859375, \color{blue}{\left(x \cdot x\right)} \cdot 0.125\right)
\] |
Applied egg-rr100.0%
[Start]100.0% | \[ \mathsf{fma}\left({x}^{4}, -0.0859375, \left(x \cdot x\right) \cdot 0.125\right)
\] |
|---|---|
fma-udef [=>]100.0% | \[ \color{blue}{{x}^{4} \cdot -0.0859375 + \left(x \cdot x\right) \cdot 0.125}
\] |
associate-*l* [=>]100.0% | \[ {x}^{4} \cdot -0.0859375 + \color{blue}{x \cdot \left(x \cdot 0.125\right)}
\] |
if 1.0002 < (hypot.f64 1 x) Initial program 98.3%
Simplified98.3%
[Start]98.3% | \[ 1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
\] |
|---|---|
distribute-lft-in [=>]98.3% | \[ 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}}
\] |
metadata-eval [=>]98.3% | \[ 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}
\] |
associate-*r/ [=>]98.3% | \[ 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}}
\] |
metadata-eval [=>]98.3% | \[ 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}}
\] |
Applied egg-rr99.9%
[Start]98.3% | \[ 1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}
\] |
|---|---|
flip-- [=>]98.4% | \[ \color{blue}{\frac{1 \cdot 1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}} \cdot \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}}
\] |
metadata-eval [=>]98.4% | \[ \frac{\color{blue}{1} - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}} \cdot \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
add-sqr-sqrt [<=]99.8% | \[ \frac{1 - \color{blue}{\left(0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}\right)}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
associate--r+ [=>]99.9% | \[ \frac{\color{blue}{\left(1 - 0.5\right) - \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
metadata-eval [=>]99.9% | \[ \frac{\color{blue}{0.5} - \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
Applied egg-rr99.9%
[Start]99.9% | \[ \frac{0.5 - \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
|---|---|
flip-- [=>]99.8% | \[ \frac{\color{blue}{\frac{0.5 \cdot 0.5 - \frac{0.5}{\mathsf{hypot}\left(1, x\right)} \cdot \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
div-inv [=>]99.8% | \[ \frac{\color{blue}{\left(0.5 \cdot 0.5 - \frac{0.5}{\mathsf{hypot}\left(1, x\right)} \cdot \frac{0.5}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \frac{1}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
metadata-eval [=>]99.8% | \[ \frac{\left(\color{blue}{0.25} - \frac{0.5}{\mathsf{hypot}\left(1, x\right)} \cdot \frac{0.5}{\mathsf{hypot}\left(1, x\right)}\right) \cdot \frac{1}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
frac-times [=>]99.9% | \[ \frac{\left(0.25 - \color{blue}{\frac{0.5 \cdot 0.5}{\mathsf{hypot}\left(1, x\right) \cdot \mathsf{hypot}\left(1, x\right)}}\right) \cdot \frac{1}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
metadata-eval [=>]99.9% | \[ \frac{\left(0.25 - \frac{\color{blue}{0.25}}{\mathsf{hypot}\left(1, x\right) \cdot \mathsf{hypot}\left(1, x\right)}\right) \cdot \frac{1}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
hypot-udef [=>]99.9% | \[ \frac{\left(0.25 - \frac{0.25}{\color{blue}{\sqrt{1 \cdot 1 + x \cdot x}} \cdot \mathsf{hypot}\left(1, x\right)}\right) \cdot \frac{1}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
hypot-udef [=>]99.9% | \[ \frac{\left(0.25 - \frac{0.25}{\sqrt{1 \cdot 1 + x \cdot x} \cdot \color{blue}{\sqrt{1 \cdot 1 + x \cdot x}}}\right) \cdot \frac{1}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
add-sqr-sqrt [<=]99.9% | \[ \frac{\left(0.25 - \frac{0.25}{\color{blue}{1 \cdot 1 + x \cdot x}}\right) \cdot \frac{1}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
metadata-eval [=>]99.9% | \[ \frac{\left(0.25 - \frac{0.25}{\color{blue}{1} + x \cdot x}\right) \cdot \frac{1}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
Simplified99.9%
[Start]99.9% | \[ \frac{\left(0.25 - \frac{0.25}{1 + x \cdot x}\right) \cdot \frac{1}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
|---|---|
associate-*r/ [=>]99.9% | \[ \frac{\color{blue}{\frac{\left(0.25 - \frac{0.25}{1 + x \cdot x}\right) \cdot 1}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
*-rgt-identity [=>]99.9% | \[ \frac{\frac{\color{blue}{0.25 - \frac{0.25}{1 + x \cdot x}}}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
/-rgt-identity [<=]99.9% | \[ \frac{\frac{\color{blue}{\frac{0.25 - \frac{0.25}{1 + x \cdot x}}{1}}}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
/-rgt-identity [=>]99.9% | \[ \frac{\frac{\color{blue}{0.25 - \frac{0.25}{1 + x \cdot x}}}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
unpow2 [<=]99.9% | \[ \frac{\frac{0.25 - \frac{0.25}{1 + \color{blue}{{x}^{2}}}}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
+-commutative [=>]99.9% | \[ \frac{\frac{0.25 - \frac{0.25}{\color{blue}{{x}^{2} + 1}}}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
unpow2 [=>]99.9% | \[ \frac{\frac{0.25 - \frac{0.25}{\color{blue}{x \cdot x} + 1}}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
Applied egg-rr99.9%
[Start]99.9% | \[ \frac{\frac{0.25 - \frac{0.25}{x \cdot x + 1}}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
|---|---|
div-sub [=>]99.9% | \[ \frac{\color{blue}{\frac{0.25}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}} - \frac{\frac{0.25}{x \cdot x + 1}}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
fma-def [=>]99.9% | \[ \frac{\frac{0.25}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}} - \frac{\frac{0.25}{\color{blue}{\mathsf{fma}\left(x, x, 1\right)}}}{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}
\] |
Final simplification100.0%
| Alternative 1 | |
|---|---|
| Accuracy | 99.9% |
| Cost | 40516 |
| Alternative 2 | |
|---|---|
| Accuracy | 99.9% |
| Cost | 40132 |
| Alternative 3 | |
|---|---|
| Accuracy | 99.9% |
| Cost | 26756 |
| Alternative 4 | |
|---|---|
| Accuracy | 99.1% |
| Cost | 13956 |
| Alternative 5 | |
|---|---|
| Accuracy | 99.1% |
| Cost | 13828 |
| Alternative 6 | |
|---|---|
| Accuracy | 98.7% |
| Cost | 13636 |
| Alternative 7 | |
|---|---|
| Accuracy | 98.5% |
| Cost | 13316 |
| Alternative 8 | |
|---|---|
| Accuracy | 97.7% |
| Cost | 6857 |
| Alternative 9 | |
|---|---|
| Accuracy | 60.8% |
| Cost | 712 |
| Alternative 10 | |
|---|---|
| Accuracy | 60.8% |
| Cost | 712 |
| Alternative 11 | |
|---|---|
| Accuracy | 60.8% |
| Cost | 584 |
| Alternative 12 | |
|---|---|
| Accuracy | 37.7% |
| Cost | 328 |
| Alternative 13 | |
|---|---|
| Accuracy | 27.4% |
| Cost | 64 |
herbie shell --seed 2023165
(FPCore (x)
:name "Given's Rotation SVD example, simplified"
:precision binary64
(- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))