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 \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right)}}\right)double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r76150 = R;
double r76151 = 2.0;
double r76152 = phi1;
double r76153 = phi2;
double r76154 = r76152 - r76153;
double r76155 = r76154 / r76151;
double r76156 = sin(r76155);
double r76157 = pow(r76156, r76151);
double r76158 = cos(r76152);
double r76159 = cos(r76153);
double r76160 = r76158 * r76159;
double r76161 = lambda1;
double r76162 = lambda2;
double r76163 = r76161 - r76162;
double r76164 = r76163 / r76151;
double r76165 = sin(r76164);
double r76166 = r76160 * r76165;
double r76167 = r76166 * r76165;
double r76168 = r76157 + r76167;
double r76169 = sqrt(r76168);
double r76170 = 1.0;
double r76171 = r76170 - r76168;
double r76172 = sqrt(r76171);
double r76173 = atan2(r76169, r76172);
double r76174 = r76151 * r76173;
double r76175 = r76150 * r76174;
return r76175;
}
double f(double R, double lambda1, double lambda2, double phi1, double phi2) {
double r76176 = R;
double r76177 = 2.0;
double r76178 = phi1;
double r76179 = r76178 / r76177;
double r76180 = sin(r76179);
double r76181 = phi2;
double r76182 = r76181 / r76177;
double r76183 = cos(r76182);
double r76184 = r76180 * r76183;
double r76185 = cos(r76179);
double r76186 = sin(r76182);
double r76187 = r76185 * r76186;
double r76188 = r76184 - r76187;
double r76189 = pow(r76188, r76177);
double r76190 = cos(r76178);
double r76191 = cos(r76181);
double r76192 = r76190 * r76191;
double r76193 = lambda1;
double r76194 = lambda2;
double r76195 = r76193 - r76194;
double r76196 = r76195 / r76177;
double r76197 = sin(r76196);
double r76198 = r76192 * r76197;
double r76199 = r76198 * r76197;
double r76200 = r76189 + r76199;
double r76201 = sqrt(r76200);
double r76202 = 1.0;
double r76203 = exp(r76197);
double r76204 = log(r76203);
double r76205 = r76192 * r76204;
double r76206 = r76205 * r76197;
double r76207 = r76189 + r76206;
double r76208 = r76202 - r76207;
double r76209 = sqrt(r76208);
double r76210 = atan2(r76201, r76209);
double r76211 = r76177 * r76210;
double r76212 = r76176 * r76211;
return r76212;
}



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-diff13.8
rmApplied add-log-exp13.8
Final simplification13.8
herbie shell --seed 2020036
(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))))))))))