Average Error: 16.7 → 3.8
Time: 55.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 \log \left(\frac{\sqrt{e^{\pi}}}{e^{\sin^{-1} \left(\mathsf{fma}\left(\cos \phi_2 \cdot \cos \phi_1, \mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_2 \cdot \sin \lambda_1\right), \sin \phi_1 \cdot \sin \phi_2\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(\cos \phi_2 \cdot \cos \phi_1, \mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_2 \cdot \sin \lambda_1\right), \sin \phi_1 \cdot \sin \phi_2\right)\right)}}\right)
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1378661 = phi1;
        double r1378662 = sin(r1378661);
        double r1378663 = phi2;
        double r1378664 = sin(r1378663);
        double r1378665 = r1378662 * r1378664;
        double r1378666 = cos(r1378661);
        double r1378667 = cos(r1378663);
        double r1378668 = r1378666 * r1378667;
        double r1378669 = lambda1;
        double r1378670 = lambda2;
        double r1378671 = r1378669 - r1378670;
        double r1378672 = cos(r1378671);
        double r1378673 = r1378668 * r1378672;
        double r1378674 = r1378665 + r1378673;
        double r1378675 = acos(r1378674);
        double r1378676 = R;
        double r1378677 = r1378675 * r1378676;
        return r1378677;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1378678 = R;
        double r1378679 = atan2(1.0, 0.0);
        double r1378680 = exp(r1378679);
        double r1378681 = sqrt(r1378680);
        double r1378682 = phi2;
        double r1378683 = cos(r1378682);
        double r1378684 = phi1;
        double r1378685 = cos(r1378684);
        double r1378686 = r1378683 * r1378685;
        double r1378687 = lambda2;
        double r1378688 = cos(r1378687);
        double r1378689 = lambda1;
        double r1378690 = cos(r1378689);
        double r1378691 = sin(r1378687);
        double r1378692 = sin(r1378689);
        double r1378693 = r1378691 * r1378692;
        double r1378694 = fma(r1378688, r1378690, r1378693);
        double r1378695 = sin(r1378684);
        double r1378696 = sin(r1378682);
        double r1378697 = r1378695 * r1378696;
        double r1378698 = fma(r1378686, r1378694, r1378697);
        double r1378699 = asin(r1378698);
        double r1378700 = exp(r1378699);
        double r1378701 = r1378681 / r1378700;
        double r1378702 = log(r1378701);
        double r1378703 = r1378678 * r1378702;
        return r1378703;
}

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 add-log-exp3.7

    \[\leadsto \color{blue}{\log \left(e^{\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 \lambda_2\right)\right)}\right)} \cdot R\]

  6. Simplified3.7

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

  8. Applied acos-asin3.8

    \[\leadsto \log \left(e^{\color{blue}{\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_1 \cdot \sin \lambda_2\right), \sin \phi_1 \cdot \sin \phi_2\right)\right)}}\right) \cdot R\]

  9. Applied exp-diff3.8

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

  10. Simplified3.8

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

  11. Final simplification3.8

    \[\leadsto R \cdot \log \left(\frac{\sqrt{e^{\pi}}}{e^{\sin^{-1} \left(\mathsf{fma}\left(\cos \phi_2 \cdot \cos \phi_1, \mathsf{fma}\left(\cos \lambda_2, \cos \lambda_1, \sin \lambda_2 \cdot \sin \lambda_1\right), \sin \phi_1 \cdot \sin \phi_2\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))