System.Random.MWC.Distributions:truncatedExp from mwc-random-0.13.3.2

Average Error: 25.3 → 8.1

Time: 1.1m

Precision: 64

• could not determine a ground truth for program body

  1. x = -1.985095466690918e-37
  2. y = 1.329721963648757e+163
  3. z = 1.4413438782480998e+140
  4. t = 2.530003709242839e+61

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;e^{z} \le 0.9999999999999964472863211994990706443787:\\ \;\;\;\;x - \frac{1}{\frac{t}{\log \left(y \cdot e^{z} + \left(1 - y\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;x - \left(\left(1 \cdot \left(\frac{\sqrt[3]{z} \cdot \sqrt[3]{z}}{t} \cdot \left(y \cdot \sqrt[3]{z}\right)\right) + \frac{\left(z \cdot \left(z \cdot y\right)\right) \cdot 0.5}{t}\right) + \frac{\log 1}{t}\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r15660920 = x;
        double r15660921 = 1.0;
        double r15660922 = y;
        double r15660923 = r15660921 - r15660922;
        double r15660924 = z;
        double r15660925 = exp(r15660924);
        double r15660926 = r15660922 * r15660925;
        double r15660927 = r15660923 + r15660926;
        double r15660928 = log(r15660927);
        double r15660929 = t;
        double r15660930 = r15660928 / r15660929;
        double r15660931 = r15660920 - r15660930;
        return r15660931;
}

↓

double f(double x, double y, double z, double t) {
        double r15660932 = z;
        double r15660933 = exp(r15660932);
        double r15660934 = 0.9999999999999964;
        bool r15660935 = r15660933 <= r15660934;
        double r15660936 = x;
        double r15660937 = 1.0;
        double r15660938 = t;
        double r15660939 = y;
        double r15660940 = r15660939 * r15660933;
        double r15660941 = 1.0;
        double r15660942 = r15660941 - r15660939;
        double r15660943 = r15660940 + r15660942;
        double r15660944 = log(r15660943);
        double r15660945 = r15660938 / r15660944;
        double r15660946 = r15660937 / r15660945;
        double r15660947 = r15660936 - r15660946;
        double r15660948 = cbrt(r15660932);
        double r15660949 = r15660948 * r15660948;
        double r15660950 = r15660949 / r15660938;
        double r15660951 = r15660939 * r15660948;
        double r15660952 = r15660950 * r15660951;
        double r15660953 = r15660941 * r15660952;
        double r15660954 = r15660932 * r15660939;
        double r15660955 = r15660932 * r15660954;
        double r15660956 = 0.5;
        double r15660957 = r15660955 * r15660956;
        double r15660958 = r15660957 / r15660938;
        double r15660959 = r15660953 + r15660958;
        double r15660960 = log(r15660941);
        double r15660961 = r15660960 / r15660938;
        double r15660962 = r15660959 + r15660961;
        double r15660963 = r15660936 - r15660962;
        double r15660964 = r15660935 ? r15660947 : r15660963;
        return r15660964;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	25.3
Target	16.3
Herbie	8.1

\[\begin{array}{l} \mathbf{if}\;z \lt -2.887462308820794658905265984545350618896 \cdot 10^{119}:\\ \;\;\;\;\left(x - \frac{\frac{-0.5}{y \cdot t}}{z \cdot z}\right) - \frac{-0.5}{y \cdot t} \cdot \frac{\frac{2}{z}}{z \cdot z}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{\log \left(1 + z \cdot y\right)}{t}\\ \end{array}\]

Derivation

1. Split input into 2 regimes

2. if (exp z) < 0.9999999999999964

   1. Initial program 11.6

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

   3. Applied clear-num 11.7

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

   if 0.9999999999999964 < (exp z)

   1. Initial program 31.4

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

   2. Taylor expanded around 0 7.2

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

   3. Simplified 7.2

      \[\leadsto x - \color{blue}{\left(\frac{\log 1}{t} + \left(0.5 \cdot \frac{\left(y \cdot z\right) \cdot z}{t} + \frac{\left(1 \cdot y\right) \cdot z}{t}\right)\right)}\]
   4. Using strategy rm

   5. Applied associate-/l* 6.6

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

   6. Taylor expanded around 0 7.2

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

   7. Simplified 8.9

      \[\leadsto x - \left(\frac{\log 1}{t} + \color{blue}{\left(\frac{0.5 \cdot \left(\left(y \cdot z\right) \cdot z\right)}{t} + \frac{z}{\frac{t}{y}} \cdot 1\right)}\right)\]
   8. Using strategy rm

   9. Applied div-inv 8.9

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

   10. Applied add-cube-cbrt 9.1

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

   11. Applied times-frac 6.5

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

   12. Simplified 6.5

       \[\leadsto x - \left(\frac{\log 1}{t} + \left(\frac{0.5 \cdot \left(\left(y \cdot z\right) \cdot z\right)}{t} + \left(\frac{\sqrt[3]{z} \cdot \sqrt[3]{z}}{t} \cdot \color{blue}{\left(y \cdot \sqrt[3]{z}\right)}\right) \cdot 1\right)\right)\]
3. Recombined 2 regimes into one program.

4. Final simplification 8.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;e^{z} \le 0.9999999999999964472863211994990706443787:\\ \;\;\;\;x - \frac{1}{\frac{t}{\log \left(y \cdot e^{z} + \left(1 - y\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;x - \left(\left(1 \cdot \left(\frac{\sqrt[3]{z} \cdot \sqrt[3]{z}}{t} \cdot \left(y \cdot \sqrt[3]{z}\right)\right) + \frac{\left(z \cdot \left(z \cdot y\right)\right) \cdot 0.5}{t}\right) + \frac{\log 1}{t}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019168 
(FPCore (x y z t)
  :name "System.Random.MWC.Distributions:truncatedExp from mwc-random-0.13.3.2"

  :herbie-target
  (if (< z -2.8874623088207947e+119) (- (- x (/ (/ (- 0.5) (* y t)) (* z z))) (* (/ (- 0.5) (* y t)) (/ (/ 2.0 z) (* z z)))) (- x (/ (log (+ 1.0 (* z y))) t)))

  (- x (/ (log (+ (- 1.0 y) (* y (exp z)))) t)))