6.2 不変条件の原理

6.2.1 斜めにしか動けないロボット

座標 \((0, 0)\) に置かれたロボットが二次元格子を動き回る状況を考えよう。任意の時刻におけるロボットの状態は、ロボットの現在位置を表す整数座標 \((x, y)\) で特定できる。例えば初期状態は \((0, 0)\) である。各ステップでロボットは斜め四方のいずれかにのみ移動できるとする (図 \(\text{6.2}\))。

数学の言葉を使って正確に表現すれば、ロボットの移動をモデル化する状態機械の遷移関係は次の集合である:

例えば、最初のステップの後、ロボットは状態 \((1, 1)\), \((1, -1)\), \((-1, 1)\), \((-1, -1)\) のいずれかにある。そして二番目のステップの後、ロボットの状態には \((0, 0)\) を含めて \(9\) 個の可能性がある。では、次の問題を考えよう: ロボットは座標 \((1, 0)\) に到達できるだろうか？

ロボットを頭の中で少し動かしてみれば、ロボットは \(m+n\) が偶数であるような座標 \((m,n)\) にしか到達できないことに気が付くだろう。つまりロボットは和が奇数である座標 \((1,0)\) に到達できない。これが正しいと言えるのは、「座標の和が偶数」という性質が遷移の前後で保存されるからである。こういった性質を保存不変条件 (preserved invariant) と呼ぶ。

これから保存不変条件を使った議論を示す。数学的帰納法が使われる流れに注意して読んでほしい。最初に「座標の和が偶数」という性質を定義しておく:

この補題はロボットの遷移の定義 \((m, n) \to (m \pm 1, n \pm 1)\) から直ちに従う: 遷移による座標の和の変化は \(0\), \(2\), \(-2\) のいずれかであり、偶奇性は変化しない。後は遷移の回数に関する単純な数学的帰納法を使えば、次の定理を証明できる:

証明 ロボットが実行した遷移の回数に関する数学的帰納法で示す。次の述語 \(P(n)\) を帰納法の仮定とする:

ベースケース: ロボットが \(0\) 回の遷移で到達できるのは初期位置 \((0, 0)\) だけであり、その座標の和 \(0+0 = 0\) は偶数なので \(P(0)\) は成り立つ。

帰納ステップ: ある \(n\) で \(P(n)\) が成り立つと仮定する。\(r\) を \(n+1\) 回の遷移で到達できる任意の状態とする。\(\text{Even-sum}(r)\) が成り立つことを示せばよい。

状態 \(r\) には \(n + 1\) 回の遷移で到達できるので、その一つ前の状態 \(q\) には \(n\) 回の遷移で到達でき、さらに遷移 \(q \to r\) が存在する。よって帰納法の仮定 \(P(n)\) と補題 6.2.1 より \(\text{Even-sum}(r)\) も成立する。これで \(P(n) \ \operatorname{\text{\footnotesize IMPLIES}}\ P(n+1)\) が証明された。

数学的帰納法の原理より、全ての非負整数 \(n\) で「\(q\) が \(n\) 回の遷移で到達できる状態なら \(\text{Even-sum}(q)\)」が成り立つ。つまりロボットが到達できる全ての状態は「座標の和が偶数」という性質を満たす。 ■

証明 定理 6.2.2 より、ロボットは座標の和が偶数である位置にしか移動できない。つまり位置 \((1, 0)\) にも移動できない。 ■

6.2.2 不変条件の原理

保存不変条件 \(\text{Even-sum}\) を利用して斜め四方にしか動けないロボットの性質を証明する上記の議論は、本書が不変条件の原理 (invariant principle) と呼ぶ基礎的な証明技法の単純な例である。これは状態に達するまでのステップ数に関する数学的帰納法で不変条件を証明する技法を意味する。

状態機械の実行 (execution) とは、何らかの状態から始まる正当な遷移の列である:

不変条件の原理は第 5.1.1 項で示した数学的帰納法の原理を状態機械で使いやすいように言い換えたものに過ぎない。初期状態で述語が成り立つことの証明がベースケースに、述語が保存不変条件であることの証明が帰納ステップに対応する¹。

6.2.3 容器に水を入れる問題

こんな問題を考えよう: 水の入る空の容器が二つある。それぞれの容器の容量が \(5\) ガロンと \(3\) ガロンのとき、\(5\) ガロンの容器にちょうど \(4\) ガロンの水を入れることはできるだろうか？

