Numeric.SpecFunctions:invIncompleteBetaWorker from math-functions-0.1.5.2, G

Average Error: 9.79% → 1.35%

Time: 13.8s

Precision: binary64

Cost: 73872

Math

\[x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \]

↓

\[\begin{array}{l} t_0 := e^{-z}\\ t_1 := \log \left(\frac{y}{y + z}\right)\\ t_2 := \frac{e^{y \cdot t_1}}{y}\\ t_3 := \frac{1}{y} + x\\ \mathbf{if}\;t_2 \leq -2 \cdot 10^{+37}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;t_2 \leq -1 \cdot 10^{-280}:\\ \;\;\;\;x + \frac{t_0}{y}\\ \mathbf{elif}\;t_2 \leq 0:\\ \;\;\;\;x + \frac{{\left(e^{y}\right)}^{t_1}}{y}\\ \mathbf{elif}\;t_2 \leq 10^{-8}:\\ \;\;\;\;x + \frac{\mathsf{fma}\left(0.5, \frac{z \cdot \frac{z}{y}}{e^{z}}, t_0\right)}{y}\\ \mathbf{else}:\\ \;\;\;\;t_3\\ \end{array} \]

FPCore

(FPCore (x y z)
 :precision binary64
 (+ x (/ (exp (* y (log (/ y (+ z y))))) y)))

↓

(FPCore (x y z)
 :precision binary64
 (let* ((t_0 (exp (- z)))
        (t_1 (log (/ y (+ y z))))
        (t_2 (/ (exp (* y t_1)) y))
        (t_3 (+ (/ 1.0 y) x)))
   (if (<= t_2 -2e+37)
     t_3
     (if (<= t_2 -1e-280)
       (+ x (/ t_0 y))
       (if (<= t_2 0.0)
         (+ x (/ (pow (exp y) t_1) y))
         (if (<= t_2 1e-8)
           (+ x (/ (fma 0.5 (/ (* z (/ z y)) (exp z)) t_0) y))
           t_3))))))

C

double code(double x, double y, double z) {
	return x + (exp((y * log((y / (z + y))))) / y);
}

↓

double code(double x, double y, double z) {
	double t_0 = exp(-z);
	double t_1 = log((y / (y + z)));
	double t_2 = exp((y * t_1)) / y;
	double t_3 = (1.0 / y) + x;
	double tmp;
	if (t_2 <= -2e+37) {
		tmp = t_3;
	} else if (t_2 <= -1e-280) {
		tmp = x + (t_0 / y);
	} else if (t_2 <= 0.0) {
		tmp = x + (pow(exp(y), t_1) / y);
	} else if (t_2 <= 1e-8) {
		tmp = x + (fma(0.5, ((z * (z / y)) / exp(z)), t_0) / y);
	} else {
		tmp = t_3;
	}
	return tmp;
}

Julia

function code(x, y, z)
	return Float64(x + Float64(exp(Float64(y * log(Float64(y / Float64(z + y))))) / y))
end

↓

function code(x, y, z)
	t_0 = exp(Float64(-z))
	t_1 = log(Float64(y / Float64(y + z)))
	t_2 = Float64(exp(Float64(y * t_1)) / y)
	t_3 = Float64(Float64(1.0 / y) + x)
	tmp = 0.0
	if (t_2 <= -2e+37)
		tmp = t_3;
	elseif (t_2 <= -1e-280)
		tmp = Float64(x + Float64(t_0 / y));
	elseif (t_2 <= 0.0)
		tmp = Float64(x + Float64((exp(y) ^ t_1) / y));
	elseif (t_2 <= 1e-8)
		tmp = Float64(x + Float64(fma(0.5, Float64(Float64(z * Float64(z / y)) / exp(z)), t_0) / y));
	else
		tmp = t_3;
	end
	return tmp
end

Wolfram

