(FPCore (x y z t a)
:precision binary64
(/ (* (* x y) z) (sqrt (- (* z z) (* t a)))))
↓
(FPCore (x y z t a)
:precision binary64
(let* ((t_1 (* x (* y (* z (pow (- (* z z) (* a t)) -0.5))))))
(if (<= z -7.107067327257021e+138)
(- (* -0.5 (* (/ y (/ z a)) (/ t (/ z x)))) (* y x))
(if (<= z -9.8e-175)
t_1
(if (<= z 1.12e-124)
(* y (* (* z x) (* (pow (- t) -0.5) (pow a -0.5))))
(if (<= z 2.3e+45) t_1 (* y x)))))))
double code(double x, double y, double z, double t, double a) {
double t_1 = x * (y * (z * pow(((z * z) - (a * t)), -0.5)));
double tmp;
if (z <= -7.107067327257021e+138) {
tmp = (-0.5 * ((y / (z / a)) * (t / (z / x)))) - (y * x);
} else if (z <= -9.8e-175) {
tmp = t_1;
} else if (z <= 1.12e-124) {
tmp = y * ((z * x) * (pow(-t, -0.5) * pow(a, -0.5)));
} else if (z <= 2.3e+45) {
tmp = t_1;
} else {
tmp = y * x;
}
return tmp;
}
real(8) function code(x, y, z, t, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: t
real(8), intent (in) :: a
code = ((x * y) * z) / sqrt(((z * z) - (t * a)))
end function
↓
real(8) function code(x, y, z, t, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: t
real(8), intent (in) :: a
real(8) :: t_1
real(8) :: tmp
t_1 = x * (y * (z * (((z * z) - (a * t)) ** (-0.5d0))))
if (z <= (-7.107067327257021d+138)) then
tmp = ((-0.5d0) * ((y / (z / a)) * (t / (z / x)))) - (y * x)
else if (z <= (-9.8d-175)) then
tmp = t_1
else if (z <= 1.12d-124) then
tmp = y * ((z * x) * ((-t ** (-0.5d0)) * (a ** (-0.5d0))))
else if (z <= 2.3d+45) then
tmp = t_1
else
tmp = y * x
end if
code = tmp
end function
public static double code(double x, double y, double z, double t, double a) {
return ((x * y) * z) / Math.sqrt(((z * z) - (t * a)));
}
↓
public static double code(double x, double y, double z, double t, double a) {
double t_1 = x * (y * (z * Math.pow(((z * z) - (a * t)), -0.5)));
double tmp;
if (z <= -7.107067327257021e+138) {
tmp = (-0.5 * ((y / (z / a)) * (t / (z / x)))) - (y * x);
} else if (z <= -9.8e-175) {
tmp = t_1;
} else if (z <= 1.12e-124) {
tmp = y * ((z * x) * (Math.pow(-t, -0.5) * Math.pow(a, -0.5)));
} else if (z <= 2.3e+45) {
tmp = t_1;
} else {
tmp = y * x;
}
return tmp;
}
\[\leadsto \color{blue}{y \cdot \left(\left(z \cdot x\right) \cdot \sqrt{\frac{1}{z \cdot z - a \cdot t}}\right)}
\]
Proof
(*.f64 y (*.f64 (*.f64 z x) (sqrt.f64 (/.f64 1 (-.f64 (*.f64 z z) (*.f64 a t)))))): 0 points increase in error, 0 points decrease in error
(*.f64 y (*.f64 (*.f64 z x) (sqrt.f64 (/.f64 1 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 z 2)) (*.f64 a t)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 y (*.f64 z x)) (sqrt.f64 (/.f64 1 (-.f64 (pow.f64 z 2) (*.f64 a t)))))): 44 points increase in error, 11 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (sqrt.f64 (/.f64 1 (-.f64 (pow.f64 z 2) (*.f64 a t)))) (*.f64 y (*.f64 z x)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 -1/2 (*.f64 (/.f64 y (/.f64 z a)) (/.f64 t (/.f64 z x)))) (*.f64 x y)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 -1/2 (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y a) z)) (/.f64 t (/.f64 z x)))) (*.f64 x y)): 17 points increase in error, 5 points decrease in error
(-.f64 (*.f64 -1/2 (*.f64 (/.f64 (*.f64 y a) z) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 t x) z)))) (*.f64 x y)): 13 points increase in error, 8 points decrease in error
(-.f64 (*.f64 -1/2 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (*.f64 y a) (*.f64 t x)) (*.f64 z z)))) (*.f64 x y)): 17 points increase in error, 8 points decrease in error
(-.f64 (*.f64 -1/2 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 y (*.f64 a (*.f64 t x)))) (*.f64 z z))) (*.f64 x y)): 8 points increase in error, 9 points decrease in error
(-.f64 (*.f64 -1/2 (/.f64 (*.f64 y (*.f64 a (*.f64 t x))) (Rewrite<= unpow2_binary64 (pow.f64 z 2)))) (*.f64 x y)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 -1/2 (/.f64 (*.f64 y (*.f64 a (*.f64 t x))) (pow.f64 z 2))) (Rewrite<= *-commutative_binary64 (*.f64 y x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1/2 (/.f64 (*.f64 y (*.f64 a (*.f64 t x))) (pow.f64 z 2))) (neg.f64 (*.f64 y x)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1/2 (/.f64 (*.f64 y (*.f64 a (*.f64 t x))) (pow.f64 z 2))) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 y x)))): 0 points increase in error, 0 points decrease in error
if -7.10706732725702149e138 < z < -9.79999999999999996e-175 or 1.12e-124 < z < 2.30000000000000012e45
Initial program 8.0
\[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}
\]
Simplified7.9
\[\leadsto \color{blue}{x \cdot \frac{y \cdot z}{\sqrt{z \cdot z - t \cdot a}}}
\]
Proof
(*.f64 x (/.f64 (*.f64 y z) (sqrt.f64 (-.f64 (*.f64 z z) (*.f64 t a))))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 x (*.f64 y z)) (sqrt.f64 (-.f64 (*.f64 z z) (*.f64 t a))))): 34 points increase in error, 10 points decrease in error
(/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x y) z)) (sqrt.f64 (-.f64 (*.f64 z z) (*.f64 t a)))): 16 points increase in error, 42 points decrease in error
Applied egg-rr4.8
\[\leadsto x \cdot \color{blue}{\left(y \cdot \left(z \cdot {\left(z \cdot z - t \cdot a\right)}^{-0.5}\right)\right)}
\]
if -9.79999999999999996e-175 < z < 1.12e-124
Initial program 16.9
\[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}
\]
Taylor expanded in x around 0 15.5
\[\leadsto \frac{\color{blue}{y \cdot \left(z \cdot x\right)}}{\sqrt{z \cdot z - t \cdot a}}
\]
Applied egg-rr15.1
\[\leadsto \color{blue}{y \cdot \left(\left(z \cdot x\right) \cdot {\left(z \cdot z - t \cdot a\right)}^{-0.5}\right)}
\]
herbie shell --seed 2022291
(FPCore (x y z t a)
:name "Statistics.Math.RootFinding:ridders from math-functions-0.1.5.2"
:precision binary64
:herbie-target
(if (< z -3.1921305903852764e+46) (- (* y x)) (if (< z 5.976268120920894e+90) (/ (* x z) (/ (sqrt (- (* z z) (* a t))) y)) (* y x)))
(/ (* (* x y) z) (sqrt (- (* z z) (* t a)))))