Average Error: 16.6 → 3.8
Time: 37.6s
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\]
↓
\[\log \left(e^{\cos^{-1} \left(\mathsf{fma}\left(\cos \phi_1 \cdot \cos \phi_2, \mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right), \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
↓
\log \left(e^{\cos^{-1} \left(\mathsf{fma}\left(\cos \phi_1 \cdot \cos \phi_2, \mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right), \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 r20791 = phi1;
        double r20792 = sin(r20791);
        double r20793 = phi2;
        double r20794 = sin(r20793);
        double r20795 = r20792 * r20794;
        double r20796 = cos(r20791);
        double r20797 = cos(r20793);
        double r20798 = r20796 * r20797;
        double r20799 = lambda1;
        double r20800 = lambda2;
        double r20801 = r20799 - r20800;
        double r20802 = cos(r20801);
        double r20803 = r20798 * r20802;
        double r20804 = r20795 + r20803;
        double r20805 = acos(r20804);
        double r20806 = R;
        double r20807 = r20805 * r20806;
        return r20807;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r20808 = phi1;
        double r20809 = cos(r20808);
        double r20810 = phi2;
        double r20811 = cos(r20810);
        double r20812 = r20809 * r20811;
        double r20813 = lambda2;
        double r20814 = cos(r20813);
        double r20815 = lambda1;
        double r20816 = cos(r20815);
        double r20817 = sin(r20815);
        double r20818 = sin(r20813);
        double r20819 = r20817 * r20818;
        double r20820 = fma(r20814, r20816, r20819);
        double r20821 = sin(r20808);
        double r20822 = sin(r20810);
        double r20823 = r20821 * r20822;
        double r20824 = fma(r20812, r20820, r20823);
        double r20825 = acos(r20824);
        double r20826 = exp(r20825);
        double r20827 = log(r20826);
        double r20828 = R;
        double r20829 = r20827 * r20828;
        return r20829;
}

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.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 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. Applied distribute-lft-in3.8

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

  6. Applied add-log-exp3.8

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

  7. Simplified3.8

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

  8. Final simplification3.8

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

Reproduce

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