floating-point - 浮点: is a/b - 1 > 0 if a > b

Question

假设任何精度的 IEEE 754 都是 a / b - 1.0 > 0.0对于所有有限 float a和b哪里a > b > 0 ？这个编译器依赖吗？如何证明或反驳这个性质？下面的简短脚本返回 true。

import numpy as np
arr = np.random.rand(1000000)
np.all((np.nextafter(arr, np.inf) / arr - 1) > 0.0)

Answer 1

在通常的平局比赛中确实如此。不失一般性，假设1 <= a < 2 。舍入到偶数时，如果 b < 1 ，然后a/b = sum(i=0..infty) (1-b)^i a > a + (1-b)a >= a + ulp(a)/2 a ，所以round-to-even(a/b) > a 。所以我们可以假设1 <= b < a < 2 。您可以计算a/b = 1 + (a-b)/b > 1 + (a-b)/2 >= 1 + ulp(a)/2 , so round-to-even(a/b) > 1 .