Average Error: 16.8 → 3.9
Time: 52.0s
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\]
↓
\[R \cdot e^{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\mathsf{fma}\left(\left(\sin \phi_2\right), \left(\sin \phi_1\right), \left(\mathsf{fma}\left(\left(\cos \lambda_2\right), \left(\cos \lambda_1\right), \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)\right)\right)\right)\right)}\]
\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
↓
R \cdot e^{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\mathsf{fma}\left(\left(\sin \phi_2\right), \left(\sin \phi_1\right), \left(\mathsf{fma}\left(\left(\cos \lambda_2\right), \left(\cos \lambda_1\right), \left(\sin \lambda_1 \cdot \sin \lambda_2\right)\right) \cdot \left(\cos \phi_1 \cdot \cos \phi_2\right)\right)\right)\right)\right)}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1003779 = phi1;
        double r1003780 = sin(r1003779);
        double r1003781 = phi2;
        double r1003782 = sin(r1003781);
        double r1003783 = r1003780 * r1003782;
        double r1003784 = cos(r1003779);
        double r1003785 = cos(r1003781);
        double r1003786 = r1003784 * r1003785;
        double r1003787 = lambda1;
        double r1003788 = lambda2;
        double r1003789 = r1003787 - r1003788;
        double r1003790 = cos(r1003789);
        double r1003791 = r1003786 * r1003790;
        double r1003792 = r1003783 + r1003791;
        double r1003793 = acos(r1003792);
        double r1003794 = R;
        double r1003795 = r1003793 * r1003794;
        return r1003795;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1003796 = R;
        double r1003797 = atan2(1.0, 0.0);
        double r1003798 = 2.0;
        double r1003799 = r1003797 / r1003798;
        double r1003800 = phi2;
        double r1003801 = sin(r1003800);
        double r1003802 = phi1;
        double r1003803 = sin(r1003802);
        double r1003804 = lambda2;
        double r1003805 = cos(r1003804);
        double r1003806 = lambda1;
        double r1003807 = cos(r1003806);
        double r1003808 = sin(r1003806);
        double r1003809 = sin(r1003804);
        double r1003810 = r1003808 * r1003809;
        double r1003811 = fma(r1003805, r1003807, r1003810);
        double r1003812 = cos(r1003802);
        double r1003813 = cos(r1003800);
        double r1003814 = r1003812 * r1003813;
        double r1003815 = r1003811 * r1003814;
        double r1003816 = fma(r1003801, r1003803, r1003815);
        double r1003817 = asin(r1003816);
        double r1003818 = r1003799 - r1003817;
        double r1003819 = log(r1003818);
        double r1003820 = exp(r1003819);
        double r1003821 = r1003796 * r1003820;
        return r1003821;
}

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

    \[\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 cos-diff3.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 \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)}\right) \cdot R\]
  4. Using strategy rm

  5. Applied add-exp-log3.8

    \[\leadsto \color{blue}{e^{\log \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 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)\right)}} \cdot R\]

  6. Simplified3.8

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

  8. Applied acos-asin3.9

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

  9. Final simplification3.9

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

Reproduce

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