Average Error: 16.9 → 4.0
Time: 14.5s
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\]
↓
\[\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\]
\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
↓
\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
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r32575 = phi1;
        double r32576 = sin(r32575);
        double r32577 = phi2;
        double r32578 = sin(r32577);
        double r32579 = r32576 * r32578;
        double r32580 = cos(r32575);
        double r32581 = cos(r32577);
        double r32582 = r32580 * r32581;
        double r32583 = lambda1;
        double r32584 = lambda2;
        double r32585 = r32583 - r32584;
        double r32586 = cos(r32585);
        double r32587 = r32582 * r32586;
        double r32588 = r32579 + r32587;
        double r32589 = acos(r32588);
        double r32590 = R;
        double r32591 = r32589 * r32590;
        return r32591;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r32592 = atan2(1.0, 0.0);
        double r32593 = 2.0;
        double r32594 = r32592 / r32593;
        double r32595 = phi1;
        double r32596 = sin(r32595);
        double r32597 = phi2;
        double r32598 = sin(r32597);
        double r32599 = r32596 * r32598;
        double r32600 = cos(r32595);
        double r32601 = cos(r32597);
        double r32602 = r32600 * r32601;
        double r32603 = lambda1;
        double r32604 = cos(r32603);
        double r32605 = lambda2;
        double r32606 = cos(r32605);
        double r32607 = r32604 * r32606;
        double r32608 = sin(r32603);
        double r32609 = sin(r32605);
        double r32610 = r32608 * r32609;
        double r32611 = r32607 + r32610;
        double r32612 = r32602 * r32611;
        double r32613 = r32599 + r32612;
        double r32614 = asin(r32613);
        double r32615 = r32594 - r32614;
        double r32616 = R;
        double r32617 = r32615 * r32616;
        return r32617;
}

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 16.9

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

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

    \[\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. Final simplification4.0

    \[\leadsto \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\]

Reproduce

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