Average Error: 17.1 → 4.1
Time: 3.5m
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\]
↓
\[\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \log \left(e^{\sin \lambda_1 \cdot \sin \left(-\lambda_2\right)}\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
↓
\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1 - \log \left(e^{\sin \lambda_1 \cdot \sin \left(-\lambda_2\right)}\right)\right)\right) \cdot R
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r23551 = phi1;
        double r23552 = sin(r23551);
        double r23553 = phi2;
        double r23554 = sin(r23553);
        double r23555 = r23552 * r23554;
        double r23556 = cos(r23551);
        double r23557 = cos(r23553);
        double r23558 = r23556 * r23557;
        double r23559 = lambda1;
        double r23560 = lambda2;
        double r23561 = r23559 - r23560;
        double r23562 = cos(r23561);
        double r23563 = r23558 * r23562;
        double r23564 = r23555 + r23563;
        double r23565 = acos(r23564);
        double r23566 = R;
        double r23567 = r23565 * r23566;
        return r23567;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r23568 = phi1;
        double r23569 = sin(r23568);
        double r23570 = phi2;
        double r23571 = sin(r23570);
        double r23572 = r23569 * r23571;
        double r23573 = cos(r23568);
        double r23574 = cos(r23570);
        double r23575 = r23573 * r23574;
        double r23576 = lambda2;
        double r23577 = cos(r23576);
        double r23578 = lambda1;
        double r23579 = cos(r23578);
        double r23580 = r23577 * r23579;
        double r23581 = sin(r23578);
        double r23582 = -r23576;
        double r23583 = sin(r23582);
        double r23584 = r23581 * r23583;
        double r23585 = exp(r23584);
        double r23586 = log(r23585);
        double r23587 = r23580 - r23586;
        double r23588 = r23575 * r23587;
        double r23589 = r23572 + r23588;
        double r23590 = acos(r23589);
        double r23591 = R;
        double r23592 = r23590 * r23591;
        return r23592;
}

Error

Bits error versus R

Bits error versus lambda1

Bits error versus lambda2

Bits error versus phi1

Bits error versus phi2

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 17.1

    \[\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 sub-neg17.1

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

  4. Applied cos-sum4.1

    \[\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 \left(-\lambda_2\right) - \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)}\right) \cdot R\]

  5. Simplified4.1

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

  7. Applied add-log-exp4.1

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

  8. Final simplification4.1

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

Reproduce

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