浮点乘法的严格不等式

Question

假设 a、x 和 y 是正 IEEE 浮点数 x < y。证明 a×x < a×y 其中× 表示浮点乘法四舍五入到最近。

天真地，您可能会假设对于某些 a 和 x 接近 y , 你会得到 a×x = a×y .原来这不可能发生（只要非规范化数字、无穷大和 NaN 是排除）。

我对优雅的证明感兴趣，如果可能的话，一本书或论文这是给出的地方。

TAKE 2: 正如Pascal Cuoq 的回复所示，上面的语句是错误的。 y = 1 的限制版本怎么样？这里是待证命题：

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

Answer 1

属性为假，如以下 C99 程序所示，当使用为 double 和 FLT_EVAL_METHOD=0 提供 IEEE binary64 的编译器编译时：

#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

那是y1.0的前身，x是[=14=的前身]，a是1.0的后继者。 x 和 y 的值在它们的 binade 的顶部，相对精度最好，而 a*x 和 a*y 的值在他们的底部，相对精度最差的地方。这就是 a*x 和 a*y 舍入为相同值的方式。

问题中的属性看起来是正确的，因为反例只能发生在 x 和 y 由单个 ULP 分隔并且乘以 a将它们发送到目标二进制文件中的位置比在原始二进制文件中的位置相对较低。

Answer 2

为您修改后的问题提供正式证明（语言略有改动）：

Suppose a and x are positive IEEE floating point numbers with x < 1. Prove that [ax] < a where [] denotes default floating-point rounding.

WLOG，让a在[1, 2)。如果 a 是 1，则该语句通常为真，因此我们实际上只需要考虑 (1,2) 中的 a。 x < 1 意味着 x <= 1 - u/2，其中 u = ulp(1) = ulp(a)。我们有：

ax <= a - au/2

我们还有a > 1，所以au/2 > u/2，所以：

ax <= a - au/2 < a - u/2

因为ax比a低半个ulp多，[ax] < a.

浮点乘法的严格不等式

Strict inequality for floating point multiplication

floating-point

floating-accuracy

ieee-754