Spherical law of cosines

Average Error: 16.8 → 3.9

Time: 15.2s

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

↓

\[\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \frac{\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left({\left({\left(\cos \lambda_1\right)}^{2} \cdot {\left(\cos \lambda_2\right)}^{2}\right)}^{1} - \left(\sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right) \cdot \left(\sin \lambda_1 \cdot \sin \left(-\lambda_2\right)\right)\right)}{\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \left(-\lambda_2\right)}\right) \cdot R\]

C

double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r33858 = phi1;
        double r33859 = sin(r33858);
        double r33860 = phi2;
        double r33861 = sin(r33860);
        double r33862 = r33859 * r33861;
        double r33863 = cos(r33858);
        double r33864 = cos(r33860);
        double r33865 = r33863 * r33864;
        double r33866 = lambda1;
        double r33867 = lambda2;
        double r33868 = r33866 - r33867;
        double r33869 = cos(r33868);
        double r33870 = r33865 * r33869;
        double r33871 = r33862 + r33870;
        double r33872 = acos(r33871);
        double r33873 = R;
        double r33874 = r33872 * r33873;
        return r33874;
}

↓

double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
        double r33875 = phi1;
        double r33876 = sin(r33875);
        double r33877 = phi2;
        double r33878 = sin(r33877);
        double r33879 = r33876 * r33878;
        double r33880 = cos(r33875);
        double r33881 = cos(r33877);
        double r33882 = r33880 * r33881;
        double r33883 = lambda1;
        double r33884 = cos(r33883);
        double r33885 = 2.0;
        double r33886 = pow(r33884, r33885);
        double r33887 = lambda2;
        double r33888 = cos(r33887);
        double r33889 = pow(r33888, r33885);
        double r33890 = r33886 * r33889;
        double r33891 = 1.0;
        double r33892 = pow(r33890, r33891);
        double r33893 = sin(r33883);
        double r33894 = -r33887;
        double r33895 = sin(r33894);
        double r33896 = r33893 * r33895;
        double r33897 = r33896 * r33896;
        double r33898 = r33892 - r33897;
        double r33899 = r33882 * r33898;
        double r33900 = r33884 * r33888;
        double r33901 = r33900 + r33896;
        double r33902 = r33899 / r33901;
        double r33903 = r33879 + r33902;
        double r33904 = acos(r33903);
        double r33905 = R;
        double r33906 = r33904 * r33905;
        return r33906;
}

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

   \[\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-neg 16.8

   \[\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-sum 3.8

   \[\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. Simplified 3.8

   \[\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. Using strategy rm

7. Applied flip-- 3.8

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

8. Applied associate-*r/ 3.9

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

10. Applied pow1 3.9

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

11. Applied pow1 3.9

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

12. Applied pow-prod-down 3.9

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

13. Applied pow1 3.9

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

14. Applied pow1 3.9

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

15. Applied pow-prod-down 3.9

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

16. Applied pow-prod-down 3.9

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

17. Simplified 3.9

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

18. Final simplification 3.9

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

Reproduce

herbie shell --seed 2020062 
(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))