Average Error: 16.6 → 3.9
Time: 14.3s
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\]
↓
\[\cos^{-1} \left(\log \left(e^{\sin \phi_1 \cdot \sin \phi_2}\right) + \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) \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
↓
\cos^{-1} \left(\log \left(e^{\sin \phi_1 \cdot \sin \phi_2}\right) + \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) \cdot R
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r26832 = phi1;
        double r26833 = sin(r26832);
        double r26834 = phi2;
        double r26835 = sin(r26834);
        double r26836 = r26833 * r26835;
        double r26837 = cos(r26832);
        double r26838 = cos(r26834);
        double r26839 = r26837 * r26838;
        double r26840 = lambda1;
        double r26841 = lambda2;
        double r26842 = r26840 - r26841;
        double r26843 = cos(r26842);
        double r26844 = r26839 * r26843;
        double r26845 = r26836 + r26844;
        double r26846 = acos(r26845);
        double r26847 = R;
        double r26848 = r26846 * r26847;
        return r26848;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r26849 = phi1;
        double r26850 = sin(r26849);
        double r26851 = phi2;
        double r26852 = sin(r26851);
        double r26853 = r26850 * r26852;
        double r26854 = exp(r26853);
        double r26855 = log(r26854);
        double r26856 = cos(r26849);
        double r26857 = cos(r26851);
        double r26858 = r26856 * r26857;
        double r26859 = lambda1;
        double r26860 = cos(r26859);
        double r26861 = lambda2;
        double r26862 = cos(r26861);
        double r26863 = r26860 * r26862;
        double r26864 = sin(r26859);
        double r26865 = -r26861;
        double r26866 = sin(r26865);
        double r26867 = r26864 * r26866;
        double r26868 = r26863 - r26867;
        double r26869 = r26858 * r26868;
        double r26870 = r26855 + r26869;
        double r26871 = acos(r26870);
        double r26872 = R;
        double r26873 = r26871 * r26872;
        return r26873;
}

Error

Bits error versus R

Bits error versus lambda1

Bits error versus lambda2

Bits error versus phi1

Bits error versus phi2

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 16.6

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

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

    \[\leadsto \cos^{-1} \left(\color{blue}{\log \left(e^{\sin \phi_1 \cdot \sin \phi_2}\right)} + \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) \cdot R\]

  8. Final simplification3.9

    \[\leadsto \cos^{-1} \left(\log \left(e^{\sin \phi_1 \cdot \sin \phi_2}\right) + \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) \cdot R\]

Reproduce

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