Kahan p13 Example 1

Average Error: 0.0 → 0.1

Time: 4.8s

Precision: 64

Math

\[\frac{1 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}}{2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}}\]

↓

\[\frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \sqrt[3]{{\left(\frac{2 \cdot t}{1 + t}\right)}^{6}}}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

C

double f(double t) {
        double r62635 = 1.0;
        double r62636 = 2.0;
        double r62637 = t;
        double r62638 = r62636 * r62637;
        double r62639 = r62635 + r62637;
        double r62640 = r62638 / r62639;
        double r62641 = r62640 * r62640;
        double r62642 = r62635 + r62641;
        double r62643 = r62636 + r62641;
        double r62644 = r62642 / r62643;
        return r62644;
}

↓

double f(double t) {
        double r62645 = 1.0;
        double r62646 = r62645 * r62645;
        double r62647 = 2.0;
        double r62648 = t;
        double r62649 = r62647 * r62648;
        double r62650 = r62645 + r62648;
        double r62651 = r62649 / r62650;
        double r62652 = r62651 * r62651;
        double r62653 = 6.0;
        double r62654 = pow(r62651, r62653);
        double r62655 = cbrt(r62654);
        double r62656 = r62652 * r62655;
        double r62657 = r62646 - r62656;
        double r62658 = r62647 + r62652;
        double r62659 = r62645 - r62652;
        double r62660 = r62658 * r62659;
        double r62661 = r62657 / r62660;
        return r62661;
}

Error

Bits error versus t

Derivation

1. Initial program 0.0

   \[\frac{1 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}}{2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}}\]
2. Using strategy rm

3. Applied flip-+ 0.0

   \[\leadsto \frac{\color{blue}{\frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}{1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}}}}{2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}}\]

4. Applied associate-/l/ 0.0

   \[\leadsto \color{blue}{\frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}}\]
5. Using strategy rm

6. Applied add-cbrt-cube 21.7

   \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{\color{blue}{\sqrt[3]{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}}\right)}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

7. Applied add-cbrt-cube 22.0

   \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot \color{blue}{\sqrt[3]{\left(t \cdot t\right) \cdot t}}}{\sqrt[3]{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}\right)}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

8. Applied add-cbrt-cube 22.0

   \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(\frac{2 \cdot t}{1 + t} \cdot \frac{\color{blue}{\sqrt[3]{\left(2 \cdot 2\right) \cdot 2}} \cdot \sqrt[3]{\left(t \cdot t\right) \cdot t}}{\sqrt[3]{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}\right)}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

9. Applied cbrt-unprod 22.0

   \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(\frac{2 \cdot t}{1 + t} \cdot \frac{\color{blue}{\sqrt[3]{\left(\left(2 \cdot 2\right) \cdot 2\right) \cdot \left(\left(t \cdot t\right) \cdot t\right)}}}{\sqrt[3]{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}\right)}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

10. Applied cbrt-undiv 22.0

    \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(\frac{2 \cdot t}{1 + t} \cdot \color{blue}{\sqrt[3]{\frac{\left(\left(2 \cdot 2\right) \cdot 2\right) \cdot \left(\left(t \cdot t\right) \cdot t\right)}{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}}\right)}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

11. Applied add-cbrt-cube 22.1

    \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(\frac{2 \cdot t}{\color{blue}{\sqrt[3]{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}} \cdot \sqrt[3]{\frac{\left(\left(2 \cdot 2\right) \cdot 2\right) \cdot \left(\left(t \cdot t\right) \cdot t\right)}{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}\right)}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

12. Applied add-cbrt-cube 22.0

    \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(\frac{2 \cdot \color{blue}{\sqrt[3]{\left(t \cdot t\right) \cdot t}}}{\sqrt[3]{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}} \cdot \sqrt[3]{\frac{\left(\left(2 \cdot 2\right) \cdot 2\right) \cdot \left(\left(t \cdot t\right) \cdot t\right)}{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}\right)}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

13. Applied add-cbrt-cube 22.0

    \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(\frac{\color{blue}{\sqrt[3]{\left(2 \cdot 2\right) \cdot 2}} \cdot \sqrt[3]{\left(t \cdot t\right) \cdot t}}{\sqrt[3]{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}} \cdot \sqrt[3]{\frac{\left(\left(2 \cdot 2\right) \cdot 2\right) \cdot \left(\left(t \cdot t\right) \cdot t\right)}{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}\right)}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

14. Applied cbrt-unprod 22.0

    \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(\frac{\color{blue}{\sqrt[3]{\left(\left(2 \cdot 2\right) \cdot 2\right) \cdot \left(\left(t \cdot t\right) \cdot t\right)}}}{\sqrt[3]{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}} \cdot \sqrt[3]{\frac{\left(\left(2 \cdot 2\right) \cdot 2\right) \cdot \left(\left(t \cdot t\right) \cdot t\right)}{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}\right)}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

15. Applied cbrt-undiv 22.0

    \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(\color{blue}{\sqrt[3]{\frac{\left(\left(2 \cdot 2\right) \cdot 2\right) \cdot \left(\left(t \cdot t\right) \cdot t\right)}{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}} \cdot \sqrt[3]{\frac{\left(\left(2 \cdot 2\right) \cdot 2\right) \cdot \left(\left(t \cdot t\right) \cdot t\right)}{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}\right)}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

16. Applied cbrt-unprod 22.0

    \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \color{blue}{\sqrt[3]{\frac{\left(\left(2 \cdot 2\right) \cdot 2\right) \cdot \left(\left(t \cdot t\right) \cdot t\right)}{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)} \cdot \frac{\left(\left(2 \cdot 2\right) \cdot 2\right) \cdot \left(\left(t \cdot t\right) \cdot t\right)}{\left(\left(1 + t\right) \cdot \left(1 + t\right)\right) \cdot \left(1 + t\right)}}}}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

17. Simplified 0.1

    \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \sqrt[3]{\color{blue}{{\left(\frac{2 \cdot t}{1 + t}\right)}^{6}}}}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

18. Final simplification 0.1

    \[\leadsto \frac{1 \cdot 1 - \left(\frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \sqrt[3]{{\left(\frac{2 \cdot t}{1 + t}\right)}^{6}}}{\left(2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right) \cdot \left(1 - \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}\right)}\]

Reproduce

herbie shell --seed 2019353 +o rules:numerics
(FPCore (t)
  :name "Kahan p13 Example 1"
  :precision binary64
  (/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))))