相关疑难解决方法(0)

请考虑以下代码:

0.1 + 0.2 == 0.3  ->  false

0.1 + 0.2         ->  0.30000000000000004

为什么会出现这些不准确之处？

我正在努力将sqrt函数(对于64位双精度数)从fdlibm移植到我目前正在使用的模型检查器工具(cbmc).
作为我的一部分,我阅读了很多关于ieee-754标准的内容,但我认为我不理解基本操作(包括sqrt)的精度保证.

测试我的fdlibm的sqrt端口,我在64位double上使用sqrt进行了以下计算:

sqrt(1977061516825203605555216616167125005658976571589721139027150498657494589171970335387417823661417383745964289845929120708819092392090053015474001800648403714048.0) = 44464159913633855548904943164666890000299422761159637702558734139742800916250624.0

(这个案例在我的测试中打破了关于精度的简单后置条件;我不确定是否可以使用IEEE-754来实现这种后置条件)

为了进行比较,几个多精度工具计算如下:

sqrt(1977061516825203605555216616167125005658976571589721139027150498657494589171970335387417823661417383745964289845929120708819092392090053015474001800648403714048.0) =44464159913633852501611468455197640079591886932526256694498106717014555047373210.truncated

可以看出,左起第17个数字是不同的,意味着如下错误:

3047293474709469249920707535828633381008060627422728245868877413.0

问题1:是否允许这么大的错误？

标准是说每个基本操作(+, - ,*,/,sqrt)应该在0.5 ulps之内,这意味着它应该等于数学上精确的结果四舍五入到最近的fp表示(维基说的是一些库)只保证1 ulp,但目前并不重要).

问题2:这是否意味着,每个基本操作都应该有一个错误<2.220446e-16,64位双精度(机器epsilon)？

我用x86-32 linux系统(glibc/eglibc)计算了相同的结果,并得到了与fdlibm相同的结果,让我想到:

• a:我做错了什么(但是如何:printf将成为候选人,但我不知道是否可能是这个原因)
• b:错误/精度在这些库中很常见