Spherical law of cosines

Average Error: 16.7 → 4.2

Time: 56.3s

Precision: 64

Math

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

C

double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1595286 = phi1;
        double r1595287 = sin(r1595286);
        double r1595288 = phi2;
        double r1595289 = sin(r1595288);
        double r1595290 = r1595287 * r1595289;
        double r1595291 = cos(r1595286);
        double r1595292 = cos(r1595288);
        double r1595293 = r1595291 * r1595292;
        double r1595294 = lambda1;
        double r1595295 = lambda2;
        double r1595296 = r1595294 - r1595295;
        double r1595297 = cos(r1595296);
        double r1595298 = r1595293 * r1595297;
        double r1595299 = r1595290 + r1595298;
        double r1595300 = acos(r1595299);
        double r1595301 = R;
        double r1595302 = r1595300 * r1595301;
        return r1595302;
}

↓

double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r1595303 = R;
        double r1595304 = atan2(1.0, 0.0);
        double r1595305 = 2.0;
        double r1595306 = r1595304 / r1595305;
        double r1595307 = phi2;
        double r1595308 = sin(r1595307);
        double r1595309 = phi1;
        double r1595310 = sin(r1595309);
        double r1595311 = cos(r1595307);
        double r1595312 = cos(r1595309);
        double r1595313 = r1595311 * r1595312;
        double r1595314 = lambda1;
        double r1595315 = sin(r1595314);
        double r1595316 = lambda2;
        double r1595317 = sin(r1595316);
        double r1595318 = cos(r1595314);
        double r1595319 = cos(r1595316);
        double r1595320 = r1595318 * r1595319;
        double r1595321 = fma(r1595315, r1595317, r1595320);
        double r1595322 = r1595313 * r1595321;
        double r1595323 = fma(r1595308, r1595310, r1595322);
        double r1595324 = asin(r1595323);
        double r1595325 = r1595306 - r1595324;
        double r1595326 = r1595303 * r1595325;
        return r1595326;
}

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. Simplified 16.7

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

4. Applied cos-diff 4.1

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

6. Applied add-log-exp 4.1

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

7. Simplified 4.1

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

9. Applied acos-asin 4.2

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

10. Applied exp-diff 4.2

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

11. Applied log-div 4.2

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

12. Simplified 4.2

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

13. Simplified 4.2

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

15. Applied *-un-lft-identity 4.2

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

16. Applied associate-*r* 4.2

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

17. Simplified 4.2

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

18. Final simplification 4.2

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

Reproduce

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