Average Error: 16.7 → 3.8
Time: 51.1s
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(\cos \phi_2 \cdot \cos \phi_1, \mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right), \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 e^{\log \left(\frac{\pi}{2} - \sin^{-1} \left(\mathsf{fma}\left(\cos \phi_2 \cdot \cos \phi_1, \mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_1 \cdot \sin \lambda_2\right), \sin \phi_2 \cdot \sin \phi_1\right)\right)\right)}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r578404 = phi1;
        double r578405 = sin(r578404);
        double r578406 = phi2;
        double r578407 = sin(r578406);
        double r578408 = r578405 * r578407;
        double r578409 = cos(r578404);
        double r578410 = cos(r578406);
        double r578411 = r578409 * r578410;
        double r578412 = lambda1;
        double r578413 = lambda2;
        double r578414 = r578412 - r578413;
        double r578415 = cos(r578414);
        double r578416 = r578411 * r578415;
        double r578417 = r578408 + r578416;
        double r578418 = acos(r578417);
        double r578419 = R;
        double r578420 = r578418 * r578419;
        return r578420;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r578421 = R;
        double r578422 = atan2(1.0, 0.0);
        double r578423 = 2.0;
        double r578424 = r578422 / r578423;
        double r578425 = phi2;
        double r578426 = cos(r578425);
        double r578427 = phi1;
        double r578428 = cos(r578427);
        double r578429 = r578426 * r578428;
        double r578430 = lambda2;
        double r578431 = cos(r578430);
        double r578432 = lambda1;
        double r578433 = cos(r578432);
        double r578434 = sin(r578432);
        double r578435 = sin(r578430);
        double r578436 = r578434 * r578435;
        double r578437 = fma(r578431, r578433, r578436);
        double r578438 = sin(r578425);
        double r578439 = sin(r578427);
        double r578440 = r578438 * r578439;
        double r578441 = fma(r578429, r578437, r578440);
        double r578442 = asin(r578441);
        double r578443 = r578424 - r578442;
        double r578444 = log(r578443);
        double r578445 = exp(r578444);
        double r578446 = r578421 * r578445;
        return r578446;
}

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

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

    \[\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 acos-asin3.8

    \[\leadsto \color{blue}{\left(\frac{\pi}{2} - \sin^{-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 \left(\frac{\pi}{2} - \color{blue}{\sin^{-1} \left(\mathsf{fma}\left(\cos \phi_1 \cdot \cos \phi_2, \mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_2 \cdot \sin \lambda_1\right), \sin \phi_2 \cdot \sin \phi_1\right)\right)}\right) \cdot R\]
  7. Using strategy rm

  8. Applied add-exp-log3.8

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

  9. Final simplification3.8

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

Reproduce

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