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 r88021 = R;
double r88022 = 2.0;
double r88023 = phi1;
double r88024 = phi2;
double r88025 = r88023 - r88024;
double r88026 = r88025 / r88022;
double r88027 = sin(r88026);
double r88028 = pow(r88027, r88022);
double r88029 = cos(r88023);
double r88030 = cos(r88024);
double r88031 = r88029 * r88030;
double r88032 = lambda1;
double r88033 = lambda2;
double r88034 = r88032 - r88033;
double r88035 = r88034 / r88022;
double r88036 = sin(r88035);
double r88037 = r88031 * r88036;
double r88038 = r88037 * r88036;
double r88039 = r88028 + r88038;
double r88040 = sqrt(r88039);
double r88041 = 1.0;
double r88042 = r88041 - r88039;
double r88043 = sqrt(r88042);
double r88044 = atan2(r88040, r88043);
double r88045 = r88022 * r88044;
double r88046 = r88021 * r88045;
return r88046;
}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r88047 = R;
double r88048 = 2.0;
double r88049 = phi1;
double r88050 = r88049 / r88048;
double r88051 = sin(r88050);
double r88052 = phi2;
double r88053 = r88052 / r88048;
double r88054 = cos(r88053);
double r88055 = r88051 * r88054;
double r88056 = cos(r88050);
double r88057 = sin(r88053);
double r88058 = r88056 * r88057;
double r88059 = r88055 - r88058;
double r88060 = pow(r88059, r88048);
double r88061 = cos(r88049);
double r88062 = cos(r88052);
double r88063 = r88061 * r88062;
double r88064 = lambda1;
double r88065 = lambda2;
double r88066 = r88064 - r88065;
double r88067 = r88066 / r88048;
double r88068 = sin(r88067);
double r88069 = r88063 * r88068;
double r88070 = r88069 * r88068;
double r88071 = r88060 + r88070;
double r88072 = sqrt(r88071);
double r88073 = 1.0;
double r88074 = exp(r88068);
double r88075 = log(r88074);
double r88076 = r88063 * r88075;
double r88077 = r88076 * r88075;
double r88078 = r88060 + r88077;
double r88079 = r88073 - r88078;
double r88080 = sqrt(r88079);
double r88081 = atan2(r88072, r88080);
double r88082 = r88048 * r88081;
double r88083 = r88047 * r88082;
return r88083;
}



Bits error versus R



Bits error versus lambda1



Bits error versus lambda2



Bits error versus phi1



Bits error versus phi2
Results
Initial program 24.3
rmApplied div-sub24.3
Applied sin-diff23.7
rmApplied div-sub23.7
Applied sin-diff14.0
rmApplied add-log-exp14.0
rmApplied add-log-exp14.0
Final simplification14.0
herbie shell --seed 2020033
(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))))))))))