Pas*_*uoq 11 c floating-point ieee-754 extended-precision
以下是插值函数的两种实现.争论u1
始终在0.
和之间1.
.
#include <stdio.h>
double interpol_64(double u1, double u2, double u3)
{
return u2 * (1.0 - u1) + u1 * u3;
}
double interpol_80(double u1, double u2, double u3)
{
return u2 * (1.0 - (long double)u1) + u1 * (long double)u3;
}
int main()
{
double y64,y80,u1,u2,u3;
u1 = 0.025;
u2 = 0.195;
u3 = 0.195;
y64 = interpol_64(u1, u2, u3);
y80 = interpol_80(u1, u2, u3);
printf("u2: %a\ny64:%a\ny80:%a\n", u2, y64, y80);
}
Run Code Online (Sandbox Code Playgroud)
在具有80位long double
s 的严格IEEE 754平台上,所有计算interpol_64()
都是根据IEEE 754双精度和interpol_80()
80位扩展精度完成的.程序打印:
u2: 0x1.8f5c28f5c28f6p-3
y64:0x1.8f5c28f5c28f5p-3
y80:0x1.8f5c28f5c28f6p-3
Run Code Online (Sandbox Code Playgroud)
我感兴趣的财产"由该函数返回的结果总是在中间u2
和u3
".此属性为false interpol_64()
,如main()
上面的值所示.
该物业是否有机会成为真实的interpol_80()
?如果不是,反例是什么?如果我们知道它们u2 != u3
或它们之间的距离最小,这会有帮助吗?是否有一种方法来确定中间计算的有效位宽度,在该计算中,属性将保证为真?
编辑:在我尝试的所有随机值上,当内部计算以扩展精度完成时,属性保持不变.如果interpol_80()
接受了long double
参数,那么构建一个反例也相对容易,但这里的问题是关于一个带double
参数的函数.这使得构建反例(如果有的话)变得更加困难.
注意:生成x87指令的编译器可能会为interpol_64()
和生成相同的代码interpol_80()
,但这与我的问题相关.
是的,interpol_80() 是安全的,我们来演示一下。
问题表明输入是 64 位浮点数
rnd64(ui) = ui
Run Code Online (Sandbox Code Playgroud)
结果是准确的(假设*和+是数学运算)
r = u2*(1-u1)+(u1*u3)
Run Code Online (Sandbox Code Playgroud)
舍入为 64 位浮点数的最佳返回值是
r64 = rnd64(r)
Run Code Online (Sandbox Code Playgroud)
因为我们有这些属性
u2 <= r <= u3
Run Code Online (Sandbox Code Playgroud)
可以保证
rnd64(u2) <= rnd64(r) <= rnd64(u3)
u2 <= r64 <= u3
Run Code Online (Sandbox Code Playgroud)
转换为 80 位 u1、u2、u3 也是准确的。
rnd80(ui)=ui
Run Code Online (Sandbox Code Playgroud)
现在,我们假设0 <= u2 <= u3
,那么执行不精确的浮点运算最多会导致 4 个舍入错误:
rf = rnd(rnd(u2*rnd(1-u1)) + rnd(u1*u3))
Run Code Online (Sandbox Code Playgroud)
假设四舍五入到最接近的偶数,则该值最多与精确值相差 2 ULP。如果使用 64 位浮点数或 80 位浮点数进行舍入:
r - 2 ulp64(r) <= rf64 <= r + 2 ulp64(r)
r - 2 ulp80(r) <= rf80 <= r + 2 ulp80(r)
Run Code Online (Sandbox Code Playgroud)
rf64
可能会偏离 2 ulp,所以 interpol-64() 是不安全的,但是呢rnd64( rf80 )
?
我们可以说:
rnd64(r - 2 ulp80(r)) <= rnd64(rf80) <= rnd64(r + 2 ulp80(r))
Run Code Online (Sandbox Code Playgroud)
自0 <= u2 <= u3
那以后
ulp80(u2) <= ulp80(r) <= ulp80(r3)
rnd64(u2 - 2 ulp80(u2)) <= rnd64(r - 2 ulp80(r)) <= rnd64(rf80)
rnd64(u3 + 2 ulp80(u3)) >= rnd64(r + 2 ulp80(r)) >= rnd64(rf80)
Run Code Online (Sandbox Code Playgroud)
(u2-ulp64(u2)/2 , u2+ulp64(u2)/2)
幸运的是,就像我们得到的范围内的每个数字一样
rnd64(u2 - 2 ulp80(u2)) = u2
rnd64(u3 + 2 ulp80(u3)) = u3
Run Code Online (Sandbox Code Playgroud)
自从ulp80(x)=ulp62(x)/2^(64-53)
这样我们就得到了证明
u2 <= rnd64(rf80) <= u3
Run Code Online (Sandbox Code Playgroud)
对于 u2 <= u3 <= 0,我们可以轻松应用相同的证明。
最后要研究的情况是 u2 <= 0 <= u3。如果我们减去 2 个大值,则结果最多可达 ulp(big)/2,而不是 ulp(big-big)/2...
因此,我们所做的断言不再成立:
r - 2 ulp64(r) <= rf64 <= r + 2 ulp64(r)
Run Code Online (Sandbox Code Playgroud)
幸运的是,u2 <= u2*(1-u1) <= 0 <= u1*u3 <= u3
这在四舍五入后被保留
u2 <= rnd(u2*rnd(1-u1)) <= 0 <= rnd(u1*u3) <= u3
Run Code Online (Sandbox Code Playgroud)
因此,由于添加的数量具有相反的符号:
u2 <= rnd(u2*rnd(1-u1)) + rnd(u1*u3) <= u3
Run Code Online (Sandbox Code Playgroud)
四舍五入后也是如此,所以我们可以再次保证
u2 <= rnd64( rf80 ) <= u3
Run Code Online (Sandbox Code Playgroud)
量子电动力学
为了完整起见,我们应该关心非正规输入(逐渐下溢),但我希望你不会对压力测试那么恶毒。我不会展示那些会发生什么......
编辑:
这是后续断言,因为以下断言有点近似,并在 0 <= u2 <= u3 时生成一些注释
r - 2 ulp80(r) <= rf80 <= r + 2 ulp80(r)
Run Code Online (Sandbox Code Playgroud)
我们可以写出以下不等式:
rnd(1-u1) <= 1
rnd(1-u1) <= 1-u1+ulp(1)/4
u2*rnd(1-u1) <= u2 <= r
u2*rnd(1-u1) <= u2*(1-u1)+u2*ulp(1)/4
u2*ulp(1) < 2*ulp(u2) <= 2*ulp(r)
u2*rnd(1-u1) < u2*(1-u1)+ulp(r)/2
Run Code Online (Sandbox Code Playgroud)
对于下一个舍入操作,我们使用
ulp(u2*rnd(1-u1)) <= ulp(r)
rnd(u2*rnd(1-u1)) < u2*(1-u1)+ulp(r)/2 + ulp(u2*rnd(1-u1))/2
rnd(u2*rnd(1-u1)) < u2*(1-u1)+ulp(r)/2 + ulp(r)/2
rnd(u2*rnd(1-u1)) < u2*(1-u1)+ulp(r)
Run Code Online (Sandbox Code Playgroud)
对于总和的第二部分,我们有:
u1*u3 <= r
rnd(u1*u3) <= u1*u3 + ulp(u1*u3)/2
rnd(u1*u3) <= u1*u3 + ulp(r)/2
rnd(u2*rnd(1-u1))+rnd(u1*u3) < u2*(1-u1)+u1*u3 + 3*ulp(r)/2
rnd(rnd(u2*rnd(1-u1))+rnd(u1*u3)) < r + 3*ulp(r)/2 + ulp(r+3*ulp(r)/2)/2
ulp(r+3*ulp(r)/2) <= 2*ulp(r)
rnd(rnd(u2*rnd(1-u1))+rnd(u1*u3)) < r + 5*ulp(r)/2
Run Code Online (Sandbox Code Playgroud)
我没有证明最初的说法,但还没有那么远......
归档时间: |
|
查看次数: |
620 次 |
最近记录: |