2nthrt (problem 3.4.6)

Average Error: 28.9 → 18.4

Time: 40.2s

Precision: 64

• could not determine a ground truth for program body

  1. x = 7.015171298646812e+194
  2. n = 4.52205504228614e-15

Math

\[{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}\]

↓

\[\begin{array}{l} \mathbf{if}\;\frac{1}{n} \le -1.425206190081909 \cdot 10^{-07}:\\ \;\;\;\;\log \left(e^{\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}} \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}}\right) \cdot \sqrt[3]{\mathsf{fma}\left(-{\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right) + \mathsf{fma}\left(1, {\left(x + 1\right)}^{\left(\frac{1}{n}\right)}, -{\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right)}\\ \mathbf{elif}\;\frac{1}{n} \le 1.0665423012237978:\\ \;\;\;\;\left(\frac{\frac{1}{x}}{n} - \frac{\frac{\frac{1}{2}}{n}}{x \cdot x}\right) - \left(-\frac{\log x}{\left(n \cdot n\right) \cdot x}\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(e^{e^{\frac{\mathsf{log1p}\left(x\right)}{n}} - {x}^{\left(\frac{1}{n}\right)}}\right)\\ \end{array}\]

C

double f(double x, double n) {
        double r1309943 = x;
        double r1309944 = 1.0;
        double r1309945 = r1309943 + r1309944;
        double r1309946 = n;
        double r1309947 = r1309944 / r1309946;
        double r1309948 = pow(r1309945, r1309947);
        double r1309949 = pow(r1309943, r1309947);
        double r1309950 = r1309948 - r1309949;
        return r1309950;
}

↓

double f(double x, double n) {
        double r1309951 = 1.0;
        double r1309952 = n;
        double r1309953 = r1309951 / r1309952;
        double r1309954 = -1.425206190081909e-07;
        bool r1309955 = r1309953 <= r1309954;
        double r1309956 = x;
        double r1309957 = r1309956 + r1309951;
        double r1309958 = pow(r1309957, r1309953);
        double r1309959 = pow(r1309956, r1309953);
        double r1309960 = r1309958 - r1309959;
        double r1309961 = cbrt(r1309960);
        double r1309962 = r1309961 * r1309961;
        double r1309963 = exp(r1309962);
        double r1309964 = log(r1309963);
        double r1309965 = cbrt(r1309956);
        double r1309966 = pow(r1309965, r1309953);
        double r1309967 = -r1309966;
        double r1309968 = r1309965 * r1309965;
        double r1309969 = pow(r1309968, r1309953);
        double r1309970 = r1309969 * r1309966;
        double r1309971 = fma(r1309967, r1309969, r1309970);
        double r1309972 = -r1309970;
        double r1309973 = fma(r1309951, r1309958, r1309972);
        double r1309974 = r1309971 + r1309973;
        double r1309975 = cbrt(r1309974);
        double r1309976 = r1309964 * r1309975;
        double r1309977 = 1.0665423012237978;
        bool r1309978 = r1309953 <= r1309977;
        double r1309979 = r1309951 / r1309956;
        double r1309980 = r1309979 / r1309952;
        double r1309981 = 0.5;
        double r1309982 = r1309981 / r1309952;
        double r1309983 = r1309956 * r1309956;
        double r1309984 = r1309982 / r1309983;
        double r1309985 = r1309980 - r1309984;
        double r1309986 = log(r1309956);
        double r1309987 = r1309952 * r1309952;
        double r1309988 = r1309987 * r1309956;
        double r1309989 = r1309986 / r1309988;
        double r1309990 = -r1309989;
        double r1309991 = r1309985 - r1309990;
        double r1309992 = log1p(r1309956);
        double r1309993 = r1309992 / r1309952;
        double r1309994 = exp(r1309993);
        double r1309995 = r1309994 - r1309959;
        double r1309996 = exp(r1309995);
        double r1309997 = log(r1309996);
        double r1309998 = r1309978 ? r1309991 : r1309997;
        double r1309999 = r1309955 ? r1309976 : r1309998;
        return r1309999;
}

Error

Bits error versus x

Bits error versus n

Derivation

1. Split input into 3 regimes

2. if (/ 1 n) < -1.425206190081909e-07

   1. Initial program 0.8

      \[{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}\]
   2. Using strategy rm

   3. Applied add-log-exp 1.1

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

   4. Applied add-log-exp 1.0

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

   5. Applied diff-log 1.0

      \[\leadsto \color{blue}{\log \left(\frac{e^{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)}}}{e^{{x}^{\left(\frac{1}{n}\right)}}}\right)}\]

   6. Simplified 1.0

      \[\leadsto \log \color{blue}{\left(e^{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}\right)}\]
   7. Using strategy rm

   8. Applied add-cube-cbrt 1.0

      \[\leadsto \log \left(e^{\color{blue}{\left(\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}} \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}\right) \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}}}\right)\]

   9. Applied exp-prod 1.0

      \[\leadsto \log \color{blue}{\left({\left(e^{\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}} \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}}\right)}^{\left(\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}\right)}\right)}\]

   10. Applied log-pow 1.0

       \[\leadsto \color{blue}{\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}} \cdot \log \left(e^{\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}} \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}}\right)}\]
   11. Using strategy rm

   12. Applied add-cube-cbrt 1.0

       \[\leadsto \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {\color{blue}{\left(\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \sqrt[3]{x}\right)}}^{\left(\frac{1}{n}\right)}} \cdot \log \left(e^{\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}} \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}}\right)\]

   13. Applied unpow-prod-down 1.0

       \[\leadsto \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - \color{blue}{{\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}}} \cdot \log \left(e^{\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}} \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}}\right)\]

   14. Applied *-un-lft-identity 1.0

       \[\leadsto \sqrt[3]{\color{blue}{1 \cdot {\left(x + 1\right)}^{\left(\frac{1}{n}\right)}} - {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}} \cdot \log \left(e^{\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}} \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}}\right)\]

   15. Applied prod-diff 1.0

       \[\leadsto \sqrt[3]{\color{blue}{\mathsf{fma}\left(1, {\left(x + 1\right)}^{\left(\frac{1}{n}\right)}, -{\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right) + \mathsf{fma}\left(-{\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right)}} \cdot \log \left(e^{\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}} \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}}\right)\]

   if -1.425206190081909e-07 < (/ 1 n) < 1.0665423012237978

   1. Initial program 44.4

      \[{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}\]
   2. Using strategy rm

   3. Applied add-log-exp 44.4

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

   4. Applied add-log-exp 44.4

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

   5. Applied diff-log 44.4

      \[\leadsto \color{blue}{\log \left(\frac{e^{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)}}}{e^{{x}^{\left(\frac{1}{n}\right)}}}\right)}\]

   6. Simplified 44.4

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

   7. Taylor expanded around inf 32.1

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

   8. Simplified 31.3

      \[\leadsto \color{blue}{\left(\frac{\frac{1}{x}}{n} - \frac{\frac{\frac{1}{2}}{n}}{x \cdot x}\right) - \left(-\frac{\log x}{x \cdot \left(n \cdot n\right)}\right)}\]

   if 1.0665423012237978 < (/ 1 n)

   1. Initial program 23.8

      \[{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}\]
   2. Using strategy rm

   3. Applied add-log-exp 23.8

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

   4. Applied add-log-exp 23.8

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

   5. Applied diff-log 23.8

      \[\leadsto \color{blue}{\log \left(\frac{e^{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)}}}{e^{{x}^{\left(\frac{1}{n}\right)}}}\right)}\]

   6. Simplified 23.8

      \[\leadsto \log \color{blue}{\left(e^{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}\right)}\]
   7. Using strategy rm

   8. Applied pow-to-exp 23.8

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

   9. Simplified 0.8

      \[\leadsto \log \left(e^{e^{\color{blue}{\frac{\mathsf{log1p}\left(x\right)}{n}}} - {x}^{\left(\frac{1}{n}\right)}}\right)\]
3. Recombined 3 regimes into one program.

4. Final simplification 18.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{1}{n} \le -1.425206190081909 \cdot 10^{-07}:\\ \;\;\;\;\log \left(e^{\sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}} \cdot \sqrt[3]{{\left(x + 1\right)}^{\left(\frac{1}{n}\right)} - {x}^{\left(\frac{1}{n}\right)}}}\right) \cdot \sqrt[3]{\mathsf{fma}\left(-{\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}, {\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right) + \mathsf{fma}\left(1, {\left(x + 1\right)}^{\left(\frac{1}{n}\right)}, -{\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\left(\frac{1}{n}\right)}\right)}\\ \mathbf{elif}\;\frac{1}{n} \le 1.0665423012237978:\\ \;\;\;\;\left(\frac{\frac{1}{x}}{n} - \frac{\frac{\frac{1}{2}}{n}}{x \cdot x}\right) - \left(-\frac{\log x}{\left(n \cdot n\right) \cdot x}\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(e^{e^{\frac{\mathsf{log1p}\left(x\right)}{n}} - {x}^{\left(\frac{1}{n}\right)}}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019152 +o rules:numerics
(FPCore (x n)
  :name "2nthrt (problem 3.4.6)"
  (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))))