主页 / coding / 问题 / 79419785
Accepted
Hans Brende
Asked: 2025-02-07 09:36:42 +0800 CST

根据 IEEE 754 语义，x * y = ((x * y) / y) * y 总是正确吗？

  • 772

给定两个非零、有限、双精度浮点数x和y，等式

x * y == ((x * y) / y) * y

在默认的 IEEE 754 语义下成立吗？

我已经通过编程搜索了数十亿种可能性（包括低于正常范围的可能性），但无法找到反例，但也不确定如何证明该断言是正确的。

（我确实知道的是，更简单的断言x == (x / y) * y和x == (x * y) / y都是错误的，因为我可以轻松找到它们的反例。）

floating-point

1 个回答

  1. Best Answer

    在双精度（binary64）中，即精度为 p = 53 位，有以下反例：

    #include <stdio.h>
int main (int argc, char *argv[])
{
  double x = 0x1.0000004000001p+0;
  double y = 0x1.ffffff8000001p+0;
  double r1 = x * y;
  double r2 = ((x * y) / y) * y;
  printf ("r1 = %a\n", r1);
  printf ("r2 = %a\n", r2);
  return 0;
}

    输出

    r1 = 0x1p+1
r2 = 0x1.fffffffffffffp+0

    我通过使用GNU MPFR在小精度下进行详尽测试（该属性不依赖于 x 和 y 的指数，可以将其设置为常数）找到了这个反例，并且发现了一个模式：在精度 p = 2k+3 时，以 2 为基数写的以下对是一个反例：

    x = 1.0{k}10{k}1
y = 1.1{k}00{k}1

    其中{k}表示该数字重复 k 次。

    注意：此问题与 GNU Emacs + Cairo 中产生的错误有点相似，其中((1/s)*b)*s)涉及表达式。请参阅我的文章。

    • 8

相关问题