Toniolo and Linder, Equation (10-)

Average Error: 47.9 → 8.0

Time: 39.4s

Precision: 64

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

Math

\[\frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) - 1\right)}\]

↓

\[\begin{array}{l} \mathbf{if}\;t \le -3.02098643531036224 \cdot 10^{180}:\\ \;\;\;\;\left(2 \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{1}{{t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right)\right)\right) \cdot \ell\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(2 \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \left(\cos k \cdot \ell\right)\right)\right)\right) \cdot \ell}{{\left(\sin k\right)}^{2}}\\ \end{array}\]

C

double f(double t, double l, double k) {
        double r126750 = 2.0;
        double r126751 = t;
        double r126752 = 3.0;
        double r126753 = pow(r126751, r126752);
        double r126754 = l;
        double r126755 = r126754 * r126754;
        double r126756 = r126753 / r126755;
        double r126757 = k;
        double r126758 = sin(r126757);
        double r126759 = r126756 * r126758;
        double r126760 = tan(r126757);
        double r126761 = r126759 * r126760;
        double r126762 = 1.0;
        double r126763 = r126757 / r126751;
        double r126764 = pow(r126763, r126750);
        double r126765 = r126762 + r126764;
        double r126766 = r126765 - r126762;
        double r126767 = r126761 * r126766;
        double r126768 = r126750 / r126767;
        return r126768;
}

↓

double f(double t, double l, double k) {
        double r126769 = t;
        double r126770 = -3.0209864353103622e+180;
        bool r126771 = r126769 <= r126770;
        double r126772 = 2.0;
        double r126773 = 1.0;
        double r126774 = k;
        double r126775 = 2.0;
        double r126776 = r126772 / r126775;
        double r126777 = pow(r126774, r126776);
        double r126778 = r126773 / r126777;
        double r126779 = 1.0;
        double r126780 = pow(r126778, r126779);
        double r126781 = pow(r126769, r126779);
        double r126782 = r126773 / r126781;
        double r126783 = pow(r126782, r126779);
        double r126784 = cos(r126774);
        double r126785 = l;
        double r126786 = r126784 * r126785;
        double r126787 = sin(r126774);
        double r126788 = pow(r126787, r126775);
        double r126789 = r126786 / r126788;
        double r126790 = r126783 * r126789;
        double r126791 = r126780 * r126790;
        double r126792 = r126780 * r126791;
        double r126793 = r126772 * r126792;
        double r126794 = r126793 * r126785;
        double r126795 = r126777 * r126781;
        double r126796 = r126773 / r126795;
        double r126797 = pow(r126796, r126779);
        double r126798 = r126797 * r126786;
        double r126799 = r126780 * r126798;
        double r126800 = r126772 * r126799;
        double r126801 = r126800 * r126785;
        double r126802 = r126801 / r126788;
        double r126803 = r126771 ? r126794 : r126802;
        return r126803;
}

Error

Bits error versus t

Bits error versus l

Bits error versus k

Derivation

1. Split input into 2 regimes

