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

Average Error: 0.0 → 0.0

Time: 3.7s

Precision: binary64

Cost: 6976

Math

\[x - \frac{y}{1 + \frac{x \cdot y}{2}} \]

↓

\[x + \frac{1}{\mathsf{fma}\left(x, -0.5, \frac{-1}{y}\right)} \]

FPCore

(FPCore (x y) :precision binary64 (- x (/ y (+ 1.0 (/ (* x y) 2.0)))))

↓

(FPCore (x y) :precision binary64 (+ x (/ 1.0 (fma x -0.5 (/ -1.0 y)))))

C

double code(double x, double y) {
	return x - (y / (1.0 + ((x * y) / 2.0)));
}

↓

double code(double x, double y) {
	return x + (1.0 / fma(x, -0.5, (-1.0 / y)));
}

Julia

function code(x, y)
	return Float64(x - Float64(y / Float64(1.0 + Float64(Float64(x * y) / 2.0))))
end

↓

function code(x, y)
	return Float64(x + Float64(1.0 / fma(x, -0.5, Float64(-1.0 / y))))
end

Wolfram

code[x_, y_] := N[(x - N[(y / N[(1.0 + N[(N[(x * y), $MachinePrecision] / 2.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

↓

code[x_, y_] := N[(x + N[(1.0 / N[(x * -0.5 + N[(-1.0 / y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 0.0

   \[x - \frac{y}{1 + \frac{x \cdot y}{2}} \]

2. Simplified 0.0

   \[\leadsto \color{blue}{x + \frac{1}{\mathsf{fma}\left(x, -0.5, \frac{-1}{y}\right)}} \]
   Proof
   (+.f64 x (/.f64 1 (fma.f64 x -1/2 (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (fma.f64 x (Rewrite<= metadata-eval (/.f64 1 -2)) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (fma.f64 x (/.f64 1 (Rewrite<= metadata-eval (/.f64 2 -1))) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x (/.f64 1 (/.f64 2 -1))) (/.f64 -1 y))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 1 (/.f64 2 -1)) x)) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (+.f64 (*.f64 (/.f64 1 (Rewrite=> metadata-eval -2)) x) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (+.f64 (*.f64 (Rewrite=> metadata-eval -1/2) x) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (+.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 -1 2)) x) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (+.f64 (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 2 x))) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 x) 2)) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 x 2))) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (Rewrite=> fma-def_binary64 (fma.f64 -1 (/.f64 x 2) (/.f64 -1 y))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (fma.f64 (Rewrite<= metadata-eval (neg.f64 1)) (/.f64 x 2) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (fma.f64 (neg.f64 (Rewrite<= *-inverses_binary64 (/.f64 y y))) (/.f64 x 2) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (fma.f64 (Rewrite<= distribute-frac-neg_binary64 (/.f64 (neg.f64 y) y)) (/.f64 x 2) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (fma.f64 (/.f64 (neg.f64 y) y) (Rewrite<= /-rgt-identity_binary64 (/.f64 (/.f64 x 2) 1)) (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (fma.f64 (/.f64 (neg.f64 y) y) (/.f64 (/.f64 x 2) 1) (/.f64 (Rewrite<= metadata-eval (neg.f64 1)) y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (fma.f64 (/.f64 (neg.f64 y) y) (/.f64 (/.f64 x 2) 1) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 1 y)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (/.f64 (neg.f64 y) y) (/.f64 (/.f64 x 2) 1)) (/.f64 1 y))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (-.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (neg.f64 y) (/.f64 x 2)) (*.f64 y 1))) (/.f64 1 y)))): 3 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (-.f64 (/.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 y (/.f64 x 2)))) (*.f64 y 1)) (/.f64 1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (-.f64 (/.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 x 2) y))) (*.f64 y 1)) (/.f64 1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (-.f64 (/.f64 (neg.f64 (Rewrite<= associate-/r/_binary64 (/.f64 x (/.f64 2 y)))) (*.f64 y 1)) (/.f64 1 y)))): 5 points increase in error, 1 points decrease in error
   (+.f64 x (/.f64 1 (-.f64 (/.f64 (Rewrite<= distribute-frac-neg_binary64 (/.f64 (neg.f64 x) (/.f64 2 y))) (*.f64 y 1)) (/.f64 1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (-.f64 (/.f64 (/.f64 (neg.f64 x) (/.f64 2 y)) (Rewrite=> *-rgt-identity_binary64 y)) (/.f64 1 y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 1 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (/.f64 (neg.f64 x) (/.f64 2 y)) 1) y)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 1 y) (-.f64 (/.f64 (neg.f64 x) (/.f64 2 y)) 1)))): 7 points increase in error, 9 points decrease in error
   (+.f64 x (/.f64 (Rewrite=> *-lft-identity_binary64 y) (-.f64 (/.f64 (neg.f64 x) (/.f64 2 y)) 1))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 y (Rewrite=> sub-neg_binary64 (+.f64 (/.f64 (neg.f64 x) (/.f64 2 y)) (neg.f64 1))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 y (+.f64 (Rewrite=> distribute-frac-neg_binary64 (neg.f64 (/.f64 x (/.f64 2 y)))) (neg.f64 1)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 y (+.f64 (neg.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 x y) 2))) (neg.f64 1)))): 3 points increase in error, 4 points decrease in error
   (+.f64 x (/.f64 y (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (/.f64 (*.f64 x y) 2) 1))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 y (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (/.f64 (*.f64 x y) 2)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 y (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (+.f64 1 (/.f64 (*.f64 x y) 2)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 y (+.f64 1 (/.f64 (*.f64 x y) 2))) -1))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 (/.f64 y (+.f64 1 (/.f64 (*.f64 x y) 2))) (Rewrite<= metadata-eval (/.f64 1 -1)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (/.f64 y (+.f64 1 (/.f64 (*.f64 x y) 2))) -1) 1))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (/.f64 y (+.f64 1 (/.f64 (*.f64 x y) 2))))) 1)): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 y (+.f64 1 (/.f64 (*.f64 x y) 2))))) 1)): 0 points increase in error, 0 points decrease in error
   (+.f64 x (Rewrite=> /-rgt-identity_binary64 (neg.f64 (/.f64 y (+.f64 1 (/.f64 (*.f64 x y) 2)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (/.f64 y (+.f64 1 (/.f64 (*.f64 x y) 2)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 y (+.f64 1 (/.f64 (*.f64 x y) 2))) -1))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (Rewrite<= *-commutative_binary64 (*.f64 -1 (/.f64 y (+.f64 1 (/.f64 (*.f64 x y) 2)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 y (+.f64 1 (/.f64 (*.f64 x y) 2)))))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= sub-neg_binary64 (-.f64 x (/.f64 y (+.f64 1 (/.f64 (*.f64 x y) 2))))): 0 points increase in error, 0 points decrease in error

3. Final simplification 0.0

   \[\leadsto x + \frac{1}{\mathsf{fma}\left(x, -0.5, \frac{-1}{y}\right)} \]

Alternatives

Alternative 1
Error	0.0
Cost	704

\[x - \frac{y}{1 + \frac{x \cdot y}{2}} \]

Alternative 2
Error	5.6
Cost	584

\[\begin{array}{l} t_0 := x - \frac{2}{x}\\ \mathbf{if}\;y \leq -1.5595933653061966 \cdot 10^{+106}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;y \leq 4.0622479262351446 \cdot 10^{+72}:\\ \;\;\;\;x - y\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]

Alternative 3
Error	23.6
Cost	456

\[\begin{array}{l} \mathbf{if}\;x \leq -1.358022098333293 \cdot 10^{-9}:\\ \;\;\;\;x\\ \mathbf{elif}\;x \leq -9.742732643486057 \cdot 10^{-188}:\\ \;\;\;\;\frac{-2}{x}\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 4
Error	8.5
Cost	456

\[\begin{array}{l} \mathbf{if}\;x \leq -9337196.738203213:\\ \;\;\;\;x\\ \mathbf{elif}\;x \leq 0.0014032615343855333:\\ \;\;\;\;x - y\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 5
Error	23.7
Cost	64

\[x \]

Reproduce

herbie shell --seed 2022294 
(FPCore (x y)
  :name "Data.Number.Erf:$cinvnormcdf from erf-2.0.0.0, B"
  :precision binary64
  (- x (/ y (+ 1.0 (/ (* x y) 2.0)))))