乘法分配律对无符号数与补码成立的证明

注：本节内容为 CS:APP 第三版中文版的批注。

引言

阅读第二章的时候发现书中使用了多次乘法的分配律，无论是无符号数还是补码数，然而并没有证明过这样做的正确性。本文将对其做一定的讨论。

无符号数

已知 $U_{\min} \leq x, y, y_1, y_2 \leq U_{\max}$ 且 $y = y_1 +_w^u y_2$，

求证：

$$
x *_w^u y = (x *_w^u y_1) +_w^u (x *_w^u y_2)
$$

证明：

$$
\begin{aligned}
&(x *_w^u y_1) +_w^u (x *_w^u y_2) \\
=&(x\cdot y_1 \pmod {2^w}) +_w^u (x\cdot y_2 \pmod {2^w}) \\
=&((x\cdot y_1 \pmod {2^w}) + (x\cdot y_2 \pmod {2^w})) \pmod {2^w} \\
=&(x\cdot y_1 + x\cdot y_2) \pmod {2^w} \\
=&x\cdot (y_1 + y_2) \pmod {2^w} \\
=&x\cdot ((y_1 + y_2) \pmod {2^w}) \pmod {2^w} \\
=&x\cdot (y_1 +_w^u y_2) \pmod {2^w} \\
=&x\cdot y \pmod {2^w} \\
=&x *_w^u y
\end{aligned}
$$

补码

已知 $T_{\min} \leq x, y, y_1, y_2 \leq T_{\max}$ 且 $y = y_1 +_w^t y_2$，

求证：

$$
x *_w^t y = (x *_w^t y_1) +_w^t (x *_w^t y_2)
$$

证明：

$$
\begin{aligned}
&(x *_w^t y_1) +_w^t (x *_w^t y_2) \\
=&[U2T(xy_1 \pmod {2^w})] {\color{skyblue}{+_w^t}} [U2T(xy_2 \pmod {2^w})] \\
=&U2T[{\color{skyblue}{T2U[U2T}}(xy_1 \pmod {2^w})] +_w^u {\color{skyblue}{T2U[U2T}}(xy_2 \pmod {2^w})]] \\
=&U2T[(xy_1 \pmod {2^w}) +_w^u (xy_2 \pmod {2^w})] \\
=&U2T[x(y_1 + y_2) \pmod {2^w}] \\
=&U2T[x(y_1 +_w^t y_2 + k2^w) \pmod {2^w}], k \in \mathbb{Z} \\
=&{\color{pink}{U2T[x(y + k2^w) \pmod {2^w}]}} \\
=&U2T[xy \pmod {2^w}] \\
=&x *_w^t y
\end{aligned}
$$

得证。

下面是上面公式粉红色部分的详细推导：

$$
y = y_1 +_w^t y_2 = U2T(T2U(y_1) + T2U(y_2))
$$

$$
y = \begin{cases}
y_1 + y_2 & y_1 + y_2 \in [T_{\min}, T_{\max}] \\
y_1 + y_2 + 2^w & y_1 + y_2 < T_{\min} \\
y_1 + y_2 - 2^w & y_1 + y_2 > T_{\max}
\end{cases}
$$

故：

$$
y = y_1 + y_2 - k2^w, k \in \mathbb Z
$$