Midpoint on a great circle

Average Error: 0.8 → 0.3

Time: 17.4s

Precision: 64

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

Math

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

↓

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

C

double f(double lambda1, double lambda2, double phi1, double phi2) {
        double r53226 = lambda1;
        double r53227 = phi2;
        double r53228 = cos(r53227);
        double r53229 = lambda2;
        double r53230 = r53226 - r53229;
        double r53231 = sin(r53230);
        double r53232 = r53228 * r53231;
        double r53233 = phi1;
        double r53234 = cos(r53233);
        double r53235 = cos(r53230);
        double r53236 = r53228 * r53235;
        double r53237 = r53234 + r53236;
        double r53238 = atan2(r53232, r53237);
        double r53239 = r53226 + r53238;
        return r53239;
}

↓

double f(double lambda1, double lambda2, double phi1, double phi2) {
        double r53240 = lambda1;
        double r53241 = phi2;
        double r53242 = cos(r53241);
        double r53243 = sin(r53240);
        double r53244 = lambda2;
        double r53245 = cos(r53244);
        double r53246 = r53243 * r53245;
        double r53247 = cos(r53240);
        double r53248 = -r53244;
        double r53249 = sin(r53248);
        double r53250 = r53247 * r53249;
        double r53251 = r53246 + r53250;
        double r53252 = r53242 * r53251;
        double r53253 = r53242 * r53245;
        double r53254 = r53247 * r53253;
        double r53255 = phi1;
        double r53256 = cos(r53255);
        double r53257 = r53254 - r53256;
        double r53258 = r53254 * r53257;
        double r53259 = 2.0;
        double r53260 = pow(r53256, r53259);
        double r53261 = r53258 + r53260;
        double r53262 = sqrt(r53261);
        double r53263 = r53261 / r53262;
        double r53264 = r53254 + r53256;
        double r53265 = r53264 / r53262;
        double r53266 = r53263 * r53265;
        double r53267 = sin(r53244);
        double r53268 = r53243 * r53267;
        double r53269 = r53268 * r53242;
        double r53270 = r53266 + r53269;
        double r53271 = atan2(r53252, r53270);
        double r53272 = r53240 + r53271;
        return r53272;
}

Error

Bits error versus lambda1

Bits error versus lambda2

Bits error versus phi1

Bits error versus phi2

Derivation

1. Initial program 0.8

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

3. Applied cos-diff 0.8

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

4. Applied distribute-rgt-in 0.8

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

5. Applied associate-+r+ 0.8

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

7. Applied sub-neg 0.8

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

8. Applied sin-sum 0.2

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

9. Simplified 0.2

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

11. Applied flip3-+ 0.2

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

12. Simplified 0.2

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

14. Applied add-sqr-sqrt 0.3

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

15. Applied sum-cubes 0.3

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

16. Applied times-frac 0.3

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

17. Simplified 0.3

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

18. Simplified 0.3

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

19. Final simplification 0.3

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

Reproduce

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