Average Error: 16.5 → 4.0
Time: 1.2m
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 \cos^{-1} \left(\log \left(e^{(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left((\left(\sin \lambda_2\right) \cdot \left(\sin \lambda_1\right) + \left(\cos \lambda_1 \cdot \cos \lambda_2\right))_*\right) + \left(\sin \phi_2 \cdot \sin \phi_1\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 \cos^{-1} \left(\log \left(e^{(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left((\left(\sin \lambda_2\right) \cdot \left(\sin \lambda_1\right) + \left(\cos \lambda_1 \cdot \cos \lambda_2\right))_*\right) + \left(\sin \phi_2 \cdot \sin \phi_1\right))_*}\right)\right)
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1409739 = phi1;
        double r1409740 = sin(r1409739);
        double r1409741 = phi2;
        double r1409742 = sin(r1409741);
        double r1409743 = r1409740 * r1409742;
        double r1409744 = cos(r1409739);
        double r1409745 = cos(r1409741);
        double r1409746 = r1409744 * r1409745;
        double r1409747 = lambda1;
        double r1409748 = lambda2;
        double r1409749 = r1409747 - r1409748;
        double r1409750 = cos(r1409749);
        double r1409751 = r1409746 * r1409750;
        double r1409752 = r1409743 + r1409751;
        double r1409753 = acos(r1409752);
        double r1409754 = R;
        double r1409755 = r1409753 * r1409754;
        return r1409755;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1409756 = R;
        double r1409757 = phi1;
        double r1409758 = cos(r1409757);
        double r1409759 = phi2;
        double r1409760 = cos(r1409759);
        double r1409761 = r1409758 * r1409760;
        double r1409762 = lambda2;
        double r1409763 = sin(r1409762);
        double r1409764 = lambda1;
        double r1409765 = sin(r1409764);
        double r1409766 = cos(r1409764);
        double r1409767 = cos(r1409762);
        double r1409768 = r1409766 * r1409767;
        double r1409769 = fma(r1409763, r1409765, r1409768);
        double r1409770 = sin(r1409759);
        double r1409771 = sin(r1409757);
        double r1409772 = r1409770 * r1409771;
        double r1409773 = fma(r1409761, r1409769, r1409772);
        double r1409774 = exp(r1409773);
        double r1409775 = log(r1409774);
        double r1409776 = acos(r1409775);
        double r1409777 = r1409756 * r1409776;
        return r1409777;
}

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. Simplified16.5

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

  4. Applied cos-diff3.9

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

  5. Taylor expanded around -inf 3.9

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

  6. Simplified3.9

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

  8. Applied add-log-exp4.0

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

  9. Final simplification4.0

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

Reproduce

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