Average Error: 16.9 → 3.8
Time: 32.4s
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\]
↓
\[\mathsf{log1p}\left(\log \left(e^{\mathsf{expm1}\left(\cos^{-1} \left(\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1, \cos \phi_2, \sin \phi_1 \cdot \sin \phi_2\right)\right)\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
↓
\mathsf{log1p}\left(\log \left(e^{\mathsf{expm1}\left(\cos^{-1} \left(\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1, \cos \phi_2, \sin \phi_1 \cdot \sin \phi_2\right)\right)\right)}\right)\right) \cdot R
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r22857 = phi1;
        double r22858 = sin(r22857);
        double r22859 = phi2;
        double r22860 = sin(r22859);
        double r22861 = r22858 * r22860;
        double r22862 = cos(r22857);
        double r22863 = cos(r22859);
        double r22864 = r22862 * r22863;
        double r22865 = lambda1;
        double r22866 = lambda2;
        double r22867 = r22865 - r22866;
        double r22868 = cos(r22867);
        double r22869 = r22864 * r22868;
        double r22870 = r22861 + r22869;
        double r22871 = acos(r22870);
        double r22872 = R;
        double r22873 = r22871 * r22872;
        return r22873;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r22874 = lambda2;
        double r22875 = cos(r22874);
        double r22876 = lambda1;
        double r22877 = cos(r22876);
        double r22878 = sin(r22876);
        double r22879 = sin(r22874);
        double r22880 = r22878 * r22879;
        double r22881 = fma(r22875, r22877, r22880);
        double r22882 = phi1;
        double r22883 = cos(r22882);
        double r22884 = r22881 * r22883;
        double r22885 = phi2;
        double r22886 = cos(r22885);
        double r22887 = sin(r22882);
        double r22888 = sin(r22885);
        double r22889 = r22887 * r22888;
        double r22890 = fma(r22884, r22886, r22889);
        double r22891 = acos(r22890);
        double r22892 = expm1(r22891);
        double r22893 = exp(r22892);
        double r22894 = log(r22893);
        double r22895 = log1p(r22894);
        double r22896 = R;
        double r22897 = r22895 * r22896;
        return r22897;
}

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.9

    \[\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.9

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

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

    \[\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 add-cbrt-cube3.8

    \[\leadsto \cos^{-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 \color{blue}{\sqrt[3]{\left(\sin \left(-\lambda_2\right) \cdot \sin \left(-\lambda_2\right)\right) \cdot \sin \left(-\lambda_2\right)}}\right)\right) \cdot R\]

  8. Applied add-cbrt-cube3.8

    \[\leadsto \cos^{-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 - \color{blue}{\sqrt[3]{\left(\sin \lambda_1 \cdot \sin \lambda_1\right) \cdot \sin \lambda_1}} \cdot \sqrt[3]{\left(\sin \left(-\lambda_2\right) \cdot \sin \left(-\lambda_2\right)\right) \cdot \sin \left(-\lambda_2\right)}\right)\right) \cdot R\]

  9. Applied cbrt-unprod3.8

    \[\leadsto \cos^{-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 - \color{blue}{\sqrt[3]{\left(\left(\sin \lambda_1 \cdot \sin \lambda_1\right) \cdot \sin \lambda_1\right) \cdot \left(\left(\sin \left(-\lambda_2\right) \cdot \sin \left(-\lambda_2\right)\right) \cdot \sin \left(-\lambda_2\right)\right)}}\right)\right) \cdot R\]

  10. Simplified3.8

    \[\leadsto \cos^{-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 - \sqrt[3]{\color{blue}{{\left(\sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}^{3}}}\right)\right) \cdot R\]
  11. Using strategy rm

  12. Applied log1p-expm1-u3.8

    \[\leadsto \color{blue}{\mathsf{log1p}\left(\mathsf{expm1}\left(\cos^{-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 - \sqrt[3]{{\left(\sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}^{3}}\right)\right)\right)\right)} \cdot R\]

  13. Simplified3.8

    \[\leadsto \mathsf{log1p}\left(\color{blue}{\mathsf{expm1}\left(\cos^{-1} \left(\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1, \cos \phi_2, \sin \phi_1 \cdot \sin \phi_2\right)\right)\right)}\right) \cdot R\]
  14. Using strategy rm

  15. Applied add-log-exp3.8

    \[\leadsto \mathsf{log1p}\left(\color{blue}{\log \left(e^{\mathsf{expm1}\left(\cos^{-1} \left(\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1, \cos \phi_2, \sin \phi_1 \cdot \sin \phi_2\right)\right)\right)}\right)}\right) \cdot R\]

  16. Final simplification3.8

    \[\leadsto \mathsf{log1p}\left(\log \left(e^{\mathsf{expm1}\left(\cos^{-1} \left(\mathsf{fma}\left(\mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_1, \cos \phi_2, \sin \phi_1 \cdot \sin \phi_2\right)\right)\right)}\right)\right) \cdot R\]

Reproduce

herbie shell --seed 2019305 +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))