Average Error: 17.3 → 4.0
Time: 48.9s
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 \log \left(\frac{\sqrt{e^{\pi}}}{e^{\sin^{-1} \left(\mathsf{fma}\left(\left(\cos \phi_2\right), \left(\mathsf{fma}\left(\left(\sin \lambda_1\right), \left(\sin \lambda_2\right), \left(\cos \lambda_2 \cdot \cos \lambda_1\right)\right) \cdot \cos \phi_1\right), \left(\sin \phi_1 \cdot \sin \phi_2\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 \log \left(\frac{\sqrt{e^{\pi}}}{e^{\sin^{-1} \left(\mathsf{fma}\left(\left(\cos \phi_2\right), \left(\mathsf{fma}\left(\left(\sin \lambda_1\right), \left(\sin \lambda_2\right), \left(\cos \lambda_2 \cdot \cos \lambda_1\right)\right) \cdot \cos \phi_1\right), \left(\sin \phi_1 \cdot \sin \phi_2\right)\right)\right)}}\right)
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1047325 = phi1;
        double r1047326 = sin(r1047325);
        double r1047327 = phi2;
        double r1047328 = sin(r1047327);
        double r1047329 = r1047326 * r1047328;
        double r1047330 = cos(r1047325);
        double r1047331 = cos(r1047327);
        double r1047332 = r1047330 * r1047331;
        double r1047333 = lambda1;
        double r1047334 = lambda2;
        double r1047335 = r1047333 - r1047334;
        double r1047336 = cos(r1047335);
        double r1047337 = r1047332 * r1047336;
        double r1047338 = r1047329 + r1047337;
        double r1047339 = acos(r1047338);
        double r1047340 = R;
        double r1047341 = r1047339 * r1047340;
        return r1047341;
}

double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1047342 = R;
        double r1047343 = atan2(1.0, 0.0);
        double r1047344 = exp(r1047343);
        double r1047345 = sqrt(r1047344);
        double r1047346 = phi2;
        double r1047347 = cos(r1047346);
        double r1047348 = lambda1;
        double r1047349 = sin(r1047348);
        double r1047350 = lambda2;
        double r1047351 = sin(r1047350);
        double r1047352 = cos(r1047350);
        double r1047353 = cos(r1047348);
        double r1047354 = r1047352 * r1047353;
        double r1047355 = fma(r1047349, r1047351, r1047354);
        double r1047356 = phi1;
        double r1047357 = cos(r1047356);
        double r1047358 = r1047355 * r1047357;
        double r1047359 = sin(r1047356);
        double r1047360 = sin(r1047346);
        double r1047361 = r1047359 * r1047360;
        double r1047362 = fma(r1047347, r1047358, r1047361);
        double r1047363 = asin(r1047362);
        double r1047364 = exp(r1047363);
        double r1047365 = r1047345 / r1047364;
        double r1047366 = log(r1047365);
        double r1047367 = r1047342 * r1047366;
        return r1047367;
}

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 17.3

    \[\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. Simplified17.3

    \[\leadsto \color{blue}{R \cdot \cos^{-1} \left(\mathsf{fma}\left(\left(\cos \phi_1 \cdot \cos \phi_2\right), \left(\cos \left(\lambda_1 - \lambda_2\right)\right), \left(\sin \phi_2 \cdot \sin \phi_1\right)\right)\right)}\]
  3. Using strategy rm
  4. Applied cos-diff3.8

    \[\leadsto R \cdot \cos^{-1} \left(\mathsf{fma}\left(\left(\cos \phi_1 \cdot \cos \phi_2\right), \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)\right)\]
  5. Using strategy rm
  6. Applied add-log-exp3.9

    \[\leadsto R \cdot \color{blue}{\log \left(e^{\cos^{-1} \left(\mathsf{fma}\left(\left(\cos \phi_1 \cdot \cos \phi_2\right), \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)\right)}\right)}\]
  7. Simplified3.9

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

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

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

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

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

Reproduce

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