2. if t < -3.0209864353103622e+180

   1. Initial program 56.7

      \[\frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) - 1\right)}\]

   2. Simplified 40.6

      \[\leadsto \color{blue}{\left(\frac{\frac{2}{{\left(\frac{k}{t}\right)}^{2} \cdot \tan k}}{{t}^{3} \cdot \sin k} \cdot \ell\right) \cdot \ell}\]

   3. Taylor expanded around inf 15.8

      \[\leadsto \color{blue}{\left(2 \cdot \left({\left(\frac{1}{{k}^{2} \cdot {t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right)} \cdot \ell\]
   4. Using strategy rm

   5. Applied sqr-pow 15.8

      \[\leadsto \left(2 \cdot \left({\left(\frac{1}{\color{blue}{\left({k}^{\left(\frac{2}{2}\right)} \cdot {k}^{\left(\frac{2}{2}\right)}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right) \cdot \ell\]

   6. Applied associate-*l* 15.7

      \[\leadsto \left(2 \cdot \left({\left(\frac{1}{\color{blue}{{k}^{\left(\frac{2}{2}\right)} \cdot \left({k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}\right)}}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right) \cdot \ell\]
   7. Using strategy rm

   8. Applied *-un-lft-identity 15.7

      \[\leadsto \left(2 \cdot \left({\left(\frac{\color{blue}{1 \cdot 1}}{{k}^{\left(\frac{2}{2}\right)} \cdot \left({k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}\right)}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right) \cdot \ell\]

   9. Applied times-frac 15.4

      \[\leadsto \left(2 \cdot \left({\color{blue}{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}} \cdot \frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right) \cdot \ell\]

   10. Applied unpow-prod-down 15.4

       \[\leadsto \left(2 \cdot \left(\color{blue}{\left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot {\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1}\right)} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right) \cdot \ell\]

   11. Applied associate-*l* 13.7

       \[\leadsto \left(2 \cdot \color{blue}{\left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right)}\right) \cdot \ell\]
   12. Using strategy rm

   13. Applied *-un-lft-identity 13.7

       \[\leadsto \left(2 \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{\color{blue}{1 \cdot 1}}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right)\right) \cdot \ell\]

   14. Applied times-frac 12.9

       \[\leadsto \left(2 \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\color{blue}{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}} \cdot \frac{1}{{t}^{1}}\right)}}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right)\right) \cdot \ell\]

   15. Applied unpow-prod-down 12.9

       \[\leadsto \left(2 \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left(\color{blue}{\left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot {\left(\frac{1}{{t}^{1}}\right)}^{1}\right)} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right)\right) \cdot \ell\]

   16. Applied associate-*l* 9.4

       \[\leadsto \left(2 \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \color{blue}{\left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{1}{{t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right)}\right)\right) \cdot \ell\]

   if -3.0209864353103622e+180 < t

   1. Initial program 46.7

      \[\frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) - 1\right)}\]

   2. Simplified 38.9

      \[\leadsto \color{blue}{\left(\frac{\frac{2}{{\left(\frac{k}{t}\right)}^{2} \cdot \tan k}}{{t}^{3} \cdot \sin k} \cdot \ell\right) \cdot \ell}\]

   3. Taylor expanded around inf 16.1

      \[\leadsto \color{blue}{\left(2 \cdot \left({\left(\frac{1}{{k}^{2} \cdot {t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right)} \cdot \ell\]
   4. Using strategy rm

   5. Applied sqr-pow 16.1

      \[\leadsto \left(2 \cdot \left({\left(\frac{1}{\color{blue}{\left({k}^{\left(\frac{2}{2}\right)} \cdot {k}^{\left(\frac{2}{2}\right)}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right) \cdot \ell\]

   6. Applied associate-*l* 12.8

      \[\leadsto \left(2 \cdot \left({\left(\frac{1}{\color{blue}{{k}^{\left(\frac{2}{2}\right)} \cdot \left({k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}\right)}}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right) \cdot \ell\]
   7. Using strategy rm

   8. Applied *-un-lft-identity 12.8

      \[\leadsto \left(2 \cdot \left({\left(\frac{\color{blue}{1 \cdot 1}}{{k}^{\left(\frac{2}{2}\right)} \cdot \left({k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}\right)}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right) \cdot \ell\]

   9. Applied times-frac 12.4

      \[\leadsto \left(2 \cdot \left({\color{blue}{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}} \cdot \frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right) \cdot \ell\]

   10. Applied unpow-prod-down 12.4

       \[\leadsto \left(2 \cdot \left(\color{blue}{\left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot {\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1}\right)} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right) \cdot \ell\]

   11. Applied associate-*l* 7.6

       \[\leadsto \left(2 \cdot \color{blue}{\left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right)}\right) \cdot \ell\]
   12. Using strategy rm

   13. Applied associate-*r/ 7.9

       \[\leadsto \left(2 \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \color{blue}{\frac{{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \left(\cos k \cdot \ell\right)}{{\left(\sin k\right)}^{2}}}\right)\right) \cdot \ell\]

   14. Applied associate-*r/ 7.9

       \[\leadsto \left(2 \cdot \color{blue}{\frac{{\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \left(\cos k \cdot \ell\right)\right)}{{\left(\sin k\right)}^{2}}}\right) \cdot \ell\]

   15. Applied associate-*r/ 7.9

       \[\leadsto \color{blue}{\frac{2 \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \left(\cos k \cdot \ell\right)\right)\right)}{{\left(\sin k\right)}^{2}}} \cdot \ell\]

   16. Applied associate-*l/ 7.8

       \[\leadsto \color{blue}{\frac{\left(2 \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \left(\cos k \cdot \ell\right)\right)\right)\right) \cdot \ell}{{\left(\sin k\right)}^{2}}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 8.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;t \le -3.02098643531036224 \cdot 10^{180}:\\ \;\;\;\;\left(2 \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{1}{{t}^{1}}\right)}^{1} \cdot \frac{\cos k \cdot \ell}{{\left(\sin k\right)}^{2}}\right)\right)\right)\right) \cdot \ell\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(2 \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)}}\right)}^{1} \cdot \left({\left(\frac{1}{{k}^{\left(\frac{2}{2}\right)} \cdot {t}^{1}}\right)}^{1} \cdot \left(\cos k \cdot \ell\right)\right)\right)\right) \cdot \ell}{{\left(\sin k\right)}^{2}}\\ \end{array}\]

Reproduce

herbie shell --seed 2020045 
(FPCore (t l k)
  :name "Toniolo and Linder, Equation (10-)"
  :precision binary64
  (/ 2 (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (- (+ 1 (pow (/ k t) 2)) 1))))