R \cdot \left(2 \cdot \tan^{-1}_* \frac{\sqrt{{\left(\sin \left(\frac{\phi_1 - \phi_2}{2}\right)\right)}^{2} + \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right) \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}}{\sqrt{1 - \left({\left(\sin \left(\frac{\phi_1 - \phi_2}{2}\right)\right)}^{2} + \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right) \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right)}}\right)R \cdot \left(2 \cdot \tan^{-1}_* \frac{\sqrt{{\left(\sin \left(\frac{\phi_1}{2}\right) \cdot \cos \left(\frac{\phi_2}{2}\right) - \cos \left(\frac{\phi_1}{2}\right) \cdot \sin \left(\frac{\phi_2}{2}\right)\right)}^{2} + \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right) \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}}{\sqrt{1 - \left({\left(\sin \left(\frac{\phi_1}{2}\right) \cdot \cos \left(\frac{\phi_2}{2}\right) - \cos \left(\frac{\phi_1}{2}\right) \cdot \sin \left(\frac{\phi_2}{2}\right)\right)}^{2} + \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \log \left(e^{\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}\right)\right) \cdot \log \left(e^{\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}\right)\right)}}\right)double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r74637 = R;
double r74638 = 2.0;
double r74639 = phi1;
double r74640 = phi2;
double r74641 = r74639 - r74640;
double r74642 = r74641 / r74638;
double r74643 = sin(r74642);
double r74644 = pow(r74643, r74638);
double r74645 = cos(r74639);
double r74646 = cos(r74640);
double r74647 = r74645 * r74646;
double r74648 = lambda1;
double r74649 = lambda2;
double r74650 = r74648 - r74649;
double r74651 = r74650 / r74638;
double r74652 = sin(r74651);
double r74653 = r74647 * r74652;
double r74654 = r74653 * r74652;
double r74655 = r74644 + r74654;
double r74656 = sqrt(r74655);
double r74657 = 1.0;
double r74658 = r74657 - r74655;
double r74659 = sqrt(r74658);
double r74660 = atan2(r74656, r74659);
double r74661 = r74638 * r74660;
double r74662 = r74637 * r74661;
return r74662;
}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r74663 = R;
double r74664 = 2.0;
double r74665 = phi1;
double r74666 = r74665 / r74664;
double r74667 = sin(r74666);
double r74668 = phi2;
double r74669 = r74668 / r74664;
double r74670 = cos(r74669);
double r74671 = r74667 * r74670;
double r74672 = cos(r74666);
double r74673 = sin(r74669);
double r74674 = r74672 * r74673;
double r74675 = r74671 - r74674;
double r74676 = pow(r74675, r74664);
double r74677 = cos(r74665);
double r74678 = cos(r74668);
double r74679 = r74677 * r74678;
double r74680 = lambda1;
double r74681 = lambda2;
double r74682 = r74680 - r74681;
double r74683 = r74682 / r74664;
double r74684 = sin(r74683);
double r74685 = r74679 * r74684;
double r74686 = r74685 * r74684;
double r74687 = r74676 + r74686;
double r74688 = sqrt(r74687);
double r74689 = 1.0;
double r74690 = exp(r74684);
double r74691 = log(r74690);
double r74692 = r74679 * r74691;
double r74693 = r74692 * r74691;
double r74694 = r74676 + r74693;
double r74695 = r74689 - r74694;
double r74696 = sqrt(r74695);
double r74697 = atan2(r74688, r74696);
double r74698 = r74664 * r74697;
double r74699 = r74663 * r74698;
return r74699;
}



Bits error versus R



Bits error versus lambda1



Bits error versus lambda2



Bits error versus phi1



Bits error versus phi2
Results
Initial program 24.6
rmApplied div-sub24.6
Applied sin-diff24.0
rmApplied div-sub24.0
Applied sin-diff14.3
rmApplied add-log-exp14.3
rmApplied add-log-exp14.3
Final simplification14.3
herbie shell --seed 2020056
(FPCore (R lambda1 lambda2 phi1 phi2)
:name "Distance on a great circle"
:precision binary64
(* R (* 2 (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))))))))