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 r70303 = R;
double r70304 = 2.0;
double r70305 = phi1;
double r70306 = phi2;
double r70307 = r70305 - r70306;
double r70308 = r70307 / r70304;
double r70309 = sin(r70308);
double r70310 = pow(r70309, r70304);
double r70311 = cos(r70305);
double r70312 = cos(r70306);
double r70313 = r70311 * r70312;
double r70314 = lambda1;
double r70315 = lambda2;
double r70316 = r70314 - r70315;
double r70317 = r70316 / r70304;
double r70318 = sin(r70317);
double r70319 = r70313 * r70318;
double r70320 = r70319 * r70318;
double r70321 = r70310 + r70320;
double r70322 = sqrt(r70321);
double r70323 = 1.0;
double r70324 = r70323 - r70321;
double r70325 = sqrt(r70324);
double r70326 = atan2(r70322, r70325);
double r70327 = r70304 * r70326;
double r70328 = r70303 * r70327;
return r70328;
}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r70329 = R;
double r70330 = 2.0;
double r70331 = phi1;
double r70332 = r70331 / r70330;
double r70333 = sin(r70332);
double r70334 = phi2;
double r70335 = r70334 / r70330;
double r70336 = cos(r70335);
double r70337 = r70333 * r70336;
double r70338 = cos(r70332);
double r70339 = sin(r70335);
double r70340 = r70338 * r70339;
double r70341 = r70337 - r70340;
double r70342 = pow(r70341, r70330);
double r70343 = cos(r70331);
double r70344 = cos(r70334);
double r70345 = r70343 * r70344;
double r70346 = lambda1;
double r70347 = lambda2;
double r70348 = r70346 - r70347;
double r70349 = r70348 / r70330;
double r70350 = sin(r70349);
double r70351 = r70345 * r70350;
double r70352 = r70351 * r70350;
double r70353 = r70342 + r70352;
double r70354 = sqrt(r70353);
double r70355 = 1.0;
double r70356 = exp(r70350);
double r70357 = log(r70356);
double r70358 = r70345 * r70357;
double r70359 = r70358 * r70357;
double r70360 = r70342 + r70359;
double r70361 = r70355 - r70360;
double r70362 = sqrt(r70361);
double r70363 = atan2(r70354, r70362);
double r70364 = r70330 * r70363;
double r70365 = r70329 * r70364;
return r70365;
}



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))))))))))