6.3 部分正当性と停止性

Floydフロイドはプログラムを検証する上で必要になる性質を二つ考案した。一つ目の性質は部分正当性 (partial correctness) と呼ばれる。これは「プログラムが最終的な結果を出力するなら、それはシステムの要件を満たす」ことを意味する。

「部分正当なプログラムからは部分的にしか正当でない結果が得られるのか？」と思ったかもしれないが、それは Floyd が意味したことではない。部分正当性の「部分 (partial)」は、停止しない可能性のある処理を部分関係 (partial relation) の計算と捉えることを意味する。部分正当性は「もし結果が生成されるなら、それは正しい」ことを意味するに過ぎない。処理は無限ループに入って停止しないかもしれない。

二つ目の性質は停止性 (termination) と呼ばれる。これは処理が必ず最終的な結果を生成することを意味する。

部分正当性は不変条件の原理を使って、停止性は整列原理を使って証明されることが多い。これから高速冪乗の手続きを例として説明する。

6.3.1 高速冪乗

冪乗の計算

実数 \(a\) の \(b\) 乗を計算する最も単純な方法は、\(a\) に \(a\) を \(b-1\) 回乗じるものである。しかし、高速冪乗 (fast exponentiation) と呼ばれるアルゴリズムを使うと乗算の回数を大きく削減できる。高速冪乗アルゴリズムの定義をレジスタマシンプログラムとして次に示す。記号 \(x\), \(y\), \(z\), \(r\) は実数を保持するレジスタを表し、\(z := a\) の形をした代入文 (assignment statement) はレジスタ \(z\) の値を実数 \(a\) に置き換える操作を表す。

高速冪乗プログラム

入力を \(a \in \mathbb{R}\), \(b \in \mathbb{N}\) を受け取ったら、レジスタ \(x\), \(y\), \(z\) をそれぞれ \(a\), \(1\), \(b\) で初期化する。以降は次のステップを停止するまで繰り返す:

もし \(z = 0\) なら \(y\) を返して停止する。
\(r := \operatorname{remainder}(z, 2)\ \) (\(z\) を \(2\) で割った余り)
\(z := \operatorname{quotient}(z, 2)\ \) (\(z\) を \(2\) で割った商)
もし \(r = 1\) なら \(y := xy\)
\(x := x^{2}\)

このプログラムは必ず停止し、返り値が \(a^{b}\) であることをこれから証明する。まず、プログラムの振る舞いを状態機械でモデル化する:

\(\text{状態} ::= \mathbb{R} \times \mathbb{R} \times \mathbb{N}\)
\(\text{初期状態} ::= (a, 1, b)\)
遷移は次の規則で定義される:

\[ (x, y, z) \to \begin{cases} (x^{2},\ y, \ \operatorname{quotient}(z, 2)) & \ z \text{ が正の偶数のとき} \\ (x^{2},\ xy,\ \operatorname{quotient}(z, 2)) & \ z \text{ が正の奇数のとき} \end{cases} \]

述語 \(P((x, y, z))\) を次のように定義する:

\[ P((x, y, z)) \ \ \overset{\text{def}}{\longleftrightarrow}\ \ z \in \mathbb{N} \ \operatorname{\text{\footnotesize AND}} \ yx^{z} = a^{b} \tag{6.1}\]

\(P\) が保存不変条件だと示す。ある状態 \((x, y, z)\) で \(P((x, y, z))\) が成り立つと仮定し、\((x, y, z) \to (x_{t}, y_{t}, z_{t})\) を満たす状態 \((x_{t}, y_{t}, z_{t})\) を任意に取る。この上で \(P((x_{t}, y_{t}, z_{t}))\) を示せばよい。つまり証明すべきは次の命題である:

\[ z_{t} \in \mathbb{N} \ \operatorname{\text{\footnotesize AND}} \ y_{t}x_{t}^{z_{t}} = a^{b} \tag{6.2}\]

\((x, y, z)\) からの遷移が存在するので \(z \neq 0\) が分かる。また \(P((x, y, z))\) の成立から \(z \in \mathbb{N}\) も分かる。よって考える必要があるのは次の二つの場合だけである:

Case 1:

\(z\) が偶数のとき、遷移の定義から \(x_{t} = x^{2}\), \(y_{t} = y\), \(z_{t} = z/2\) を得る。よって \(z_{t} \in \mathbb{N}\) であり、さらに次の等式も分かる:

