浮点乘法的严格不等式

Question

假设a,x和y是正的IEEE浮点数, x < y.证明a × x < a × y其中×表示浮点乘法舍入到最近.

天真地,你可能会认为对于某些a和x接近y,你会得到一个 × x = a × y.事实证明,这不可能发生(只要不包括非规范化数字,无穷大和NaN).

我对一个优雅的证据感兴趣,如果可能的话,我会给出一本书或纸.

TAKE 2:正如Pascal Cuoq的回复所示,上述陈述是错误的.y = 1 的受限制版本怎么样？以下是要证明的陈述:

假设a和x是正的IEEE浮点数, x <1.证明a × x < a其中×表示浮点乘法舍入到最接近.

Answer 1

该属性为false,如下面的C99程序所示,当编译器为编译器提供IEEE binary64 double和FLT_EVAL_METHOD= 0时:

#include <stdio.h>
#include <math.h>
#include <float.h>

int main(void) {
  double z = 1.0;
  double y = nextafter(z, 0.0);
  double x = nextafter(y, 0.0);
  double a = 1.0 + 2 * DBL_EPSILON;

  printf("%a %a\n", a*x, a*y);
}

结果:

0x1.0000000000001p+0 0x1.0000000000001p+0

这y是1.0的前身,1.0 x的前身y,以及a1.0的继任者.的价值观x和y是在其顶部binade,其中相对精度是最好的,和值a*x和a*y是在他们的底部,其中,相对精度是最糟糕的.这是如何a*x并a*y四舍五入到相同的值.

问题中的属性看起来是正确的,因为反例只能在单个ULP上发生x并且y由单个ULP分开,并且通过a在目标binade中发送它们比在原始binade中相对更低来进行乘法.