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

Average Error: 24.9 → 8.1

Time: 12.7s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

• could not determine a ground truth for program body

  1. x = 8.463071591988411e-41
  2. y = 5.028654687011449e-267
  3. z = 2.7208697733301495e+159
  4. t = 5.176829154239403e-35

Math

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

↓

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

C

double f(double x, double y, double z, double t) {
        double r361717 = x;
        double r361718 = 1.0;
        double r361719 = y;
        double r361720 = r361718 - r361719;
        double r361721 = z;
        double r361722 = exp(r361721);
        double r361723 = r361719 * r361722;
        double r361724 = r361720 + r361723;
        double r361725 = log(r361724);
        double r361726 = t;
        double r361727 = r361725 / r361726;
        double r361728 = r361717 - r361727;
        return r361728;
}

↓

double f(double x, double y, double z, double t) {
        double r361729 = z;
        double r361730 = exp(r361729);
        double r361731 = 0.0;
        bool r361732 = r361730 <= r361731;
        double r361733 = x;
        double r361734 = 1.0;
        double r361735 = y;
        double r361736 = r361734 - r361735;
        double r361737 = r361735 * r361730;
        double r361738 = r361736 + r361737;
        double r361739 = log(r361738);
        double r361740 = 1.0;
        double r361741 = t;
        double r361742 = r361740 / r361741;
        double r361743 = r361739 * r361742;
        double r361744 = r361733 - r361743;
        double r361745 = r361729 * r361735;
        double r361746 = r361745 * r361742;
        double r361747 = r361734 * r361746;
        double r361748 = log(r361734);
        double r361749 = r361748 / r361741;
        double r361750 = 0.5;
        double r361751 = 2.0;
        double r361752 = pow(r361729, r361751);
        double r361753 = r361752 * r361735;
        double r361754 = r361753 / r361741;
        double r361755 = r361750 * r361754;
        double r361756 = r361749 + r361755;
        double r361757 = r361747 + r361756;
        double r361758 = r361733 - r361757;
        double r361759 = r361732 ? r361744 : r361758;
        return r361759;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	24.9
Target	15.6
Herbie	8.1

\[\begin{array}{l} \mathbf{if}\;z \lt -2.88746230882079466 \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.0

   1. Initial program 11.0

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

   3. Applied div-inv 11.1

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

   if 0.0 < (exp z)

   1. Initial program 30.5

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

   2. Taylor expanded around 0 6.8

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

   4. Applied div-inv 6.9

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

4. Final simplification 8.1

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

Reproduce

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

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

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