(FPCore (a k m)
:precision binary64
(/ (* a (pow k m)) (+ (+ 1.0 (* 10.0 k)) (* k k))))
↓
(FPCore (a k m)
:precision binary64
(if (<= k 1e+150)
(* a (expm1 (log1p (/ (pow k m) (fma k (+ k 10.0) 1.0)))))
(* (pow k m) (* (/ (pow (cbrt a) 2.0) k) (/ (cbrt a) k)))))
double code(double a, double k, double m) {
return (a * pow(k, m)) / ((1.0 + (10.0 * k)) + (k * k));
}
↓
double code(double a, double k, double m) {
double tmp;
if (k <= 1e+150) {
tmp = a * expm1(log1p((pow(k, m) / fma(k, (k + 10.0), 1.0))));
} else {
tmp = pow(k, m) * ((pow(cbrt(a), 2.0) / k) * (cbrt(a) / k));
}
return tmp;
}
function code(a, k, m)
return Float64(Float64(a * (k ^ m)) / Float64(Float64(1.0 + Float64(10.0 * k)) + Float64(k * k)))
end
↓
function code(a, k, m)
tmp = 0.0
if (k <= 1e+150)
tmp = Float64(a * expm1(log1p(Float64((k ^ m) / fma(k, Float64(k + 10.0), 1.0)))));
else
tmp = Float64((k ^ m) * Float64(Float64((cbrt(a) ^ 2.0) / k) * Float64(cbrt(a) / k)));
end
return tmp
end
\[\leadsto \color{blue}{a \cdot \frac{{k}^{m}}{\mathsf{fma}\left(k, k + 10, 1\right)}}
\]
Proof
(*.f64 a (/.f64 (pow.f64 k m) (fma.f64 k (+.f64 k 10) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 a (/.f64 (pow.f64 k m) (fma.f64 k (Rewrite<= +-commutative_binary64 (+.f64 10 k)) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 a (/.f64 (pow.f64 k m) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 k (+.f64 10 k)) 1)))): 0 points increase in error, 0 points decrease in error
(*.f64 a (/.f64 (pow.f64 k m) (+.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 10 k) (*.f64 k k))) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 a (/.f64 (pow.f64 k m) (Rewrite<= +-commutative_binary64 (+.f64 1 (+.f64 (*.f64 10 k) (*.f64 k k)))))): 0 points increase in error, 0 points decrease in error
(*.f64 a (/.f64 (pow.f64 k m) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 1 (*.f64 10 k)) (*.f64 k k))))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 a (pow.f64 k m)) (+.f64 (+.f64 1 (*.f64 10 k)) (*.f64 k k)))): 2 points increase in error, 3 points decrease in error
Applied egg-rr0.1
\[\leadsto a \cdot \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{{k}^{m}}{\mathsf{fma}\left(k, k + 10, 1\right)}\right)\right)}
\]
\[\leadsto \color{blue}{a \cdot \frac{{k}^{m}}{\mathsf{fma}\left(k, k + 10, 1\right)}}
\]
Proof
(*.f64 a (/.f64 (pow.f64 k m) (fma.f64 k (+.f64 k 10) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 a (/.f64 (pow.f64 k m) (fma.f64 k (Rewrite<= +-commutative_binary64 (+.f64 10 k)) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 a (/.f64 (pow.f64 k m) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 k (+.f64 10 k)) 1)))): 0 points increase in error, 0 points decrease in error
(*.f64 a (/.f64 (pow.f64 k m) (+.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 10 k) (*.f64 k k))) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 a (/.f64 (pow.f64 k m) (Rewrite<= +-commutative_binary64 (+.f64 1 (+.f64 (*.f64 10 k) (*.f64 k k)))))): 0 points increase in error, 0 points decrease in error
(*.f64 a (/.f64 (pow.f64 k m) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 1 (*.f64 10 k)) (*.f64 k k))))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 a (pow.f64 k m)) (+.f64 (+.f64 1 (*.f64 10 k)) (*.f64 k k)))): 2 points increase in error, 3 points decrease in error
(*.f64 (pow.f64 k m) (/.f64 a (*.f64 k k))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (Rewrite<= rem-exp-log_binary64 (exp.f64 (log.f64 k))) m) (/.f64 a (*.f64 k k))): 50 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (log.f64 k))))) m) (/.f64 a (*.f64 k k))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 (neg.f64 (Rewrite<= log-rec_binary64 (log.f64 (/.f64 1 k))))) m) (/.f64 a (*.f64 k k))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (exp.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (log.f64 (/.f64 1 k))))) m) (/.f64 a (*.f64 k k))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= exp-prod_binary64 (exp.f64 (*.f64 (*.f64 -1 (log.f64 (/.f64 1 k))) m))) (/.f64 a (*.f64 k k))): 0 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 (log.f64 (/.f64 1 k)) m)))) (/.f64 a (*.f64 k k))): 0 points increase in error, 0 points decrease in error
(*.f64 (exp.f64 (*.f64 -1 (*.f64 (log.f64 (/.f64 1 k)) m))) (/.f64 a (Rewrite<= unpow2_binary64 (pow.f64 k 2)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 a (pow.f64 k 2)) (exp.f64 (*.f64 -1 (*.f64 (log.f64 (/.f64 1 k)) m))))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 a (exp.f64 (*.f64 -1 (*.f64 (log.f64 (/.f64 1 k)) m)))) (pow.f64 k 2))): 1 points increase in error, 6 points decrease in error
herbie shell --seed 2022311
(FPCore (a k m)
:name "Falkner and Boettcher, Appendix A"
:precision binary64
(/ (* a (pow k m)) (+ (+ 1.0 (* 10.0 k)) (* k k))))