Data.Number.Erf:$cinvnormcdf from erf-2.0.0.0, A

Average Error: 0.3 → 0.5

Time: 8.7s

Precision: 64

Math

\[\left(\left(x \cdot 0.5 - y\right) \cdot \sqrt{z \cdot 2}\right) \cdot e^{\frac{t \cdot t}{2}}\]

↓

\[\left(x \cdot 0.5 - y\right) \cdot \left(\left({z}^{\frac{1}{2}} \cdot \sqrt{2}\right) \cdot \left(\left(\sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}} \cdot \sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}}\right) \cdot \sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}}\right)\right)\]

C

double code(double x, double y, double z, double t) {
	return ((((x * 0.5) - y) * sqrt((z * 2.0))) * exp(((t * t) / 2.0)));
}

↓

double code(double x, double y, double z, double t) {
	return (((x * 0.5) - y) * ((pow(z, 0.5) * sqrt(2.0)) * ((cbrt(pow(exp(t), (t / 2.0))) * cbrt(pow(exp(t), (t / 2.0)))) * cbrt(pow(exp(t), (t / 2.0))))));
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	0.3
Target	0.3
Herbie	0.5

\[\left(\left(x \cdot 0.5 - y\right) \cdot \sqrt{z \cdot 2}\right) \cdot {\left(e^{1}\right)}^{\left(\frac{t \cdot t}{2}\right)}\]

Derivation

1. Initial program 0.3

   \[\left(\left(x \cdot 0.5 - y\right) \cdot \sqrt{z \cdot 2}\right) \cdot e^{\frac{t \cdot t}{2}}\]
2. Using strategy rm

3. Applied associate-*l* 0.3

   \[\leadsto \color{blue}{\left(x \cdot 0.5 - y\right) \cdot \left(\sqrt{z \cdot 2} \cdot e^{\frac{t \cdot t}{2}}\right)}\]
4. Using strategy rm

5. Applied *-un-lft-identity 0.3

   \[\leadsto \left(x \cdot 0.5 - y\right) \cdot \left(\sqrt{z \cdot 2} \cdot e^{\frac{t \cdot t}{\color{blue}{1 \cdot 2}}}\right)\]

6. Applied times-frac 0.3

   \[\leadsto \left(x \cdot 0.5 - y\right) \cdot \left(\sqrt{z \cdot 2} \cdot e^{\color{blue}{\frac{t}{1} \cdot \frac{t}{2}}}\right)\]

7. Applied exp-prod 0.3

   \[\leadsto \left(x \cdot 0.5 - y\right) \cdot \left(\sqrt{z \cdot 2} \cdot \color{blue}{{\left(e^{\frac{t}{1}}\right)}^{\left(\frac{t}{2}\right)}}\right)\]

8. Simplified 0.3

   \[\leadsto \left(x \cdot 0.5 - y\right) \cdot \left(\sqrt{z \cdot 2} \cdot {\color{blue}{\left(e^{t}\right)}}^{\left(\frac{t}{2}\right)}\right)\]
9. Using strategy rm

10. Applied add-cube-cbrt 0.3

    \[\leadsto \left(x \cdot 0.5 - y\right) \cdot \left(\sqrt{z \cdot 2} \cdot \color{blue}{\left(\left(\sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}} \cdot \sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}}\right) \cdot \sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}}\right)}\right)\]
11. Using strategy rm

12. Applied sqrt-prod 0.5

    \[\leadsto \left(x \cdot 0.5 - y\right) \cdot \left(\color{blue}{\left(\sqrt{z} \cdot \sqrt{2}\right)} \cdot \left(\left(\sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}} \cdot \sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}}\right) \cdot \sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}}\right)\right)\]

13. Simplified 0.5

    \[\leadsto \left(x \cdot 0.5 - y\right) \cdot \left(\left(\color{blue}{{z}^{\frac{1}{2}}} \cdot \sqrt{2}\right) \cdot \left(\left(\sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}} \cdot \sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}}\right) \cdot \sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}}\right)\right)\]

14. Final simplification 0.5

    \[\leadsto \left(x \cdot 0.5 - y\right) \cdot \left(\left({z}^{\frac{1}{2}} \cdot \sqrt{2}\right) \cdot \left(\left(\sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}} \cdot \sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}}\right) \cdot \sqrt[3]{{\left(e^{t}\right)}^{\left(\frac{t}{2}\right)}}\right)\right)\]

Reproduce

herbie shell --seed 2020057 +o rules:numerics
(FPCore (x y z t)
  :name "Data.Number.Erf:$cinvnormcdf from erf-2.0.0.0, A"
  :precision binary64

  :herbie-target
  (* (* (- (* x 0.5) y) (sqrt (* z 2))) (pow (exp 1) (/ (* t t) 2)))

  (* (* (- (* x 0.5) y) (sqrt (* z 2))) (exp (/ (* t t) 2))))