Bearing on a great circle

Average Error: 13.6 → 0.2

Time: 27.0s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

\[\tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\]

↓

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

C

double f(double lambda1, double lambda2, double phi1, double phi2) {
        double r126389 = lambda1;
        double r126390 = lambda2;
        double r126391 = r126389 - r126390;
        double r126392 = sin(r126391);
        double r126393 = phi2;
        double r126394 = cos(r126393);
        double r126395 = r126392 * r126394;
        double r126396 = phi1;
        double r126397 = cos(r126396);
        double r126398 = sin(r126393);
        double r126399 = r126397 * r126398;
        double r126400 = sin(r126396);
        double r126401 = r126400 * r126394;
        double r126402 = cos(r126391);
        double r126403 = r126401 * r126402;
        double r126404 = r126399 - r126403;
        double r126405 = atan2(r126395, r126404);
        return r126405;
}

↓

double f(double lambda1, double lambda2, double phi1, double phi2) {
        double r126406 = lambda1;
        double r126407 = sin(r126406);
        double r126408 = lambda2;
        double r126409 = cos(r126408);
        double r126410 = r126407 * r126409;
        double r126411 = cos(r126406);
        double r126412 = -r126408;
        double r126413 = sin(r126412);
        double r126414 = r126411 * r126413;
        double r126415 = r126410 + r126414;
        double r126416 = phi2;
        double r126417 = cos(r126416);
        double r126418 = r126415 * r126417;
        double r126419 = phi1;
        double r126420 = cos(r126419);
        double r126421 = sin(r126416);
        double r126422 = r126420 * r126421;
        double r126423 = r126409 * r126411;
        double r126424 = r126423 * r126423;
        double r126425 = 2.0;
        double r126426 = pow(r126407, r126425);
        double r126427 = sin(r126408);
        double r126428 = pow(r126427, r126425);
        double r126429 = r126426 * r126428;
        double r126430 = r126424 - r126429;
        double r126431 = sin(r126419);
        double r126432 = r126431 * r126417;
        double r126433 = r126430 * r126432;
        double r126434 = r126407 * r126427;
        double r126435 = r126423 - r126434;
        double r126436 = r126433 / r126435;
        double r126437 = r126422 - r126436;
        double r126438 = atan2(r126418, r126437);
        return r126438;
}

Error

Bits error versus lambda1

Bits error versus lambda2

Bits error versus phi1

Bits error versus phi2

Derivation

1. Initial program 13.6

   \[\tan^{-1}_* \frac{\sin \left(\lambda_1 - \lambda_2\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\sin \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)}\]
2. Using strategy rm

3. Applied sub-neg 13.6

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

4. Applied sin-sum 6.9

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

5. Simplified 6.9

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

7. Applied cos-diff 0.2

   \[\leadsto \tan^{-1}_* \frac{\left(\sin \lambda_1 \cdot \cos \lambda_2 + \cos \lambda_1 \cdot \sin \left(-\lambda_2\right)\right) \cdot \cos \phi_2}{\cos \phi_1 \cdot \sin \phi_2 - \left(\sin \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)}}\]

8. Simplified 0.2

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

10. Applied flip-+ 0.2

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

11. Applied associate-*r/ 0.2

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

13. Applied pow1 0.2

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

14. Applied pow1 0.2

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

15. Applied pow-prod-down 0.2

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

16. Applied pow1 0.2

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

17. Applied pow1 0.2

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

18. Applied pow-prod-down 0.2

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

19. Applied pow-prod-down 0.2

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

20. Simplified 0.2

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

21. Final simplification 0.2

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

Reproduce

herbie shell --seed 2020043 
(FPCore (lambda1 lambda2 phi1 phi2)
  :name "Bearing on a great circle"
  :precision binary64
  (atan2 (* (sin (- lambda1 lambda2)) (cos phi2)) (- (* (cos phi1) (sin phi2)) (* (* (sin phi1) (cos phi2)) (cos (- lambda1 lambda2))))))