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

Average Error: 0.3 → 0.3

Time: 23.8s

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({\left({\left(e^{t}\right)}^{t}\right)}^{\left(\frac{\frac{1}{2}}{2}\right)} \cdot \left(\sqrt{z \cdot 2} \cdot \left(x \cdot 0.5\right) + \sqrt{z \cdot 2} \cdot \left(-y\right)\right)\right) \cdot {\left({\left(e^{t}\right)}^{t}\right)}^{\left(\frac{\frac{1}{2}}{2}\right)}\]

C

double f(double x, double y, double z, double t) {
        double r522343 = x;
        double r522344 = 0.5;
        double r522345 = r522343 * r522344;
        double r522346 = y;
        double r522347 = r522345 - r522346;
        double r522348 = z;
        double r522349 = 2.0;
        double r522350 = r522348 * r522349;
        double r522351 = sqrt(r522350);
        double r522352 = r522347 * r522351;
        double r522353 = t;
        double r522354 = r522353 * r522353;
        double r522355 = r522354 / r522349;
        double r522356 = exp(r522355);
        double r522357 = r522352 * r522356;
        return r522357;
}

↓

double f(double x, double y, double z, double t) {
        double r522358 = t;
        double r522359 = exp(r522358);
        double r522360 = pow(r522359, r522358);
        double r522361 = 0.5;
        double r522362 = 2.0;
        double r522363 = r522361 / r522362;
        double r522364 = pow(r522360, r522363);
        double r522365 = z;
        double r522366 = r522365 * r522362;
        double r522367 = sqrt(r522366);
        double r522368 = x;
        double r522369 = 0.5;
        double r522370 = r522368 * r522369;
        double r522371 = r522367 * r522370;
        double r522372 = y;
        double r522373 = -r522372;
        double r522374 = r522367 * r522373;
        double r522375 = r522371 + r522374;
        double r522376 = r522364 * r522375;
        double r522377 = 1.0;
        double r522378 = r522377 / r522362;
        double r522379 = 2.0;
        double r522380 = r522378 / r522379;
        double r522381 = pow(r522360, r522380);
        double r522382 = r522376 * r522381;
        return r522382;
}

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.3

\[\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 div-inv 0.3

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

4. Applied exp-prod 0.3

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

6. Applied *-un-lft-identity 0.3

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

7. Applied add-sqr-sqrt 0.3

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

8. Applied times-frac 0.3

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

9. Applied pow-unpow 0.3

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

10. Simplified 0.3

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

12. Applied sqr-pow 0.3

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

13. Applied associate-*r* 0.3

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

14. Simplified 0.3

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

16. Applied sub-neg 0.3

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

17. Applied distribute-lft-in 0.3

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

18. Final simplification 0.3

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

Reproduce

herbie shell --seed 2019235 +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))))