Average Error: 17.2 → 4.0
Time: 13.7s
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_1 \cdot \cos \lambda_2 - \sin \lambda_1 \cdot \sin \left(-\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
↓
\cos^{-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 \left(-\lambda_2\right)\right)\right) \cdot R
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r26621 = phi1;
        double r26622 = sin(r26621);
        double r26623 = phi2;
        double r26624 = sin(r26623);
        double r26625 = r26622 * r26624;
        double r26626 = cos(r26621);
        double r26627 = cos(r26623);
        double r26628 = r26626 * r26627;
        double r26629 = lambda1;
        double r26630 = lambda2;
        double r26631 = r26629 - r26630;
        double r26632 = cos(r26631);
        double r26633 = r26628 * r26632;
        double r26634 = r26625 + r26633;
        double r26635 = acos(r26634);
        double r26636 = R;
        double r26637 = r26635 * r26636;
        return r26637;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r26638 = phi1;
        double r26639 = sin(r26638);
        double r26640 = phi2;
        double r26641 = sin(r26640);
        double r26642 = r26639 * r26641;
        double r26643 = cos(r26638);
        double r26644 = cos(r26640);
        double r26645 = r26643 * r26644;
        double r26646 = lambda1;
        double r26647 = cos(r26646);
        double r26648 = lambda2;
        double r26649 = cos(r26648);
        double r26650 = r26647 * r26649;
        double r26651 = sin(r26646);
        double r26652 = -r26648;
        double r26653 = sin(r26652);
        double r26654 = r26651 * r26653;
        double r26655 = r26650 - r26654;
        double r26656 = r26645 * r26655;
        double r26657 = r26642 + r26656;
        double r26658 = acos(r26657);
        double r26659 = R;
        double r26660 = r26658 * r26659;
        return r26660;
}

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

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

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

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

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

  6. Final simplification4.0

    \[\leadsto \cos^{-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 \left(-\lambda_2\right)\right)\right) \cdot R\]

Reproduce

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