Average Error: 16.5 → 3.6
Time: 42.1s
Precision: 64
\[\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R\]
↓
\[\left(\frac{\pi}{2} - \sin^{-1} \left(\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right), \cos \phi_1 \cdot \cos \phi_2, \sin \phi_1 \cdot \sin \phi_2\right)\right)\right) \cdot R\]
\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R
↓
\left(\frac{\pi}{2} - \sin^{-1} \left(\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right), \cos \phi_1 \cdot \cos \phi_2, \sin \phi_1 \cdot \sin \phi_2\right)\right)\right) \cdot R
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r23834 = phi1;
        double r23835 = sin(r23834);
        double r23836 = phi2;
        double r23837 = sin(r23836);
        double r23838 = r23835 * r23837;
        double r23839 = cos(r23834);
        double r23840 = cos(r23836);
        double r23841 = r23839 * r23840;
        double r23842 = lambda1;
        double r23843 = lambda2;
        double r23844 = r23842 - r23843;
        double r23845 = cos(r23844);
        double r23846 = r23841 * r23845;
        double r23847 = r23838 + r23846;
        double r23848 = acos(r23847);
        double r23849 = R;
        double r23850 = r23848 * r23849;
        return r23850;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r23851 = atan2(1.0, 0.0);
        double r23852 = 2.0;
        double r23853 = r23851 / r23852;
        double r23854 = lambda1;
        double r23855 = cos(r23854);
        double r23856 = lambda2;
        double r23857 = cos(r23856);
        double r23858 = sin(r23854);
        double r23859 = sin(r23856);
        double r23860 = r23858 * r23859;
        double r23861 = fma(r23855, r23857, r23860);
        double r23862 = phi1;
        double r23863 = cos(r23862);
        double r23864 = phi2;
        double r23865 = cos(r23864);
        double r23866 = r23863 * r23865;
        double r23867 = sin(r23862);
        double r23868 = sin(r23864);
        double r23869 = r23867 * r23868;
        double r23870 = fma(r23861, r23866, r23869);
        double r23871 = asin(r23870);
        double r23872 = r23853 - r23871;
        double r23873 = R;
        double r23874 = r23872 * r23873;
        return r23874;
}

Error

Bits error versus R

Bits error versus lambda1

Bits error versus lambda2

Bits error versus phi1

Bits error versus phi2

Derivation

  1. Initial program 16.5

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

  3. Applied sub-neg16.5

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

  4. Applied cos-sum3.6

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

  5. Simplified3.6

    \[\leadsto \cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\color{blue}{\cos \lambda_1 \cdot \cos \lambda_2} - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right) \cdot R\]
  6. Using strategy rm

  7. Applied acos-asin3.6

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

  8. Simplified3.6

    \[\leadsto \left(\frac{\pi}{2} - \color{blue}{\sin^{-1} \left(\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right), \cos \phi_1 \cdot \cos \phi_2, \sin \phi_1 \cdot \sin \phi_2\right)\right)}\right) \cdot R\]

  9. Final simplification3.6

    \[\leadsto \left(\frac{\pi}{2} - \sin^{-1} \left(\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_1, \cos \lambda_2, \sin \lambda_1 \cdot \sin \lambda_2\right), \cos \phi_1 \cdot \cos \phi_2, \sin \phi_1 \cdot \sin \phi_2\right)\right)\right) \cdot R\]

Reproduce

herbie shell --seed 2019303 +o rules:numerics
(FPCore (R lambda1 lambda2 phi1 phi2)
  :name "Spherical law of cosines"
  :precision binary64
  (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R))