\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \cos \left(\lambda_1 - \lambda_2\right)\right) \cdot R\log \left(e^{\cos^{-1} \left(\sin \phi_1 \cdot \sin \phi_2 + \left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \left(\cos \lambda_1 \cdot \cos \lambda_2 + \sin \lambda_1 \cdot \sin \lambda_2\right)\right)}\right) \cdot Rdouble f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r23289 = phi1;
double r23290 = sin(r23289);
double r23291 = phi2;
double r23292 = sin(r23291);
double r23293 = r23290 * r23292;
double r23294 = cos(r23289);
double r23295 = cos(r23291);
double r23296 = r23294 * r23295;
double r23297 = lambda1;
double r23298 = lambda2;
double r23299 = r23297 - r23298;
double r23300 = cos(r23299);
double r23301 = r23296 * r23300;
double r23302 = r23293 + r23301;
double r23303 = acos(r23302);
double r23304 = R;
double r23305 = r23303 * r23304;
return r23305;
}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r23306 = phi1;
double r23307 = sin(r23306);
double r23308 = phi2;
double r23309 = sin(r23308);
double r23310 = r23307 * r23309;
double r23311 = cos(r23306);
double r23312 = cos(r23308);
double r23313 = r23311 * r23312;
double r23314 = lambda1;
double r23315 = cos(r23314);
double r23316 = lambda2;
double r23317 = cos(r23316);
double r23318 = r23315 * r23317;
double r23319 = sin(r23314);
double r23320 = sin(r23316);
double r23321 = r23319 * r23320;
double r23322 = r23318 + r23321;
double r23323 = r23313 * r23322;
double r23324 = r23310 + r23323;
double r23325 = acos(r23324);
double r23326 = exp(r23325);
double r23327 = log(r23326);
double r23328 = R;
double r23329 = r23327 * r23328;
return r23329;
}



Bits error versus R



Bits error versus lambda1



Bits error versus lambda2



Bits error versus phi1



Bits error versus phi2
Results
Initial program 16.9
rmApplied cos-diff3.9
rmApplied add-log-exp3.9
Final simplification3.9
herbie shell --seed 2020065
(FPCore (R lambda1 lambda2 phi1 phi2)
:name "Spherical law of cosines"
:precision binary64
(* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R))