VandenBroeck and Keller, Equation (6)

Average Error: 16.4 → 8.6

Time: 13.2s

Precision: 64

• could not determine a ground truth for program body

  1. F = 9.835650614246157e+92
  2. l = 2649526956147094.5

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

Math

\[\pi \cdot \ell - \frac{1}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]

↓

\[\begin{array}{l} \mathbf{if}\;\pi \cdot \ell \le -3.25877154259171114 \cdot 10^{163}:\\ \;\;\;\;\pi \cdot \ell - \frac{1}{F} \cdot \frac{1 \cdot \sin \left(\pi \cdot \ell\right)}{F \cdot \cos \left(\left(\sqrt[3]{\pi \cdot \ell} \cdot \sqrt[3]{\pi \cdot \ell}\right) \cdot \left(\sqrt[3]{-1} \cdot \sqrt[3]{e^{\log \pi - \log \left(\frac{-1}{\ell}\right)}}\right)\right)}\\ \mathbf{elif}\;\pi \cdot \ell \le 7.52430755046992877 \cdot 10^{152}:\\ \;\;\;\;\pi \cdot \ell - \frac{1}{F} \cdot \frac{1 \cdot \sin \left(\pi \cdot \ell\right)}{F \cdot \left(\left(\frac{1}{24} \cdot \left({\pi}^{4} \cdot {\ell}^{4}\right) + 1\right) - \frac{1}{2} \cdot \left({\pi}^{2} \cdot {\ell}^{2}\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\sqrt{\pi} \cdot \left(\sqrt{\pi} \cdot \ell\right)\right)\right)\\ \end{array}\]

C

double f(double F, double l) {
        double r16729 = atan2(1.0, 0.0);
        double r16730 = l;
        double r16731 = r16729 * r16730;
        double r16732 = 1.0;
        double r16733 = F;
        double r16734 = r16733 * r16733;
        double r16735 = r16732 / r16734;
        double r16736 = tan(r16731);
        double r16737 = r16735 * r16736;
        double r16738 = r16731 - r16737;
        return r16738;
}

↓

double f(double F, double l) {
        double r16739 = atan2(1.0, 0.0);
        double r16740 = l;
        double r16741 = r16739 * r16740;
        double r16742 = -3.258771542591711e+163;
        bool r16743 = r16741 <= r16742;
        double r16744 = 1.0;
        double r16745 = F;
        double r16746 = r16744 / r16745;
        double r16747 = 1.0;
        double r16748 = sin(r16741);
        double r16749 = r16747 * r16748;
        double r16750 = cbrt(r16741);
        double r16751 = r16750 * r16750;
        double r16752 = -1.0;
        double r16753 = cbrt(r16752);
        double r16754 = log(r16739);
        double r16755 = r16752 / r16740;
        double r16756 = log(r16755);
        double r16757 = r16754 - r16756;
        double r16758 = exp(r16757);
        double r16759 = cbrt(r16758);
        double r16760 = r16753 * r16759;
        double r16761 = r16751 * r16760;
        double r16762 = cos(r16761);
        double r16763 = r16745 * r16762;
        double r16764 = r16749 / r16763;
        double r16765 = r16746 * r16764;
        double r16766 = r16741 - r16765;
        double r16767 = 7.524307550469929e+152;
        bool r16768 = r16741 <= r16767;
        double r16769 = 0.041666666666666664;
        double r16770 = 4.0;
        double r16771 = pow(r16739, r16770);
        double r16772 = pow(r16740, r16770);
        double r16773 = r16771 * r16772;
        double r16774 = r16769 * r16773;
        double r16775 = r16774 + r16744;
        double r16776 = 0.5;
        double r16777 = 2.0;
        double r16778 = pow(r16739, r16777);
        double r16779 = pow(r16740, r16777);
        double r16780 = r16778 * r16779;
        double r16781 = r16776 * r16780;
        double r16782 = r16775 - r16781;
        double r16783 = r16745 * r16782;
        double r16784 = r16749 / r16783;
        double r16785 = r16746 * r16784;
        double r16786 = r16741 - r16785;
        double r16787 = r16747 / r16745;
        double r16788 = sqrt(r16739);
        double r16789 = r16788 * r16740;
        double r16790 = r16788 * r16789;
        double r16791 = tan(r16790);
        double r16792 = r16787 * r16791;
        double r16793 = r16746 * r16792;
        double r16794 = r16741 - r16793;
        double r16795 = r16768 ? r16786 : r16794;
        double r16796 = r16743 ? r16766 : r16795;
        return r16796;
}

Error

Bits error versus F

Bits error versus l

Derivation

1. Split input into 3 regimes

2. if (* PI l) < -3.258771542591711e+163

   1. Initial program 19.2

      \[\pi \cdot \ell - \frac{1}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]
   2. Using strategy rm

   3. Applied *-un-lft-identity 19.2

      \[\leadsto \pi \cdot \ell - \frac{\color{blue}{1 \cdot 1}}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]

   4. Applied times-frac 19.2

      \[\leadsto \pi \cdot \ell - \color{blue}{\left(\frac{1}{F} \cdot \frac{1}{F}\right)} \cdot \tan \left(\pi \cdot \ell\right)\]

   5. Applied associate-*l* 19.2

      \[\leadsto \pi \cdot \ell - \color{blue}{\frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\pi \cdot \ell\right)\right)}\]
   6. Using strategy rm

   7. Applied tan-quot 19.2

      \[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \color{blue}{\frac{\sin \left(\pi \cdot \ell\right)}{\cos \left(\pi \cdot \ell\right)}}\right)\]

   8. Applied frac-times 19.2

      \[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \color{blue}{\frac{1 \cdot \sin \left(\pi \cdot \ell\right)}{F \cdot \cos \left(\pi \cdot \ell\right)}}\]
   9. Using strategy rm

   10. Applied add-cube-cbrt 19.2

       \[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \frac{1 \cdot \sin \left(\pi \cdot \ell\right)}{F \cdot \cos \color{blue}{\left(\left(\sqrt[3]{\pi \cdot \ell} \cdot \sqrt[3]{\pi \cdot \ell}\right) \cdot \sqrt[3]{\pi \cdot \ell}\right)}}\]

   11. Taylor expanded around -inf 19.2

       \[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \frac{1 \cdot \sin \left(\pi \cdot \ell\right)}{F \cdot \cos \left(\left(\sqrt[3]{\pi \cdot \ell} \cdot \sqrt[3]{\pi \cdot \ell}\right) \cdot \color{blue}{\left(\sqrt[3]{-1} \cdot e^{\frac{1}{3} \cdot \left(\log \pi - \log \left(\frac{-1}{\ell}\right)\right)}\right)}\right)}\]

   12. Simplified 19.2

       \[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \frac{1 \cdot \sin \left(\pi \cdot \ell\right)}{F \cdot \cos \left(\left(\sqrt[3]{\pi \cdot \ell} \cdot \sqrt[3]{\pi \cdot \ell}\right) \cdot \color{blue}{\left(\sqrt[3]{-1} \cdot \sqrt[3]{e^{\log \pi - \log \left(\frac{-1}{\ell}\right)}}\right)}\right)}\]

   if -3.258771542591711e+163 < (* PI l) < 7.524307550469929e+152

   1. Initial program 15.2

      \[\pi \cdot \ell - \frac{1}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]
   2. Using strategy rm

   3. Applied *-un-lft-identity 15.2

      \[\leadsto \pi \cdot \ell - \frac{\color{blue}{1 \cdot 1}}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]

   4. Applied times-frac 15.2

      \[\leadsto \pi \cdot \ell - \color{blue}{\left(\frac{1}{F} \cdot \frac{1}{F}\right)} \cdot \tan \left(\pi \cdot \ell\right)\]

   5. Applied associate-*l* 9.7

      \[\leadsto \pi \cdot \ell - \color{blue}{\frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\pi \cdot \ell\right)\right)}\]
   6. Using strategy rm

   7. Applied tan-quot 9.7

      \[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \color{blue}{\frac{\sin \left(\pi \cdot \ell\right)}{\cos \left(\pi \cdot \ell\right)}}\right)\]

   8. Applied frac-times 9.7

      \[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \color{blue}{\frac{1 \cdot \sin \left(\pi \cdot \ell\right)}{F \cdot \cos \left(\pi \cdot \ell\right)}}\]

   9. Taylor expanded around 0 4.4

      \[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \frac{1 \cdot \sin \left(\pi \cdot \ell\right)}{F \cdot \color{blue}{\left(\left(\frac{1}{24} \cdot \left({\pi}^{4} \cdot {\ell}^{4}\right) + 1\right) - \frac{1}{2} \cdot \left({\pi}^{2} \cdot {\ell}^{2}\right)\right)}}\]

   if 7.524307550469929e+152 < (* PI l)

   1. Initial program 20.2

      \[\pi \cdot \ell - \frac{1}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]
   2. Using strategy rm

   3. Applied *-un-lft-identity 20.2

      \[\leadsto \pi \cdot \ell - \frac{\color{blue}{1 \cdot 1}}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]

   4. Applied times-frac 20.2

      \[\leadsto \pi \cdot \ell - \color{blue}{\left(\frac{1}{F} \cdot \frac{1}{F}\right)} \cdot \tan \left(\pi \cdot \ell\right)\]

   5. Applied associate-*l* 20.2

      \[\leadsto \pi \cdot \ell - \color{blue}{\frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\pi \cdot \ell\right)\right)}\]
   6. Using strategy rm

   7. Applied add-sqr-sqrt 20.2

      \[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\color{blue}{\left(\sqrt{\pi} \cdot \sqrt{\pi}\right)} \cdot \ell\right)\right)\]

   8. Applied associate-*l* 20.2

      \[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \color{blue}{\left(\sqrt{\pi} \cdot \left(\sqrt{\pi} \cdot \ell\right)\right)}\right)\]