\[ \begin{aligned} y_{t} x_{t}^{z_{t}} &= y (x^{2})^{z/2} \\ &= yx^{2\cdot z / 2} \\ &= yx^{z} \\ &= a^{b} \qquad (P(x, y, z) \text{ の成立より}) \end{aligned} \]

Case 2:

\(z\) が奇数のとき、遷移の定義から \(x_{t} = x^{2}\), \(y_{t} = xy\), \(z_{t} = (z - 1)/2\) を得る。よって \(z_{t} \in \mathbb{N}\) であり、さらに次の等式も分かる:

\[ \begin{aligned} y_{t} x_{t}^{z_{t}} &= xy (x^{2})^{(z-1)/2} \\ &= yx^{1 + 2\cdot (z - 1) / 2} \\ &= yx^{1 + (z - 1)} \\ &= yx^{z} \\ &= a^{b} \qquad (P(x, y, z) \text{ の成立より}) \end{aligned} \]

両方の場合で等式 \(\text{(6.2)}\) が成り立つので、\(P\) は保存不変条件である。

ここまで来れば、部分正当性は簡単に証明できる。\(1\cdot a^{b} = a^{b}\) より初期状態 \((a, 1, b)\) は \(P\) を満たすので、不変条件の原理より \(P\) は全ての到達可能な状態で成り立つ。プログラムが停止するとき必ず \(z = 0\) であり、もし状態 \((x, y, 0)\) が到達可能なら \(y = y x^{0} = a^{b}\) である。つまり上記の高速冪乗プログラムが停止するときレジスタ \(y\) には \(a^{b}\) が格納される。

これで部分正当性が分かった。では停止性についてはどうだろうか？停止性の証明では、上記のプログラムによる \(a^{b}\) の計算で実行される乗算の回数が、\(b\) を二進数で表したときの桁数にほぼ等しい事実が利用される。つまり、ナイーブなアプローチだと乗算が \(b-1\) 回必要になるのに対して、高速冪乗だと約 \(\log b\) 回¹で済む。

より正確に言えば、\(b > 1\) のとき高速冪乗アルゴリズムは最大でも \(2 (\lceil \log b \rceil + 1)\) 回の乗算で \(a^{b}\) を計算する: レジスタ \(z\) の値は最初 \(b\) であり、反復ごとに半分以下になる。よって反復が最大で \(\lceil \log b \rceil + 1\) 回だけ実行された後 \(z\) の値が \(0\) になり、プログラムは停止する。これで停止性が分かった。各反復に乗算は \(2\) 回含まれるので、\(b > 0\) のとき \(z = 0\) となるまでに実行される乗算の総回数は \(2 (\lceil \log b \rceil + 1)\) と分かる (参照: 問題 6.6)。

6.3.2 誘導変数

乗算回数の上界の証明では、それぞれの状態に関連付く非負整数の値 \(z\) が小さくなり続けることを利用した。この値は状態の「サイズ」と理解できる。整列原理より、この「サイズ」が無限に小さくなり続けることはできない。言い換えれば、「サイズ」が最小値に到達するとプログラムは進行不能になる: つまり停止する。

これを一般化した「状態に値を関連付ける」テクニック ── 値が非負整数である必要はなく、遷移で必ず小さくならなくても構わない ── はアルゴリズムの解析で有用になる場合が多い。物理学には同じ役割を果たすポテンシャル関数 (potential function) という概念が存在する。アルゴリズム解析の文脈では、状態に関連付けられる値を誘導変数 (derived variable) と呼ぶ。

例えば前節で触れた水を入れる容器を使った問題では、二つの容器に入っている水の総量を表す誘導変数 \(f\colon \text{状態集合} \to \mathbb{R}\) を \(f((a, b)) ::= a + b\) と定義できる。同様に、斜め四方にしか動けないロボットの問題では、ロボットの \(x\) 座標を表す誘導変数 \(x\text{-coord}((i,j)) = i\) を定義できる。

状態機械の解析で役立つ誘導変数に関する標準的な性質がいくつかある。

定義 6.3.1

誘導変数 \(f\colon \text{状態集合} \to \mathbb{R}\) が狭義減少 (strictly decreasing) とは、次の関係が成り立つことを言う:

\[ \text{遷移 } q \to q^{\prime} \text{ が存在する} \ \operatorname{\text{\footnotesize IMPLIES}}\ f(q^{\prime}) < f(q) \]

同様に \(f\) が広義減少 (weakly decreasing) とは、次の関係が成り立つことを言う:

