前置き
2の補数や2の補数表記を利用した加算・減算・乗算が、非負整数にとどまらず整数同士の演算でも辻褄が合っている事は自明ではないと思いました。かつ、自分に相性の良い記事を見つけられませんでした。よって、その辺を整理します。
辻褄が合っているとは
これから、数 $x \in \mathbb{Z} $ に対しbit列 $B_x$ を対応させていきます(機械は僕と違って2や3がわからないからです）。そこで $x + y$ や対応する $B_x + B_y$ を考えるわけですが、この時
$$\forall x, y \in \mathbb{Z}, \quad B_x + B_y = B_{x+y}...(1)$$
$$\forall x, y \in \mathbb{Z}, \quad B_x - B_y = B_{x-y}...(2)$$
$$\forall x, y \in \mathbb{Z}, \quad B_x \times B_y = B_{x \times y} ... (3)$$
が成立していないと明らかにおかしいです。逆に、これが成立していれば良いこともわかります。よって、この記事ではこの等式が実際の機械の $+, -, \times$ で成立している事を確認していきます。
前提
bit列の長さは全部 $w$ とする。
また、これからは上の2式の成立を言う事を目指すのでbit列と整数ある程度区別して考えます(気持ちの部分なのでよくわからなかったらこの文は無視してください)。
2の補数
$x\in \mathbb{Z}$ に対し、 $x$ の $2$ の補数 $x_c$ を
$$B_{x_c} = (\neg B_x) + B_1$$
を満たす $x_c$ と定義します。
注意: +は加算器による加算
符号なし整数
$x\in \mathbb{Z}$ とbit列 $B_x$ の対応を次で取ります。
$$ x' \equiv x \pmod {2^w} \quad かつ \quad 0 \le x' < 2^w となるx' の2進数表示を B_x とする。$$
bit列には $2$ 進数の加算と乗算が実装されてるとします。
命題: $\forall x, y, z$, 演算$・ \in {+, -, \times}$ について
$$x ・ y \equiv z \pmod {2^w} ⇔ B_{z} = B_{x ・ y} \dots (4)$$
証明: 明らか
よって今後は左辺の成立を言えば十分で、つまりbit列に対応する数が$\pmod {2^w}$ で一致を言えば良いです。
なお、非負整数同士の加算と乗算はそれぞれ(1), (3)を満たす様に実装されているとします（ここは2の補数と独立で、かつ桁溢れの挙動を考えると正しいです。)。
2の補数の性質(in 非負整数)
命題: $\forall x\in \mathbb{Z}, \quad x_c \equiv 2^w - x \pmod{2^w}$
証明:
$$\neg B_x = B_{2^w -1 - x}$$
$$\neg B_x + B_1 = B_{2^w -1 - x} + B_1$$
よって
$$ B_{x_c} = B_{2^w - x}$$
から成立。
以上より、次の命題がすぐにわかります。
命題: $\forall x\in \mathbb{Z}, \quad -x \equiv x_c \pmod{2^w}$
今後の非負整数に関する議論は全て、$\mathbb{Z}/ 2^w\mathbb{Z}$ において、$[-x] = [x_c]$ であることより直ちに成立と言っても良いと思います。つまり、加算の逆元をとる操作が補数を取る操作と同じと言う事です。
減算
$$ x - y $$
$$\equiv x + y_c \pmod{2^w} $$
よって(4) より
$$B_{x + y_c} = B_{x - y}$$
です。よって、 $B_y$ を補数表現 $B_{y_c}$ に直した上で加算機により $B_{x + y_c}$ を計算すれば $B_{x-y}$ が求まります。
以上より、2の補数を取って加算する様な減算は(2)を満たします。
乗算
正の整数同士の乗算は(3)が成立する様に実装されているとします。
$$ x \times(-y)$$
$$ \equiv x \times y_c \pmod{2^w}$$
より、この場合も$B_y$ を補数表現 $B_{y_c}$ に直した上で乗算機により $B_{x \times y_c}$ を計算する様な乗算は(3)を満たします。
よって、非負整数の演算では負の数は補数を取って計算すれば良い事がわかりました。
ここからが本題です。
符号付き整数
$\forall x\in \mathbb{Z}$ とbit列 $B_x$ の対応を次で取ります。
$$ x' \equiv x \pmod {2^w} \quad かつ \quad -2^{w-1} \le x' < 2^{w-1} となるx' を取る。$$
$$x' = -2^{w-1}B[w-1] + \sum_{i=0}^{w-2}2^{i}B[i] となる B を B_x と置く。$$
そして、bit列には $2$ 進数の加算が実装されてるとします(highest bitの重みが反転しているにも関わらず！)。そして、乗算は参考文献のものが実装されているとします。
補題: $\mod 2^w の代表元として [-2^{w-1}, 2^{w-1} - 1]$ が取れる
証明: 明らか
命題: $\forall x, y, z$, 演算$・ \in {+, -, \times}$ について
$$x ・ y \equiv z \pmod {2^w} ⇔ B_{z} = B_{x ・ y} \dots (4)$$
証明: 補題より明らか
よって、符号付き整数の演算の正当性を考える時も先ほどと同様に、bit列に対応する数が$\pmod {2^w}$ で一致を言えば良いです。
加算
2の補数を準備する前に、加算を終わらせておきます。
$\forall x, y \in \mathbb{Z} \quadに対し、 B_x + B_y = B_z$ が成立したとします。
ここで、
$$ -2^{w-1} \equiv 2^{w-1} \pmod{2^w} $$
より、2進の加算器の実装を考えると
$$ x + y \equiv z \pmod {2^w}$$
です。
よって、結局2進加算器による $+$ が (1) を満たしています。
2の補数の性質(in 整数)
命題:
命題: $\forall x \in \mathbb{Z}, \quad x_c \equiv - x \pmod{2^w}$
証明:
-
$x に対応する x'が\ge 0$ の時
$$\neg B_x = B_{2^{w-1}-1 - x -2^{w-1}}$$
$$\neg B_x = B_{-1-x}$$
$$\neg B_x + B_1 = B_{-1-x} + B_1$$
よって
$$ B_{x_c} = B_{-x}$$ -
$xに対応するx'が < 0$ の時
$$\neg B_x = B_{2^{w-1}-1 - (x + 2^{w-1})}$$
$$\neg B_x = B_{-1 - x}$$
$$ B_{x_c} = B_{-x}$$
より成立。
減算
非負整数の時と同じ議論をすれば良いです。
追記: 乗算
調べたところによると、補数が絡む乗算も正しく求まるように、非負整数と整数の乗算機は実装が異なっていそうです。符号拡張がどうのこうのという話まで出ていて、難しそうです。
ここで、補数が絡む乗算も正しく求まるとすると、
$$x \times -y \equiv x \times y_c \pmod{2^w} $$
より、 -をつける時は補数を取ってからかける様な実装が(3)を満たします。
おまけ: 未定義動作との関係
加算機が桁溢れを起こした時 $\mod 2^w$ で正しい値を返す実装になっているかと、オーバーフロウを未定義動作とするかには直接の関係は無いと思っています。
例えば、$4$ bit符号付き整数に対し、$-1 + 3$ を計算すると
$$ -1 = 1111$$
$$ 3 = 0011$$
より
$$1111 + 0011 = 0010(?)$$
を計算する事になり、これが桁が溢れるからと言って $\mod 2^w$ で正しい値を返す事を保証しない実装になっていると、 $-1 + 3$ すら正しく計算される保証がない事になります。
ここで行った議論も、演算に使用される $x, y \in \mathbb{Z} について、 x + y, x - y, x \times y$ がそれぞれ型の範囲に収まる様に関数の定義域を制限すれば、オーバーフロウを経由する事なく議論できます。ただ、すぐ上で注意した通り桁溢れは起きる事情の上、オーバーフロウと内部的な桁溢れを区別する(例: $\neg -2^{w-1} = -2^{w-1}$ in 整数 ですが、途中で $(2^{w-1} - 1) + 1 = -2^{w-1}$ を経由します）以上煩雑な場合分けが増えると思いますし、何より実態に沿っていないと思います。
終わりに
4時間後に期末テストが始まります。