Average Error: 30.1 → 0.5
Time: 22.8s
Precision: 64
\[\sqrt[3]{x + 1} - \sqrt[3]{x}\]
↓
\[\frac{1}{\mathsf{fma}\left(\sqrt[3]{x + 1}, \sqrt[3]{x + 1}, \sqrt[3]{x} \cdot \left(\sqrt[3]{x} + \sqrt[3]{x + 1}\right)\right)}\]
\sqrt[3]{x + 1} - \sqrt[3]{x}
↓
\frac{1}{\mathsf{fma}\left(\sqrt[3]{x + 1}, \sqrt[3]{x + 1}, \sqrt[3]{x} \cdot \left(\sqrt[3]{x} + \sqrt[3]{x + 1}\right)\right)}
double f(double x) {
        double r54026 = x;
        double r54027 = 1.0;
        double r54028 = r54026 + r54027;
        double r54029 = cbrt(r54028);
        double r54030 = cbrt(r54026);
        double r54031 = r54029 - r54030;
        return r54031;
}
↓
double f(double x) {
        double r54032 = 1.0;
        double r54033 = x;
        double r54034 = r54033 + r54032;
        double r54035 = cbrt(r54034);
        double r54036 = cbrt(r54033);
        double r54037 = r54036 + r54035;
        double r54038 = r54036 * r54037;
        double r54039 = fma(r54035, r54035, r54038);
        double r54040 = r54032 / r54039;
        return r54040;
}

Error

Bits error versus x

Derivation

  1. Initial program 30.1

    \[\sqrt[3]{x + 1} - \sqrt[3]{x}\]
  2. Using strategy rm

  3. Applied add-log-exp31.8

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

  4. Applied add-log-exp31.8

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

  5. Applied diff-log31.8

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

  6. Simplified30.1

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

  8. Applied flip3--30.1

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

  9. Simplified29.7

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

  10. Simplified29.7

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

  12. Applied *-un-lft-identity29.7

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

  13. Applied *-un-lft-identity29.7

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

  14. Applied times-frac29.7

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

  15. Applied exp-prod29.7

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

  16. Applied log-pow0.5

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

  17. Simplified0.5

    \[\leadsto \frac{1 + 0}{\mathsf{fma}\left(\sqrt[3]{x + 1}, \sqrt[3]{x + 1}, \sqrt[3]{x} \cdot \left(\sqrt[3]{x} + \sqrt[3]{x + 1}\right)\right)} \cdot \color{blue}{1}\]

  18. Final simplification0.5

    \[\leadsto \frac{1}{\mathsf{fma}\left(\sqrt[3]{x + 1}, \sqrt[3]{x + 1}, \sqrt[3]{x} \cdot \left(\sqrt[3]{x} + \sqrt[3]{x + 1}\right)\right)}\]

Reproduce

herbie shell --seed 2019199 +o rules:numerics
(FPCore (x)
  :name "2cbrt (problem 3.3.4)"
  (- (cbrt (+ x 1.0)) (cbrt x)))