code[x_, y_, z_] := N[(x + N[(N[Exp[N[(y * N[Log[N[(y / N[(z + y), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision] / y), $MachinePrecision]), $MachinePrecision]

↓

code[x_, y_, z_] := Block[{t$95$0 = N[Exp[(-z)], $MachinePrecision]}, Block[{t$95$1 = N[Log[N[(y / N[(y + z), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$2 = N[(N[Exp[N[(y * t$95$1), $MachinePrecision]], $MachinePrecision] / y), $MachinePrecision]}, Block[{t$95$3 = N[(N[(1.0 / y), $MachinePrecision] + x), $MachinePrecision]}, If[LessEqual[t$95$2, -2e+37], t$95$3, If[LessEqual[t$95$2, -1e-280], N[(x + N[(t$95$0 / y), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$2, 0.0], N[(x + N[(N[Power[N[Exp[y], $MachinePrecision], t$95$1], $MachinePrecision] / y), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$2, 1e-8], N[(x + N[(N[(0.5 * N[(N[(z * N[(z / y), $MachinePrecision]), $MachinePrecision] / N[Exp[z], $MachinePrecision]), $MachinePrecision] + t$95$0), $MachinePrecision] / y), $MachinePrecision]), $MachinePrecision], t$95$3]]]]]]]]

Target

Original	9.79%
Target	1.9%
Herbie	1.35%

\[\begin{array}{l} \mathbf{if}\;\frac{y}{z + y} < 7.11541576 \cdot 10^{-315}:\\ \;\;\;\;x + \frac{e^{\frac{-1}{z}}}{y}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{e^{\log \left({\left(\frac{y}{y + z}\right)}^{y}\right)}}{y}\\ \end{array} \]

Derivation

1. Split input into 4 regimes

2. if (/.f64 (exp.f64 (*.f64 y (log.f64 (/.f64 y (+.f64 z y))))) y) < -1.99999999999999991e37 or 1e-8 < (/.f64 (exp.f64 (*.f64 y (log.f64 (/.f64 y (+.f64 z y))))) y)

   1. Initial program 10.42

      \[x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \]

   2. Simplified 0.15

      \[\leadsto \color{blue}{x + \frac{{\left(e^{y}\right)}^{\log \left(\frac{y}{y + z}\right)}}{y}} \]
      Proof

      [Start] 10.42	\[ x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \]
      exp-prod [=>] 0.15	\[ x + \frac{\color{blue}{{\left(e^{y}\right)}^{\log \left(\frac{y}{z + y}\right)}}}{y} \]
      sqr-pow [=>] 0.15	\[ x + \frac{\color{blue}{{\left(e^{y}\right)}^{\left(\frac{\log \left(\frac{y}{z + y}\right)}{2}\right)} \cdot {\left(e^{y}\right)}^{\left(\frac{\log \left(\frac{y}{z + y}\right)}{2}\right)}}}{y} \]
      sqr-pow [<=] 0.15	\[ x + \frac{\color{blue}{{\left(e^{y}\right)}^{\log \left(\frac{y}{z + y}\right)}}}{y} \]
      +-commutative [=>] 0.15	\[ x + \frac{{\left(e^{y}\right)}^{\log \left(\frac{y}{\color{blue}{y + z}}\right)}}{y} \]

   3. Taylor expanded in y around inf 0.47

      \[\leadsto \color{blue}{\frac{1}{y} + x} \]

   if -1.99999999999999991e37 < (/.f64 (exp.f64 (*.f64 y (log.f64 (/.f64 y (+.f64 z y))))) y) < -9.9999999999999996e-281

   1. Initial program 3.86

      \[x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \]

   2. Simplified 3.86

      \[\leadsto \color{blue}{x + \frac{{\left(\frac{y}{y + z}\right)}^{y}}{y}} \]
      Proof

      [Start] 3.86	\[ x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \]
      *-commutative [=>] 3.86	\[ x + \frac{e^{\color{blue}{\log \left(\frac{y}{z + y}\right) \cdot y}}}{y} \]
      exp-prod [=>] 3.86	\[ x + \frac{\color{blue}{{\left(e^{\log \left(\frac{y}{z + y}\right)}\right)}^{y}}}{y} \]
      rem-exp-log [=>] 3.86	\[ x + \frac{{\color{blue}{\left(\frac{y}{z + y}\right)}}^{y}}{y} \]
      +-commutative [=>] 3.86	\[ x + \frac{{\left(\frac{y}{\color{blue}{y + z}}\right)}^{y}}{y} \]

   3. Taylor expanded in y around inf 4.53

      \[\leadsto x + \frac{\color{blue}{e^{-1 \cdot z}}}{y} \]

   4. Simplified 4.53

      \[\leadsto x + \frac{\color{blue}{e^{-z}}}{y} \]
      Proof

      [Start] 4.53	\[ x + \frac{e^{-1 \cdot z}}{y} \]
      mul-1-neg [=>] 4.53	\[ x + \frac{e^{\color{blue}{-z}}}{y} \]

   if -9.9999999999999996e-281 < (/.f64 (exp.f64 (*.f64 y (log.f64 (/.f64 y (+.f64 z y))))) y) < 0.0

   1. Initial program 30

      \[x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \]

   2. Simplified 0.4

      \[\leadsto \color{blue}{x + \frac{{\left(e^{y}\right)}^{\log \left(\frac{y}{y + z}\right)}}{y}} \]
      Proof

      [Start] 30	\[ x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \]
      exp-prod [=>] 0.4	\[ x + \frac{\color{blue}{{\left(e^{y}\right)}^{\log \left(\frac{y}{z + y}\right)}}}{y} \]
      sqr-pow [=>] 0.4	\[ x + \frac{\color{blue}{{\left(e^{y}\right)}^{\left(\frac{\log \left(\frac{y}{z + y}\right)}{2}\right)} \cdot {\left(e^{y}\right)}^{\left(\frac{\log \left(\frac{y}{z + y}\right)}{2}\right)}}}{y} \]
      sqr-pow [<=] 0.4	\[ x + \frac{\color{blue}{{\left(e^{y}\right)}^{\log \left(\frac{y}{z + y}\right)}}}{y} \]
      +-commutative [=>] 0.4	\[ x + \frac{{\left(e^{y}\right)}^{\log \left(\frac{y}{\color{blue}{y + z}}\right)}}{y} \]

   if 0.0 < (/.f64 (exp.f64 (*.f64 y (log.f64 (/.f64 y (+.f64 z y))))) y) < 1e-8

   1. Initial program 3.89

      \[x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \]

   2. Simplified 3.89

      \[\leadsto \color{blue}{x + \frac{{\left(\frac{y}{y + z}\right)}^{y}}{y}} \]
      Proof

      [Start] 3.89	\[ x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \]
      *-commutative [=>] 3.89	\[ x + \frac{e^{\color{blue}{\log \left(\frac{y}{z + y}\right) \cdot y}}}{y} \]
      exp-prod [=>] 3.89	\[ x + \frac{\color{blue}{{\left(e^{\log \left(\frac{y}{z + y}\right)}\right)}^{y}}}{y} \]
      rem-exp-log [=>] 3.89	\[ x + \frac{{\color{blue}{\left(\frac{y}{z + y}\right)}}^{y}}{y} \]
      +-commutative [=>] 3.89	\[ x + \frac{{\left(\frac{y}{\color{blue}{y + z}}\right)}^{y}}{y} \]

   3. Taylor expanded in y around inf 4.55

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

   4. Simplified 4.55

      \[\leadsto x + \frac{\color{blue}{\mathsf{fma}\left(0.5, \frac{z \cdot z}{y} \cdot e^{-z}, e^{-z}\right)}}{y} \]
      Proof

      [Start] 4.55	\[ x + \frac{0.5 \cdot \frac{e^{-1 \cdot z} \cdot \left(-1 \cdot {z}^{2} + 2 \cdot {z}^{2}\right)}{y} + e^{-1 \cdot z}}{y} \]
      fma-def [=>] 4.55	\[ x + \frac{\color{blue}{\mathsf{fma}\left(0.5, \frac{e^{-1 \cdot z} \cdot \left(-1 \cdot {z}^{2} + 2 \cdot {z}^{2}\right)}{y}, e^{-1 \cdot z}\right)}}{y} \]
      *-commutative [=>] 4.55	\[ x + \frac{\mathsf{fma}\left(0.5, \frac{\color{blue}{\left(-1 \cdot {z}^{2} + 2 \cdot {z}^{2}\right) \cdot e^{-1 \cdot z}}}{y}, e^{-1 \cdot z}\right)}{y} \]
      associate-/l* [=>] 4.55	\[ x + \frac{\mathsf{fma}\left(0.5, \color{blue}{\frac{-1 \cdot {z}^{2} + 2 \cdot {z}^{2}}{\frac{y}{e^{-1 \cdot z}}}}, e^{-1 \cdot z}\right)}{y} \]
      distribute-rgt-out [=>] 4.55	\[ x + \frac{\mathsf{fma}\left(0.5, \frac{\color{blue}{{z}^{2} \cdot \left(-1 + 2\right)}}{\frac{y}{e^{-1 \cdot z}}}, e^{-1 \cdot z}\right)}{y} \]
      metadata-eval [=>] 4.55	\[ x + \frac{\mathsf{fma}\left(0.5, \frac{{z}^{2} \cdot \color{blue}{1}}{\frac{y}{e^{-1 \cdot z}}}, e^{-1 \cdot z}\right)}{y} \]
      *-rgt-identity [=>] 4.55	\[ x + \frac{\mathsf{fma}\left(0.5, \frac{\color{blue}{{z}^{2}}}{\frac{y}{e^{-1 \cdot z}}}, e^{-1 \cdot z}\right)}{y} \]
      associate-/r/ [=>] 4.55	\[ x + \frac{\mathsf{fma}\left(0.5, \color{blue}{\frac{{z}^{2}}{y} \cdot e^{-1 \cdot z}}, e^{-1 \cdot z}\right)}{y} \]
      unpow2 [=>] 4.55	\[ x + \frac{\mathsf{fma}\left(0.5, \frac{\color{blue}{z \cdot z}}{y} \cdot e^{-1 \cdot z}, e^{-1 \cdot z}\right)}{y} \]
      mul-1-neg [=>] 4.55	\[ x + \frac{\mathsf{fma}\left(0.5, \frac{z \cdot z}{y} \cdot e^{\color{blue}{-z}}, e^{-1 \cdot z}\right)}{y} \]
      mul-1-neg [=>] 4.55	\[ x + \frac{\mathsf{fma}\left(0.5, \frac{z \cdot z}{y} \cdot e^{-z}, e^{\color{blue}{-z}}\right)}{y} \]

   5. Applied egg-rr 0.02

      \[\leadsto x + \frac{\mathsf{fma}\left(0.5, \color{blue}{\frac{z}{\frac{y}{z} \cdot e^{z}}}, e^{-z}\right)}{y} \]

   6. Simplified 0.12

      \[\leadsto x + \frac{\mathsf{fma}\left(0.5, \color{blue}{\frac{z \cdot \frac{z}{y}}{e^{z}}}, e^{-z}\right)}{y} \]
      Proof

      [Start] 0.02	\[ x + \frac{\mathsf{fma}\left(0.5, \frac{z}{\frac{y}{z} \cdot e^{z}}, e^{-z}\right)}{y} \]
      associate-/r* [=>] 0.12	\[ x + \frac{\mathsf{fma}\left(0.5, \color{blue}{\frac{\frac{z}{\frac{y}{z}}}{e^{z}}}, e^{-z}\right)}{y} \]
      associate-/l* [<=] 4.55	\[ x + \frac{\mathsf{fma}\left(0.5, \frac{\color{blue}{\frac{z \cdot z}{y}}}{e^{z}}, e^{-z}\right)}{y} \]
      associate-*r/ [<=] 0.12	\[ x + \frac{\mathsf{fma}\left(0.5, \frac{\color{blue}{z \cdot \frac{z}{y}}}{e^{z}}, e^{-z}\right)}{y} \]

3. Recombined 4 regimes into one program.

4. Final simplification 1.35

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{e^{y \cdot \log \left(\frac{y}{y + z}\right)}}{y} \leq -2 \cdot 10^{+37}:\\ \;\;\;\;\frac{1}{y} + x\\ \mathbf{elif}\;\frac{e^{y \cdot \log \left(\frac{y}{y + z}\right)}}{y} \leq -1 \cdot 10^{-280}:\\ \;\;\;\;x + \frac{e^{-z}}{y}\\ \mathbf{elif}\;\frac{e^{y \cdot \log \left(\frac{y}{y + z}\right)}}{y} \leq 0:\\ \;\;\;\;x + \frac{{\left(e^{y}\right)}^{\log \left(\frac{y}{y + z}\right)}}{y}\\ \mathbf{elif}\;\frac{e^{y \cdot \log \left(\frac{y}{y + z}\right)}}{y} \leq 10^{-8}:\\ \;\;\;\;x + \frac{\mathsf{fma}\left(0.5, \frac{z \cdot \frac{z}{y}}{e^{z}}, e^{-z}\right)}{y}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{y} + x\\ \end{array} \]

Alternatives

Alternative 1
Error	1.32%
Cost	60560

\[\begin{array}{l} t_0 := \log \left(\frac{y}{y + z}\right)\\ t_1 := \frac{1}{y} + x\\ t_2 := \frac{e^{y \cdot t_0}}{y}\\ t_3 := x + \frac{e^{-z}}{y}\\ \mathbf{if}\;t_2 \leq -2 \cdot 10^{+37}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t_2 \leq -1 \cdot 10^{-280}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;t_2 \leq 0:\\ \;\;\;\;x + \frac{{\left(e^{y}\right)}^{t_0}}{y}\\ \mathbf{elif}\;t_2 \leq 10^{-8}:\\ \;\;\;\;t_3\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 2
Error	1.15%
Cost	7049

\[\begin{array}{l} \mathbf{if}\;y \leq -5 \cdot 10^{+183} \lor \neg \left(y \leq 8.5 \cdot 10^{-23}\right):\\ \;\;\;\;x + \frac{e^{-z}}{y}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{y} + x\\ \end{array} \]

Alternative 3
Error	23.06%
Cost	456

\[\begin{array}{l} \mathbf{if}\;y \leq -1 \cdot 10^{-70}:\\ \;\;\;\;x\\ \mathbf{elif}\;y \leq 2.8 \cdot 10^{-10}:\\ \;\;\;\;\frac{1}{y}\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 4
Error	4.02%
Cost	320

\[\frac{1}{y} + x \]

Alternative 5
Error	43.95%
Cost	64

\[x \]

Reproduce

herbie shell --seed 2023088 
(FPCore (x y z)
  :name "Numeric.SpecFunctions:invIncompleteBetaWorker from math-functions-0.1.5.2, G"
  :precision binary64

  :herbie-target
  (if (< (/ y (+ z y)) 7.11541576e-315) (+ x (/ (exp (/ -1.0 z)) y)) (+ x (/ (exp (log (pow (/ y (+ y z)) y))) y)))

  (+ x (/ (exp (* y (log (/ y (+ z y))))) y)))