Average Error: 0.8 → 0.3
Time: 28.8s
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)}\]
↓
\[\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)}{\log \left(e^{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)}\right) + \log \left(e^{\sin \lambda_1 \cdot \sin \lambda_2}\right) \cdot \cos \phi_2}\]
\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)}
↓
\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)}{\log \left(e^{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)}\right) + \log \left(e^{\sin \lambda_1 \cdot \sin \lambda_2}\right) \cdot \cos \phi_2}
double f(double lambda1, double lambda2, double phi1, double phi2) {
        double r44781 = lambda1;
        double r44782 = phi2;
        double r44783 = cos(r44782);
        double r44784 = lambda2;
        double r44785 = r44781 - r44784;
        double r44786 = sin(r44785);
        double r44787 = r44783 * r44786;
        double r44788 = phi1;
        double r44789 = cos(r44788);
        double r44790 = cos(r44785);
        double r44791 = r44783 * r44790;
        double r44792 = r44789 + r44791;
        double r44793 = atan2(r44787, r44792);
        double r44794 = r44781 + r44793;
        return r44794;
}
↓
double f(double lambda1, double lambda2, double phi1, double phi2) {
        double r44795 = lambda1;
        double r44796 = phi2;
        double r44797 = cos(r44796);
        double r44798 = sin(r44795);
        double r44799 = lambda2;
        double r44800 = cos(r44799);
        double r44801 = r44798 * r44800;
        double r44802 = cos(r44795);
        double r44803 = sin(r44799);
        double r44804 = r44802 * r44803;
        double r44805 = r44801 - r44804;
        double r44806 = r44797 * r44805;
        double r44807 = r44800 * r44797;
        double r44808 = phi1;
        double r44809 = cos(r44808);
        double r44810 = fma(r44802, r44807, r44809);
        double r44811 = exp(r44810);
        double r44812 = log(r44811);
        double r44813 = r44798 * r44803;
        double r44814 = exp(r44813);
        double r44815 = log(r44814);
        double r44816 = r44815 * r44797;
        double r44817 = r44812 + r44816;
        double r44818 = atan2(r44806, r44817);
        double r44819 = r44795 + r44818;
        return r44819;
}

Error

Bits error versus lambda1

Bits error versus lambda2

Bits error versus phi1

Bits error versus phi2

Derivation

  1. Initial program 0.8

    \[\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 cos-diff0.8

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \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)}}\]

  4. Applied distribute-rgt-in0.8

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \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)}}\]

  5. Applied associate-+r+0.8

    \[\leadsto \lambda_1 + \tan^{-1}_* \frac{\cos \phi_2 \cdot \sin \left(\lambda_1 - \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}}\]

  6. Simplified0.8

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

  8. Applied sin-diff0.2

    \[\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)}}{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_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.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)}{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right) + \color{blue}{\log \left(e^{\sin \lambda_1 \cdot \sin \lambda_2}\right)} \cdot \cos \phi_2}\]
  11. Using strategy rm

  12. 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 \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)}\right)} + \log \left(e^{\sin \lambda_1 \cdot \sin \lambda_2}\right) \cdot \cos \phi_2}\]

  13. Final simplification0.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)}{\log \left(e^{\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2 \cdot \cos \phi_2, \cos \phi_1\right)}\right) + \log \left(e^{\sin \lambda_1 \cdot \sin \lambda_2}\right) \cdot \cos \phi_2}\]

Reproduce

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