Average Error: 0.9 → 0.3
Time: 28.6s
Precision: 64
\[\lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 + \cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}\]
↓
\[\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\frac{\log \left(e^{\mathsf{fma}\left(\cos \lambda_1 \cdot \cos \phi_2, \cos \lambda_2, \cos \phi_1\right)}\right) \cdot \log \left(e^{\mathsf{fma}\left(\cos \lambda_1 \cdot \cos \phi_2, \cos \lambda_2, \cos \phi_1\right)}\right) - \left(\left(\sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \phi_2\right) \cdot \left(\left(\sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \phi_2\right)}{\log \left(e^{\mathsf{fma}\left(\cos \lambda_1 \cdot \cos \phi_2, \cos \lambda_2, \cos \phi_1\right)}\right) - \left(\sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \phi_2}} + \lambda_1\]
\lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 + \cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}
↓
\tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\frac{\log \left(e^{\mathsf{fma}\left(\cos \lambda_1 \cdot \cos \phi_2, \cos \lambda_2, \cos \phi_1\right)}\right) \cdot \log \left(e^{\mathsf{fma}\left(\cos \lambda_1 \cdot \cos \phi_2, \cos \lambda_2, \cos \phi_1\right)}\right) - \left(\left(\sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \phi_2\right) \cdot \left(\left(\sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \phi_2\right)}{\log \left(e^{\mathsf{fma}\left(\cos \lambda_1 \cdot \cos \phi_2, \cos \lambda_2, \cos \phi_1\right)}\right) - \left(\sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \phi_2}} + \lambda_1
double f(double lambda1, double lambda2, double phi1, double phi2) {
        double r2005681 = lambda1;
        double r2005682 = phi2;
        double r2005683 = cos(r2005682);
        double r2005684 = lambda2;
        double r2005685 = r2005681 - r2005684;
        double r2005686 = sin(r2005685);
        double r2005687 = r2005683 * r2005686;
        double r2005688 = phi1;
        double r2005689 = cos(r2005688);
        double r2005690 = cos(r2005685);
        double r2005691 = r2005683 * r2005690;
        double r2005692 = r2005689 + r2005691;
        double r2005693 = atan2(r2005687, r2005692);
        double r2005694 = r2005681 + r2005693;
        return r2005694;
}
↓
double f(double lambda1, double lambda2, double phi1, double phi2) {
        double r2005695 = phi2;
        double r2005696 = cos(r2005695);
        double r2005697 = lambda1;
        double r2005698 = sin(r2005697);
        double r2005699 = lambda2;
        double r2005700 = cos(r2005699);
        double r2005701 = r2005698 * r2005700;
        double r2005702 = cos(r2005697);
        double r2005703 = sin(r2005699);
        double r2005704 = r2005702 * r2005703;
        double r2005705 = r2005701 - r2005704;
        double r2005706 = r2005696 * r2005705;
        double r2005707 = r2005702 * r2005696;
        double r2005708 = phi1;
        double r2005709 = cos(r2005708);
        double r2005710 = fma(r2005707, r2005700, r2005709);
        double r2005711 = exp(r2005710);
        double r2005712 = log(r2005711);
        double r2005713 = r2005712 * r2005712;
        double r2005714 = r2005703 * r2005698;
        double r2005715 = r2005714 * r2005696;
        double r2005716 = r2005715 * r2005715;
        double r2005717 = r2005713 - r2005716;
        double r2005718 = r2005712 - r2005715;
        double r2005719 = r2005717 / r2005718;
        double r2005720 = atan2(r2005706, r2005719);
        double r2005721 = r2005720 + r2005697;
        return r2005721;
}

Error

Bits error versus lambda1

Bits error versus lambda2

Bits error versus phi1

Bits error versus phi2

Derivation

  1. Initial program 0.9

    \[\lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \lambda_2\right)}{\cos \phi_1 + \cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}\]
  2. Using strategy rm

  3. Applied sin-diff0.9

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \color{blue}{\left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}}{\cos \phi_1 + \cos \phi_2 \cdot \cos \left(\lambda_1 - \lambda_2\right)}\]
  4. Using strategy rm

  5. Applied cos-diff0.2

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\cos \phi_1 + \cos \phi_2 \cdot \color{blue}{\left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)}}\]

  6. Applied distribute-rgt-in0.2

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\cos \phi_1 + \color{blue}{\left(\left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \cos \phi_2 + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2\right)}}\]

  7. Applied associate-+r+0.2

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\left(\cos \phi_1 + \left(\cos \lambda_1 \cdot \cos \lambda_2\right) \cdot \cos \phi_2\right) + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2}}\]

  8. Simplified0.2

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\mathsf{fma}\left(\cos \phi_2 \cdot \cos \lambda_1, \cos \lambda_2, \cos \phi_1\right)} + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2}\]
  9. Using strategy rm

  10. Applied add-log-exp0.3

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\log \left(e^{\mathsf{fma}\left(\cos \phi_2 \cdot \cos \lambda_1, \cos \lambda_2, \cos \phi_1\right)}\right)} + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2}\]
  11. Using strategy rm

  12. Applied flip-+0.3

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\color{blue}{\frac{\log \left(e^{\mathsf{fma}\left(\cos \phi_2 \cdot \cos \lambda_1, \cos \lambda_2, \cos \phi_1\right)}\right) \cdot \log \left(e^{\mathsf{fma}\left(\cos \phi_2 \cdot \cos \lambda_1, \cos \lambda_2, \cos \phi_1\right)}\right) - \left(\left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2\right) \cdot \left(\left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2\right)}{\log \left(e^{\mathsf{fma}\left(\cos \phi_2 \cdot \cos \lambda_1, \cos \lambda_2, \cos \phi_1\right)}\right) - \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2}}}\]

  13. Final simplification0.3

    \[\leadsto \tan^{-1}_* \frac{\cos \phi_2 \cdot \left(\sin \lambda_1 \cdot \cos \lambda_2 - \cos \lambda_1 \cdot \sin \lambda_2\right)}{\frac{\log \left(e^{\mathsf{fma}\left(\cos \lambda_1 \cdot \cos \phi_2, \cos \lambda_2, \cos \phi_1\right)}\right) \cdot \log \left(e^{\mathsf{fma}\left(\cos \lambda_1 \cdot \cos \phi_2, \cos \lambda_2, \cos \phi_1\right)}\right) - \left(\left(\sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \phi_2\right) \cdot \left(\left(\sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \phi_2\right)}{\log \left(e^{\mathsf{fma}\left(\cos \lambda_1 \cdot \cos \phi_2, \cos \lambda_2, \cos \phi_1\right)}\right) - \left(\sin \lambda_2 \cdot \sin \lambda_1\right) \cdot \cos \phi_2}} + \lambda_1\]

Reproduce

herbie shell --seed 2019192 +o rules:numerics
(FPCore (lambda1 lambda2 phi1 phi2)
  :name "Midpoint on a great circle"
  (+ lambda1 (atan2 (* (cos phi2) (sin (- lambda1 lambda2))) (+ (cos phi1) (* (cos phi2) (cos (- lambda1 lambda2)))))))