\[\begin{array}{l}
\mathbf{if}\;k \leq 20000000000000:\\
\;\;\;\;\frac{a \cdot {k}^{m}}{\left(1 + k \cdot 10\right) + k \cdot k}\\
\mathbf{else}:\\
\;\;\;\;\frac{{k}^{m}}{\frac{k}{\frac{a}{k}}}\\
\end{array}
\]
(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 20000000000000.0)
(/ (* a (pow k m)) (+ (+ 1.0 (* k 10.0)) (* k k)))
(/ (pow k m) (/ k (/ 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 <= 20000000000000.0) {
tmp = (a * pow(k, m)) / ((1.0 + (k * 10.0)) + (k * k));
} else {
tmp = pow(k, m) / (k / (a / k));
}
return tmp;
}
real(8) function code(a, k, m)
real(8), intent (in) :: a
real(8), intent (in) :: k
real(8), intent (in) :: m
code = (a * (k ** m)) / ((1.0d0 + (10.0d0 * k)) + (k * k))
end function
↓
real(8) function code(a, k, m)
real(8), intent (in) :: a
real(8), intent (in) :: k
real(8), intent (in) :: m
real(8) :: tmp
if (k <= 20000000000000.0d0) then
tmp = (a * (k ** m)) / ((1.0d0 + (k * 10.0d0)) + (k * k))
else
tmp = (k ** m) / (k / (a / k))
end if
code = tmp
end function
public static double code(double a, double k, double m) {
return (a * Math.pow(k, m)) / ((1.0 + (10.0 * k)) + (k * k));
}
↓
public static double code(double a, double k, double m) {
double tmp;
if (k <= 20000000000000.0) {
tmp = (a * Math.pow(k, m)) / ((1.0 + (k * 10.0)) + (k * k));
} else {
tmp = Math.pow(k, m) / (k / (a / k));
}
return tmp;
}
\[\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)))): 1 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))): 27 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, 3 points decrease in error
herbie shell --seed 2022300
(FPCore (a k m)
:name "Falkner and Boettcher, Appendix A"
:precision binary64
(/ (* a (pow k m)) (+ (+ 1.0 (* 10.0 k)) (* k k))))