| Alternative 1 | |
|---|---|
| Accuracy | 100.0% |
| Cost | 8320 |

(FPCore (t)
:precision binary64
(-
1.0
(/
1.0
(+
2.0
(*
(- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))))
(- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))))))))(FPCore (t)
:precision binary64
(+
1.0
(/
-1.0
(+
2.0
(/
(+ 2.0 (/ -2.0 (+ 1.0 t)))
(/ (+ 2.0 (/ 2.0 (+ 1.0 t))) (+ 4.0 (* -4.0 (pow (+ 1.0 t) -2.0)))))))))double code(double t) {
return 1.0 - (1.0 / (2.0 + ((2.0 - ((2.0 / t) / (1.0 + (1.0 / t)))) * (2.0 - ((2.0 / t) / (1.0 + (1.0 / t)))))));
}
double code(double t) {
return 1.0 + (-1.0 / (2.0 + ((2.0 + (-2.0 / (1.0 + t))) / ((2.0 + (2.0 / (1.0 + t))) / (4.0 + (-4.0 * pow((1.0 + t), -2.0)))))));
}
real(8) function code(t)
real(8), intent (in) :: t
code = 1.0d0 - (1.0d0 / (2.0d0 + ((2.0d0 - ((2.0d0 / t) / (1.0d0 + (1.0d0 / t)))) * (2.0d0 - ((2.0d0 / t) / (1.0d0 + (1.0d0 / t)))))))
end function
real(8) function code(t)
real(8), intent (in) :: t
code = 1.0d0 + ((-1.0d0) / (2.0d0 + ((2.0d0 + ((-2.0d0) / (1.0d0 + t))) / ((2.0d0 + (2.0d0 / (1.0d0 + t))) / (4.0d0 + ((-4.0d0) * ((1.0d0 + t) ** (-2.0d0))))))))
end function
public static double code(double t) {
return 1.0 - (1.0 / (2.0 + ((2.0 - ((2.0 / t) / (1.0 + (1.0 / t)))) * (2.0 - ((2.0 / t) / (1.0 + (1.0 / t)))))));
}
public static double code(double t) {
return 1.0 + (-1.0 / (2.0 + ((2.0 + (-2.0 / (1.0 + t))) / ((2.0 + (2.0 / (1.0 + t))) / (4.0 + (-4.0 * Math.pow((1.0 + t), -2.0)))))));
}
def code(t): return 1.0 - (1.0 / (2.0 + ((2.0 - ((2.0 / t) / (1.0 + (1.0 / t)))) * (2.0 - ((2.0 / t) / (1.0 + (1.0 / t)))))))
def code(t): return 1.0 + (-1.0 / (2.0 + ((2.0 + (-2.0 / (1.0 + t))) / ((2.0 + (2.0 / (1.0 + t))) / (4.0 + (-4.0 * math.pow((1.0 + t), -2.0)))))))
function code(t) return Float64(1.0 - Float64(1.0 / Float64(2.0 + Float64(Float64(2.0 - Float64(Float64(2.0 / t) / Float64(1.0 + Float64(1.0 / t)))) * Float64(2.0 - Float64(Float64(2.0 / t) / Float64(1.0 + Float64(1.0 / t)))))))) end
function code(t) return Float64(1.0 + Float64(-1.0 / Float64(2.0 + Float64(Float64(2.0 + Float64(-2.0 / Float64(1.0 + t))) / Float64(Float64(2.0 + Float64(2.0 / Float64(1.0 + t))) / Float64(4.0 + Float64(-4.0 * (Float64(1.0 + t) ^ -2.0)))))))) end
function tmp = code(t) tmp = 1.0 - (1.0 / (2.0 + ((2.0 - ((2.0 / t) / (1.0 + (1.0 / t)))) * (2.0 - ((2.0 / t) / (1.0 + (1.0 / t))))))); end
function tmp = code(t) tmp = 1.0 + (-1.0 / (2.0 + ((2.0 + (-2.0 / (1.0 + t))) / ((2.0 + (2.0 / (1.0 + t))) / (4.0 + (-4.0 * ((1.0 + t) ^ -2.0))))))); end
code[t_] := N[(1.0 - N[(1.0 / N[(2.0 + N[(N[(2.0 - N[(N[(2.0 / t), $MachinePrecision] / N[(1.0 + N[(1.0 / t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(2.0 - N[(N[(2.0 / t), $MachinePrecision] / N[(1.0 + N[(1.0 / t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
code[t_] := N[(1.0 + N[(-1.0 / N[(2.0 + N[(N[(2.0 + N[(-2.0 / N[(1.0 + t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[(2.0 + N[(2.0 / N[(1.0 + t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(4.0 + N[(-4.0 * N[Power[N[(1.0 + t), $MachinePrecision], -2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}
1 + \frac{-1}{2 + \frac{2 + \frac{-2}{1 + t}}{\frac{2 + \frac{2}{1 + t}}{4 + -4 \cdot {\left(1 + t\right)}^{-2}}}}
Herbie found 10 alternatives:
| Alternative | Accuracy | Speedup |
|---|
Results
Initial program 100.0%
Applied egg-rr100.0%
[Start]100.0% | \[ 1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}
\] |
|---|---|
flip-- [=>]100.0% | \[ 1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \color{blue}{\frac{2 \cdot 2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}} \cdot \frac{\frac{2}{t}}{1 + \frac{1}{t}}}{2 + \frac{\frac{2}{t}}{1 + \frac{1}{t}}}}}
\] |
associate-*r/ [=>]100.0% | \[ 1 - \frac{1}{2 + \color{blue}{\frac{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 \cdot 2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}} \cdot \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \frac{\frac{2}{t}}{1 + \frac{1}{t}}}}}
\] |
metadata-eval [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(\color{blue}{4} - \frac{\frac{2}{t}}{1 + \frac{1}{t}} \cdot \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \frac{\frac{2}{t}}{1 + \frac{1}{t}}}}
\] |
pow2 [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(4 - \color{blue}{{\left(\frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}^{2}}\right)}{2 + \frac{\frac{2}{t}}{1 + \frac{1}{t}}}}
\] |
Simplified100.0%
[Start]100.0% | \[ 1 - \frac{1}{2 + \frac{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(4 - {\left(\frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}^{2}\right)}{2 + \frac{\frac{2}{t}}{1 + \frac{1}{t}}}}
\] |
|---|---|
associate-/l* [=>]100.0% | \[ 1 - \frac{1}{2 + \color{blue}{\frac{2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}}{\frac{2 + \frac{\frac{2}{t}}{1 + \frac{1}{t}}}{4 - {\left(\frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}^{2}}}}}
\] |
associate-/r* [<=]100.0% | \[ 1 - \frac{1}{2 + \frac{2 - \color{blue}{\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}}{\frac{2 + \frac{\frac{2}{t}}{1 + \frac{1}{t}}}{4 - {\left(\frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}^{2}}}}
\] |
associate-/r* [<=]100.0% | \[ 1 - \frac{1}{2 + \frac{2 - \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{\frac{2 + \color{blue}{\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}}{4 - {\left(\frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}^{2}}}}
\] |
associate-/r* [<=]100.0% | \[ 1 - \frac{1}{2 + \frac{2 - \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{\frac{2 + \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{4 - {\color{blue}{\left(\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}}^{2}}}}
\] |
Applied egg-rr100.0%
[Start]100.0% | \[ 1 - \frac{1}{2 + \frac{2 - \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{\frac{2 + \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{4 - {\left(\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}^{2}}}}
\] |
|---|---|
*-un-lft-identity [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{\color{blue}{1 \cdot \left(2 - \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}}{\frac{2 + \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{4 - {\left(\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}^{2}}}}
\] |
div-inv [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{1 \cdot \left(2 - \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}{\color{blue}{\left(2 + \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right) \cdot \frac{1}{4 - {\left(\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}^{2}}}}}
\] |
times-frac [=>]100.0% | \[ 1 - \frac{1}{2 + \color{blue}{\frac{1}{2 + \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}} \cdot \frac{2 - \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{\frac{1}{4 - {\left(\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}^{2}}}}}
\] |
distribute-rgt-in [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{1}{2 + \frac{2}{\color{blue}{1 \cdot t + \frac{1}{t} \cdot t}}} \cdot \frac{2 - \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{\frac{1}{4 - {\left(\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}^{2}}}}
\] |
*-un-lft-identity [<=]100.0% | \[ 1 - \frac{1}{2 + \frac{1}{2 + \frac{2}{\color{blue}{t} + \frac{1}{t} \cdot t}} \cdot \frac{2 - \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{\frac{1}{4 - {\left(\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}^{2}}}}
\] |
inv-pow [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{1}{2 + \frac{2}{t + \color{blue}{{t}^{-1}} \cdot t}} \cdot \frac{2 - \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{\frac{1}{4 - {\left(\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}^{2}}}}
\] |
pow-plus [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{1}{2 + \frac{2}{t + \color{blue}{{t}^{\left(-1 + 1\right)}}}} \cdot \frac{2 - \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{\frac{1}{4 - {\left(\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}^{2}}}}
\] |
metadata-eval [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{1}{2 + \frac{2}{t + {t}^{\color{blue}{0}}}} \cdot \frac{2 - \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{\frac{1}{4 - {\left(\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}^{2}}}}
\] |
metadata-eval [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{1}{2 + \frac{2}{t + \color{blue}{1}}} \cdot \frac{2 - \frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}}{\frac{1}{4 - {\left(\frac{2}{t \cdot \left(1 + \frac{1}{t}\right)}\right)}^{2}}}}
\] |
Applied egg-rr100.0%
[Start]100.0% | \[ 1 - \frac{1}{2 + \frac{1}{2 + \frac{2}{t + 1}} \cdot \frac{2 - \frac{2}{t + 1}}{\frac{1}{4 - \frac{4}{{\left(t + 1\right)}^{2}}}}}
\] |
|---|---|
expm1-log1p-u [=>]100.0% | \[ 1 - \frac{1}{2 + \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1}{2 + \frac{2}{t + 1}} \cdot \frac{2 - \frac{2}{t + 1}}{\frac{1}{4 - \frac{4}{{\left(t + 1\right)}^{2}}}}\right)\right)}}
\] |
expm1-udef [=>]100.0% | \[ 1 - \frac{1}{2 + \color{blue}{\left(e^{\mathsf{log1p}\left(\frac{1}{2 + \frac{2}{t + 1}} \cdot \frac{2 - \frac{2}{t + 1}}{\frac{1}{4 - \frac{4}{{\left(t + 1\right)}^{2}}}}\right)} - 1\right)}}
\] |
Simplified100.0%
[Start]100.0% | \[ 1 - \frac{1}{2 + \left(e^{\mathsf{log1p}\left(\frac{\left(2 - \frac{2}{t + 1}\right) \cdot \left(4 - 4 \cdot {\left(t + 1\right)}^{-2}\right)}{2 + \frac{2}{t + 1}}\right)} - 1\right)}
\] |
|---|---|
expm1-def [=>]100.0% | \[ 1 - \frac{1}{2 + \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\left(2 - \frac{2}{t + 1}\right) \cdot \left(4 - 4 \cdot {\left(t + 1\right)}^{-2}\right)}{2 + \frac{2}{t + 1}}\right)\right)}}
\] |
expm1-log1p [=>]100.0% | \[ 1 - \frac{1}{2 + \color{blue}{\frac{\left(2 - \frac{2}{t + 1}\right) \cdot \left(4 - 4 \cdot {\left(t + 1\right)}^{-2}\right)}{2 + \frac{2}{t + 1}}}}
\] |
associate-/l* [=>]100.0% | \[ 1 - \frac{1}{2 + \color{blue}{\frac{2 - \frac{2}{t + 1}}{\frac{2 + \frac{2}{t + 1}}{4 - 4 \cdot {\left(t + 1\right)}^{-2}}}}}
\] |
/-rgt-identity [<=]100.0% | \[ 1 - \frac{1}{2 + \frac{\color{blue}{\frac{2 - \frac{2}{t + 1}}{1}}}{\frac{2 + \frac{2}{t + 1}}{4 - 4 \cdot {\left(t + 1\right)}^{-2}}}}
\] |
/-rgt-identity [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{\color{blue}{2 - \frac{2}{t + 1}}}{\frac{2 + \frac{2}{t + 1}}{4 - 4 \cdot {\left(t + 1\right)}^{-2}}}}
\] |
sub-neg [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{\color{blue}{2 + \left(-\frac{2}{t + 1}\right)}}{\frac{2 + \frac{2}{t + 1}}{4 - 4 \cdot {\left(t + 1\right)}^{-2}}}}
\] |
distribute-neg-frac [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{2 + \color{blue}{\frac{-2}{t + 1}}}{\frac{2 + \frac{2}{t + 1}}{4 - 4 \cdot {\left(t + 1\right)}^{-2}}}}
\] |
metadata-eval [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{2 + \frac{\color{blue}{-2}}{t + 1}}{\frac{2 + \frac{2}{t + 1}}{4 - 4 \cdot {\left(t + 1\right)}^{-2}}}}
\] |
cancel-sign-sub-inv [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{2 + \frac{-2}{t + 1}}{\frac{2 + \frac{2}{t + 1}}{\color{blue}{4 + \left(-4\right) \cdot {\left(t + 1\right)}^{-2}}}}}
\] |
metadata-eval [=>]100.0% | \[ 1 - \frac{1}{2 + \frac{2 + \frac{-2}{t + 1}}{\frac{2 + \frac{2}{t + 1}}{4 + \color{blue}{-4} \cdot {\left(t + 1\right)}^{-2}}}}
\] |
Final simplification100.0%
| Alternative 1 | |
|---|---|
| Accuracy | 100.0% |
| Cost | 8320 |
| Alternative 2 | |
|---|---|
| Accuracy | 100.0% |
| Cost | 1856 |
| Alternative 3 | |
|---|---|
| Accuracy | 100.0% |
| Cost | 1216 |
| Alternative 4 | |
|---|---|
| Accuracy | 100.0% |
| Cost | 1088 |
| Alternative 5 | |
|---|---|
| Accuracy | 96.8% |
| Cost | 836 |
| Alternative 6 | |
|---|---|
| Accuracy | 97.1% |
| Cost | 836 |
| Alternative 7 | |
|---|---|
| Accuracy | 96.1% |
| Cost | 452 |
| Alternative 8 | |
|---|---|
| Accuracy | 96.7% |
| Cost | 452 |
| Alternative 9 | |
|---|---|
| Accuracy | 96.0% |
| Cost | 196 |
| Alternative 10 | |
|---|---|
| Accuracy | 94.9% |
| Cost | 64 |
herbie shell --seed 2023277
(FPCore (t)
:name "Kahan p13 Example 3"
:precision binary64
(- 1.0 (/ 1.0 (+ 2.0 (* (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))) (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))))))))