Average Error: 16.9 → 3.7
Time: 44.2s
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(\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) \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(\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) \cdot R
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1150551 = phi1;
        double r1150552 = sin(r1150551);
        double r1150553 = phi2;
        double r1150554 = sin(r1150553);
        double r1150555 = r1150552 * r1150554;
        double r1150556 = cos(r1150551);
        double r1150557 = cos(r1150553);
        double r1150558 = r1150556 * r1150557;
        double r1150559 = lambda1;
        double r1150560 = lambda2;
        double r1150561 = r1150559 - r1150560;
        double r1150562 = cos(r1150561);
        double r1150563 = r1150558 * r1150562;
        double r1150564 = r1150555 + r1150563;
        double r1150565 = acos(r1150564);
        double r1150566 = R;
        double r1150567 = r1150565 * r1150566;
        return r1150567;
}
↓
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1150568 = phi2;
        double r1150569 = cos(r1150568);
        double r1150570 = phi1;
        double r1150571 = cos(r1150570);
        double r1150572 = r1150569 * r1150571;
        double r1150573 = lambda2;
        double r1150574 = cos(r1150573);
        double r1150575 = lambda1;
        double r1150576 = cos(r1150575);
        double r1150577 = sin(r1150573);
        double r1150578 = sin(r1150575);
        double r1150579 = r1150577 * r1150578;
        double r1150580 = fma(r1150574, r1150576, r1150579);
        double r1150581 = sin(r1150570);
        double r1150582 = sin(r1150568);
        double r1150583 = r1150581 * r1150582;
        double r1150584 = fma(r1150572, r1150580, r1150583);
        double r1150585 = acos(r1150584);
        double r1150586 = R;
        double r1150587 = r1150585 * r1150586;
        return r1150587;
}

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.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.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. Applied distribute-lft-in3.7

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

  6. Applied add-log-exp3.8

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

  8. Applied acos-asin3.8

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

  9. 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\]
  10. Using strategy rm

  11. Applied asin-acos3.7

    \[\leadsto \left(\frac{\pi}{2} - \color{blue}{\left(\frac{\pi}{2} - \cos^{-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)}\right) \cdot R\]

  12. Applied associate--r-3.7

    \[\leadsto \color{blue}{\left(\left(\frac{\pi}{2} - \frac{\pi}{2}\right) + \cos^{-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\]

  13. Simplified3.7

    \[\leadsto \left(\color{blue}{0} + \cos^{-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\]

  14. Final simplification3.7

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

Reproduce

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