状態機械によるモデル化

この問題は状態機械を使ってモデル化できる。この状態機械の状態は大きい容器と小さい容器に入っている水の量の組である。例えば、容器の容量がそれぞれ \(5\) ガロンと \(3\) ガロンのとき、状態は実数の組 \((b, l)\) であり、それぞれ \(0 \leq b \leq 5\) と \(0 \leq l \leq 3\) を満たす。最初二つの容器は空なので、初期状態は \((0, 0)\) である。

容器に入っている水の量が正確に分かる必要があるので、許される操作は「容器に水を満たす」と「容器に入っている全て捨てる」だけとなる。これらを状態の遷移に変換すると種類が若干増えて次のようになる:

1. 小さい容器を満たす:\(\quad\) \((b, l) \to (b, 3) \quad\) (\(l < 3\))

2. 大きい容器を満たす:\(\quad\) \((b, l) \to (5, l) \quad\) (\(b < 5\))

3. 小さい容器を空にする: \(\quad\) \((b, l) \to (b, 0) \quad\) (\(l > 0\))

4. 大きい容器を空にする: \(\quad\) \((b, l) \to (0, l) \quad\) (\(b > 0\))

5. 小さい容器から大きい容器に水を移す:

   \[ (b, l) \to \begin{cases} (b + l, 0) & b + l \leq 5 \text{ のとき} \\ (5, l-(5-b)) & \text{それ以外のとき} \end{cases} \]

6. 大きい容器から小さい容器に水を移す:

   \[ (b, l) \to \begin{cases} (0, b + l) & b + l \leq 3 \text{ のとき} \\ (b - (3-l), 3) & \text{それ以外のとき} \end{cases} \]

前節で示した \(99\) カウンターの状態機械のように任意の状態から出る遷移が \(1\) 個以下である状態機械を決定的 (deterministic) と呼ぶ。ここに示した状態機械は非決定的 (nondeterministic) である: 複数の遷移を持つ状態が存在する。

この状態機械で状態 \((4, 3)\) には次の遷移で到達可能なので、先述の問題の解答は「できる」だと分かる:

容量が \(9\) ガロンと \(3\) ガロンのとき

二つの容器の容量が \(9\) ガロンと \(3\) ガロンの場合にも同じことが言えるだろうか？ つまり、\(9\) ガロンの容器にちょうど \(4\) ガロンを入れることはできるだろうか？

実は、この設定では \((4, l)\) の形をした状態は到達可能でない。この事実を不変条件の原理を使って証明してみよう。まず、保存不変条件 \(P((b, l))\) を「\(b\) と \(l\) はどちらも \(3\) の非負整数倍である」と定める。

上述の状態機械で \(b = 9\), \(l = 3\) としたとき \(P\) が保存不変条件だと示すために、ある状態 \(q ::= (b, l)\) で \(P(q)\) が成り立つと仮定する。その上で遷移 \(q \to r\) が存在する任意の状態 \(r\) で \(P(r)\) が成り立つと示せばよい。この証明では遷移の定義に対応する場合分けを利用する。

まず「小さい容器を満たす」の遷移を考える。このとき \(r = (b, 3)\) である。\(P(q)\) が成り立つので、\(b\) は \(3\) の非負整数倍である。さらに \(3\) は当然 \(3\) の非負整数倍だから、\(P(r)\) は成り立つ。

続いて「大きい容器から小さい容器に水を移す」の遷移を考える。水を移した後小さい容器が満杯になるとき、つまり \(b + l > 3\) のときは \(r = (b - (3 - l), 3)\) である。\(P(q)\) の成立から \(b\) と \(l\) がどちらも \(3\) の非負整数倍と分かる。このとき \(b - (3 - l)\) も \(3\) の非負整数倍であり、\(P(r)\) は成り立つ。

他の場合も簡単にチェックできるので、ここでは省略する。後は不変条件の原理より、到達可能な全ての状態が \(P\) を満たすと分かる。そして \((4, l)\) の形をした状態が \(P\) を満たすことはないので、解答は「できない」だと結論できる！

ところで、状態 \((1, 0)\) は \(\operatorname{\text{\footnotesize NOT}} (P)\) を満たすものの、\(P\) を満たす状態 \((0, 0)\) への遷移を持つ。そのため一般に保存不変条件の否定は保存不変条件とならない。

この問題に対する一般的な解答は第 9.2.3 項で見る。