令 a、b 和 c 为非大正整数。a/b/c 是否总是等于 a/(b * c) 与 C# 整数算术?对我来说,在 C# 中它看起来像:
int a = 5126, b = 76, c = 14;
int x1 = a / b / c;
int x2 = a / (b * c);
所以我的问题是:是否x1 == x2
适用于所有 a、b 和 c?
令 a、b 和 c 为非大正整数。a/b/c 是否总是等于 a/(b * c) 与 C# 整数算术?对我来说,在 C# 中它看起来像:
int a = 5126, b = 76, c = 14;
int x1 = a / b / c;
int x2 = a / (b * c);
所以我的问题是:是否x1 == x2
适用于所有 a、b 和 c?
我非常喜欢这个问题,因此我在2013 年 6 月 4 日将其作为我博客的主题。谢谢你的好问题!
大箱子很容易拿到。例如:
a = 1073741823;
b = 134217727;
c = 134217727;
因为b * c
溢出到负数。
我还要补充一点,在检查算术中,a / (b * c)
和之间(a / b) / c
的区别可能是正常工作的程序和崩溃的程序之间的区别。b
如果和的乘积c
溢出整数的边界,则前者将在检查的上下文中崩溃。
对于小的正整数,比如说,小到可以放入一个短整数,应该保持恒等式。
Timothy Shields 刚刚发布了一个证明;我在这里提出一个替代证明。假设这里的所有数字都是非负整数并且没有任何操作溢出。
的整数除法x / y
找到q
这样的值q * y + r == x
,其中0 <= r < y
。
所以除法a / (b * c)
找到q1
这样的值
q1 * b * c + r1 == a
在哪里0 <= r1 < b * c
除法( a / b ) / c
首先找到qt
这样的值
qt * b + r3 == a
然后找到q2
这样的值
q2 * c + r2 == qt
因此,将其替换为qt
,我们得到:
q2 * b * c + b * r2 + r3 == a
哪里0 <= r2 < c
和0 <= r3 < b
。
两个相等的事物彼此相等,所以我们有
q1 * b * c + r1 == q2 * b * c + b * r2 + r3
假设q1 == q2 + x
某个整数x
。代入并解决x
:
q2 * b * c + x * b * c + r1 = q2 * b * c + b * r2 + r3
x = (b * r2 + r3 - r1) / (b * c)
在哪里
0 <= r1 < b * c
0 <= r2 < c
0 <= r3 < b
可以x
大于零吗?不,我们有不等式:
b * r2 + r3 - r1 <= b * r2 + r3 <= b * (c - 1) + r3 < b * (c - 1) + b == b * c
所以那个分数的分子总是小于b * c
,所以x
不能大于零。
可以x
小于零吗?不,通过类似的论点,留给读者。
因此整数x
为零,因此q1 == q2
.
让\
表示整数除法(/
两个int
s 之间的 C# 运算符),让/
表示通常的数学除法。然后,如果x,y,z
是正整数并且我们忽略溢出,
(x \ y) \ z
= floor(floor(x / y) / z) [1]
= floor((x / y) / z) [2]
= floor(x / (y * z))
= x \ (y * z)
在哪里
a \ b = floor(a / b)
[1]
上面从一行到另一行的跳转[2]
解释如下。假设你有两个整数a
和b
一个小数f
在范围内[0, 1)
。很容易看出
floor(a / b) = floor((a + f) / b) [3]
如果在行中[1]
您确定a = floor(x / y)
、f = (x / y) - floor(x / y)
和b = z
,则[3]
意味着[1]
和[2]
相等。
您可以将此证明推广到负整数(仍然忽略溢出),但我将把它留给读者以保持简单。
关于溢出问题- 请参阅 Eric Lippert 的回答以获得很好的解释!他还在他的博客文章和回答中采取了更加严格的方法,如果您觉得我过于随意,您应该研究一下。
b
如果和的绝对值c
低于约sqrt(2^31)
(约 46 300),b * c
则永远不会溢出,这些值将始终匹配。如果b * c
溢出,则可能会在checked
上下文中引发错误,或者您可能会在unchecked
上下文中获得不正确的值。
避免其他人注意到的溢出错误,它们总是匹配的。
让我们假设a/b=q1
,这意味着a=b*q1+r1
,在哪里0<=r1<b
。
现在假设a/b/c=q2
,这意味着q1=c*q2+r2
,在哪里0<=r2<c
。
这意味着a=b(c*q2+r2)+r1=b*c*q2+br2+r1
.
为了a/(b*c)=a/b/c=q2
,我们需要有0<=b*r2+r1<b*c
。
但是b*r2+r1<b*r2+b=b*(r2+1)<=b*c
,根据需要,并且这两个操作匹配。
b
如果或者是负数,这不起作用c
,但我也不知道整数除法在这种情况下是如何工作的。
我会提供我自己的证明来取乐。这也忽略了溢出,不幸的是只处理正面,但我认为证明是干净和清晰的。
目标是表明
floor(floor(x/y)/z) = floor(x/y/z)
哪里/
是正常除法(在整个证明中)。
a/b
我们将唯一的商和余数表示为a = kb + r
(我们的意思k,r
是唯一的并且也注释|r| < |b|
)。然后我们有:
(1) floor(x/y) = k => x = ky + r
(2) floor(floor(x/y)/r) = k1 => floor(x/y) = k1*z + r1
(3) floor(x/y/z) = k2 => x/y = k2*z + r2
所以我们的目标就是证明这一点k1 == k2
。那么我们有:
k1*z + r1 = floor(x/y) = k = (x-r)/y (from lines 1 and 2)
=> x/y - r/y = k1*z + r1 => x/y = k1*z + r1 + r/y
因此:
(4) x/y = k1*z + r1 + r/y (from above)
x/y = k2*z + r2 (from line 3)
现在从 (2) 观察它r1
是一个整数(根据定义,fork1*z
是一个整数)和r1 < z
(也是根据定义)。此外,从(1)我们知道r < y => r/y < 1
。现在考虑(4)的总和r1 + r/y
。声明是,r1 + r/y < z
这从前面的声明中很清楚(因为0 <= r1 < z
和r1
是一个整数,所以我们有0 <= r1 <= z-1
。因此0 <= r1 + r/y < z
)。因此r1 + r/y = r2
,根据定义r2
(否则将有两个与余数x/y
的定义相矛盾的余数)。因此我们有:
x/y = k1*z + r2
x/y = k2*z + r2
我们得到了我们想要的结论k1 = k2
。
上述证明应该适用于否定,除了您需要检查额外案例的几个步骤......但我没有检查。
反例:INT_MIN / -1 / 2