\[ \text{遷移 } q \to q^{\prime} \text{ が存在する} \ \operatorname{\text{\footnotesize IMPLIES}}\ f(q^{\prime}) \leq f(q) \]

狭義増加 (strictly increasing) と広義増加 (weakly increasing) も同様に定義される²。

高速冪乗プログラムの停止性の証明では、値域が非負整数の誘導変数 \(z\) が狭義減少である事実を利用した。このアプローチによる停止性の証明を次の定理にまとめる:

定理 6.3.2

値域が \(\mathbb{N}\) で狭義減少な誘導変数 \(f\) が状態機械に存在するなら、\(q\) から始まる任意の実行の長さは \(f(q)\) 以下である。

もちろん定理 6.3.2 は \(f(q)\) の値に関する数学的帰納法で証明できる。ただ、この定理は「非負整数 \(f(q)\) から初めて一つ前のものより小さい非負整数を順に書いていくとき、非負整数は最大でも \(f(q)\) 個しか書けない」と言い換えられる。このように表現すれば、正しさは明らかである。

6.3.3 整列集合を使った停止性の証明 [スキップ可]

定理 6.3.2 は値域が整列集合 (第 2.4 節) の誘導変数に自然に拡張できる:

定理 6.3.3

値域が整列集合で狭義減少な誘導変数 \(f\) が状態機械に存在するなら、\(q\) から始まる任意の実行は有限長である。

定理 6.3.3 は実数の集合が整列なのは無限減少列が含まれないとき、かつそのときに限る事実 (問題 2.23) から直ちに従う。

広義減少な誘導変数が存在するだけではプログラムの任意の実行が停止するとは言えない事実に注意してほしい。誘導変数が同じ値を取る状態だけからなる無限長の実行は広義減少である。

6.3.4 北東から迫り来るロボット [スキップ可]

値域が整列集合の誘導変数を使って停止性を証明する、わざとらしい単純な例を一つ示す。座標が非負整数の二次元格子を動き回るロボットを考えよう。位置 \((x ,y)\) にいるロボットが次に移動できる位置は次のいずれかだとする:

\(1\) 単位だけ西 ── つまり \(x > 0\) のとき \((x, y) \to (x-1, y)\)
\(1\) 単位だけ南、そして任意の距離だけ東 ── つまり \(y > 0\) のとき \(z \geq x\) に対して \((x, y) \to (z, y - 1)\)

この規則があるとき、ロボットは \(x\) 座標または \(y\) 座標が負になる位置に移動できない。さらに、次の命題が成り立つ:

主張 6.3.4

上記のロボットは必ずどこかの時点で原点 \((0, 0)\) に到達し、動けなくなる。

ロボットを非決定性の状態機械と捉えれば、主張 6.3.4 は停止性の表明となる。この主張は明らかだと思うかもしれないが、実は値域が非負整数の誘導変数を使うアプローチでは示せない。例えば位置 \((0, 1)\) にいるロボットが動けなくなるまでの時間に上界はない: 次の移動でいくらでも東に移動できるので、動けなくなるまでの時間を好きなだけ伸ばすことができる。このため定理 6.3.2 と全く同じ方法では停止性を証明できない。

この説明を聞いた後でも、主張 6.3.4 は明らかだろうか？

トリックが分かれば明らかである。ロボットの位置 \((x, y)\) を状態として、状態集合から整列集合 \(\mathbb{N} + \mathbb{F}\) (補題 2.4.6) への誘導変数 \(v\) を次のように定める:

\[ v((x, y)) ::= y + \frac{x}{x+1} \]

このとき容易に分かるように、\((x, y) \to (x^{\prime}, y^{\prime})\) が可能なロボットの移動のとき \(v((x^{\prime},y^{\prime})) < v((x, y))\) が成り立つ。つまり \(v\) は狭義減少な誘導変数である。よって定理 6.3.3 より、いずれロボットは原点に到達してそれ以上動けなくなると分かる ── ただし動けなくなるまでの移動回数については何も言えない。

情報科学でよくあるように、\(\log b\) は \(2\) を底とする対数 \(\log_{2} b\) を意味する。自然対数 \(\log_{e} b\) は \(\ln b\) と表記し、それ以外の対数では \(\log_{10} b\) などと底を明示する。 ↩︎
広義増加を非減少 (nondecreasing) と呼ぶこともある。ただ、この用語は本書で利用しない。「減少でない (狭義減少でも広義減少でもない)」は「広義増加である」よりずっと弱い条件である。 ↩︎