3. Recombined 3 regimes into one program.

4. Final simplification 8.6

   \[\leadsto \begin{array}{l} \mathbf{if}\;\pi \cdot \ell \le -3.25877154259171114 \cdot 10^{163}:\\ \;\;\;\;\pi \cdot \ell - \frac{1}{F} \cdot \frac{1 \cdot \sin \left(\pi \cdot \ell\right)}{F \cdot \cos \left(\left(\sqrt[3]{\pi \cdot \ell} \cdot \sqrt[3]{\pi \cdot \ell}\right) \cdot \left(\sqrt[3]{-1} \cdot \sqrt[3]{e^{\log \pi - \log \left(\frac{-1}{\ell}\right)}}\right)\right)}\\ \mathbf{elif}\;\pi \cdot \ell \le 7.52430755046992877 \cdot 10^{152}:\\ \;\;\;\;\pi \cdot \ell - \frac{1}{F} \cdot \frac{1 \cdot \sin \left(\pi \cdot \ell\right)}{F \cdot \left(\left(\frac{1}{24} \cdot \left({\pi}^{4} \cdot {\ell}^{4}\right) + 1\right) - \frac{1}{2} \cdot \left({\pi}^{2} \cdot {\ell}^{2}\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\sqrt{\pi} \cdot \left(\sqrt{\pi} \cdot \ell\right)\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020042 
(FPCore (F l)
  :name "VandenBroeck and Keller, Equation (6)"
  :precision binary64
  (- (* PI l) (* (/ 1 (* F F)) (tan (* PI l)))))