Midpoint on a great circle

Average Error: 0.9 → 0.3

Time: 19.8s

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 \lambda_2\right)}{\frac{{\left(\cos \phi_1\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right)}^{3}}{\cos \phi_1 \cdot \cos \phi_1 + \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right) \cdot \frac{{\left(\cos \phi_2 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right)\right)}^{2} - {\left(\cos \phi_1\right)}^{2}}{\cos \phi_1 + \cos \phi_2 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right)}} + \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 r63601 = lambda1;
        double r63602 = phi2;
        double r63603 = cos(r63602);
        double r63604 = lambda2;
        double r63605 = r63601 - r63604;
        double r63606 = sin(r63605);
        double r63607 = r63603 * r63606;
        double r63608 = phi1;
        double r63609 = cos(r63608);
        double r63610 = cos(r63605);
        double r63611 = r63603 * r63610;
        double r63612 = r63609 + r63611;
        double r63613 = atan2(r63607, r63612);
        double r63614 = r63601 + r63613;
        return r63614;
}

↓

double f(double lambda1, double lambda2, double phi1, double phi2) {
        double r63615 = lambda1;
        double r63616 = phi2;
        double r63617 = cos(r63616);
        double r63618 = sin(r63615);
        double r63619 = lambda2;
        double r63620 = cos(r63619);
        double r63621 = r63618 * r63620;
        double r63622 = cos(r63615);
        double r63623 = sin(r63619);
        double r63624 = r63622 * r63623;
        double r63625 = r63621 - r63624;
        double r63626 = r63617 * r63625;
        double r63627 = phi1;
        double r63628 = cos(r63627);
        double r63629 = 3.0;
        double r63630 = pow(r63628, r63629);
        double r63631 = r63622 * r63620;
        double r63632 = r63617 * r63631;
        double r63633 = pow(r63632, r63629);
        double r63634 = r63630 + r63633;
        double r63635 = r63628 * r63628;
        double r63636 = r63620 * r63622;
        double r63637 = r63617 * r63636;
        double r63638 = 2.0;
        double r63639 = pow(r63637, r63638);
        double r63640 = pow(r63628, r63638);
        double r63641 = r63639 - r63640;
        double r63642 = r63628 + r63637;
        double r63643 = r63641 / r63642;
        double r63644 = r63632 * r63643;
        double r63645 = r63635 + r63644;
        double r63646 = r63634 / r63645;
        double r63647 = r63618 * r63623;
        double r63648 = r63647 * r63617;
        double r63649 = r63646 + r63648;
        double r63650 = atan2(r63626, r63649);
        double r63651 = r63615 + r63650;
        return r63651;
}

Error

Bits error versus lambda1

Bits error versus lambda2

Bits error versus phi1

Bits error versus phi2

Derivation

1. Initial program 0.9

   \[\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 sin-diff 0.9

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

5. Applied cos-diff 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 \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)}}\]

6. Applied distribute-rgt-in 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 \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)}}\]

7. Applied associate-+r+ 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 \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}}\]

8. 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 \lambda_2\right)}{\color{blue}{\left(\cos \phi_1 + \cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right)} + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2}\]
9. Using strategy rm

10. Applied flip3-+ 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 \lambda_2\right)}{\color{blue}{\frac{{\left(\cos \phi_1\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right)}^{3}}{\cos \phi_1 \cdot \cos \phi_1 + \left(\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right) - \cos \phi_1 \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right)\right)}} + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2}\]

11. 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 \lambda_2\right)}{\frac{{\left(\cos \phi_1\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right)}^{3}}{\color{blue}{\cos \phi_1 \cdot \cos \phi_1 + \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) - \cos \phi_1\right)}} + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2}\]
12. Using strategy rm

13. Applied flip-- 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 \lambda_2\right)}{\frac{{\left(\cos \phi_1\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right)}^{3}}{\cos \phi_1 \cdot \cos \phi_1 + \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right) \cdot \color{blue}{\frac{\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right) \cdot \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right) - \cos \phi_1 \cdot \cos \phi_1}{\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \cos \phi_1}}} + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2}\]

14. 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 \lambda_2\right)}{\frac{{\left(\cos \phi_1\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right)}^{3}}{\cos \phi_1 \cdot \cos \phi_1 + \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right) \cdot \frac{\color{blue}{{\left(\cos \phi_2 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right)\right)}^{2} - {\left(\cos \phi_1\right)}^{2}}}{\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right) + \cos \phi_1}} + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2}\]

15. 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 \lambda_2\right)}{\frac{{\left(\cos \phi_1\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right)}^{3}}{\cos \phi_1 \cdot \cos \phi_1 + \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right) \cdot \frac{{\left(\cos \phi_2 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right)\right)}^{2} - {\left(\cos \phi_1\right)}^{2}}{\color{blue}{\cos \phi_1 + \cos \phi_2 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right)}}} + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2}\]

16. 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 \lambda_2\right)}{\frac{{\left(\cos \phi_1\right)}^{3} + {\left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right)}^{3}}{\cos \phi_1 \cdot \cos \phi_1 + \left(\cos \phi_2 \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2\right)\right) \cdot \frac{{\left(\cos \phi_2 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right)\right)}^{2} - {\left(\cos \phi_1\right)}^{2}}{\cos \phi_1 + \cos \phi_2 \cdot \left(\cos \lambda_2 \cdot \cos \lambda_1\right)}} + \left(\sin \lambda_1 \cdot \sin \lambda_2\right) \cdot \cos \phi_2}\]

Reproduce

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