アルゴリズムの正しさ(部分正当性と停止性)
概要
アルゴリズムの正しさ(部分正当性と停止性)（correctness of algorithms）とは、事前条件を満たす入力から始めると計算が止まり、結果が事後条件を満たすことであり、止まれば正しいという部分正当性と、必ず止まるという停止性からなる。ループの部分正当性は、事前条件から成り立ち、本体の 1 回の実行で保たれ、ループを抜けたときに事後条件を導くループ不変条件があることから従う。停止性は、繰り返しのたびに整礎な順序で真に減る変量があることから従う。正しいループには必ず不変条件（最弱の事前条件）と変量（繰り返しの回数）があり、この方法は完全である。
前提知識: 整礎関係, 数学的帰納法と整列性, Euclidの互除法
アルゴリズムが 正しい とは、決められた条件を満たす入力から始めると、計算が止まり、止まったときの結果が求める条件を満たすことである。この主張は 2 つに分かれる。止まったならば結果が正しいという 部分正当性（partial correctness）と、必ず止まるという 停止性 である。両方を合わせたものを 完全正当性（total correctness）という。
繰り返し（ループ）を含むアルゴリズムでは、繰り返しの回数が入力によって変わるので、実行を 1 歩ずつ追って確かめることはできない。そこで部分正当性は ループ不変条件（loop invariant）、つまり繰り返しの各回の前後で保たれる条件を見つけて示し、停止性は繰り返しのたびに真に減る 変量（variant）を整礎な順序の中に見つけて示す。不変条件の議論は繰り返しの回数に関する帰納法であり、変量の議論は 整礎関係 の上の帰納法である。この方法は Floyd が流れ図に注釈を付ける形で始め、Hoare が構造化されたプログラムの推論規則として整えた（NK14 §12.6.1）。
この記事では、整数の変数だけをもつ小さなプログラムの言語で正しさを定義し、不変条件と変量の方法が正しいこと（健全性）と、正しいループには必ず不変条件と変量があること（完全性）を証明する。例として Euclid の互除法と高速な冪の計算の正しさを示し、条件を 1 つ外すと結論が崩れる反例を挙げる。
プログラムと実行
アルゴリズムを、次の小さな言語のプログラムとして書く。変数の有限集合 $\mathrm{Var}$ を固定し、状態 を写像 $s\colon\mathrm{Var}\to\mathbb Z$ とする。状態の全体を $\Sigma$ と書く。
- 式 $e$ は整数の定数と変数から $+,-,\times$ と $\operatorname{div},\operatorname{mod}$ で作る。状態 $s$ での値を $[\![e]\!]s\in\mathbb Z$ と書く。$n\ne0$ のとき $m\operatorname{div}n:=\lfloor m/n\rfloor$、$m\operatorname{mod}n:=m-n\lfloor m/n\rfloor$ とし、$n=0$ のときはどちらも $0$ と約束する。
- 条件 $b$ は式の比較 $e< e'$、$e=e'$ から $\lnot,\land$ で作る。状態 $s$ で真か偽かが決まる。
- プログラム $c$ を
$$ c::=\mathbf{skip}\mid x:=e\mid c_1;c_2\mid\mathbf{if}\ b\ \mathbf{then}\ c_1\ \mathbf{else}\ c_2\mid\mathbf{while}\ b\ \mathbf{do}\ c $$
で定める。 - 実行 の関係 $\langle c,s\rangle\Downarrow t$（$c$ を状態 $s$ から実行すると止まり、状態 $t$ になる）を、次の規則で生成される最小の関係とする。$s[x\mapsto n]$ は $x$ の値だけを $n$ に替えた状態である。
- $\langle\mathbf{skip},s\rangle\Downarrow s$、$\langle x:=e,s\rangle\Downarrow s[x\mapsto[\![e]\!]s]$。
- $\langle c_1,s\rangle\Downarrow s'$ かつ $\langle c_2,s'\rangle\Downarrow t$ なら $\langle c_1;c_2,s\rangle\Downarrow t$。
- $b$ が $s$ で真で $\langle c_1,s\rangle\Downarrow t$ なら $\langle\mathbf{if}\ b\ \mathbf{then}\ c_1\ \mathbf{else}\ c_2,s\rangle\Downarrow t$。偽なら $c_2$ について同じ。
- $b$ が $s$ で偽なら $\langle\mathbf{while}\ b\ \mathbf{do}\ c,s\rangle\Downarrow s$。$b$ が $s$ で真で、$\langle c,s\rangle\Downarrow s'$ かつ $\langle\mathbf{while}\ b\ \mathbf{do}\ c,s'\rangle\Downarrow t$ なら $\langle\mathbf{while}\ b\ \mathbf{do}\ c,s\rangle\Downarrow t$。
止まらない実行は、どの $t$ についても $\langle c,s\rangle\Downarrow t$ にならないことで表される。たとえば $\mathbf{while}\ 0=0\ \mathbf{do}\ \mathbf{skip}$ はどの状態からも止まらない。実際、$\langle\mathbf{while}\ 0=0\ \mathbf{do}\ \mathbf{skip},s\rangle\Downarrow t$ の導出があれば、最後の規則は真の場合で、その前提に同じ形のより短い導出が現れるので、導出の長さについての帰納法で矛盾する。
$\langle c,s\rangle\Downarrow t$ かつ $\langle c,s\rangle\Downarrow t'$ ならば $t=t'$ である。
$\langle c,s\rangle\Downarrow t$ の導出に関する帰納法で、任意の $t'$ について示す。
詳細
$\mathbf{skip}$ と代入では $t$ が $s$ から一意に決まる。$c_1;c_2$ では、$\langle c_1,s\rangle\Downarrow s_1$、$\langle c_2,s_1\rangle\Downarrow t$ と $\langle c_1,s\rangle\Downarrow s_1'$、$\langle c_2,s_1'\rangle\Downarrow t'$ について、帰納法の仮定から $s_1=s_1'$、続いて $t=t'$ である。$\mathbf{if}$ では $b$ の真偽が $s$ で決まるので同じ枝が使われ、帰納法の仮定から $t=t'$ である。$\mathbf{while}$ で $b$ が偽なら $t=t'=s$ である。真なら、どちらの導出も真の場合の規則で終わり、$\langle c,s\rangle\Downarrow s_1$ と $\langle c,s\rangle\Downarrow s_1'$ から $s_1=s_1'$、$\langle\mathbf{while}\ b\ \mathbf{do}\ c,s_1\rangle$ の 2 つの導出から $t=t'$ を得る。$\square$
部分正当性と完全正当性
状態の性質を、それを満たす状態の集合 $P\subset\Sigma$ として扱い、$s\in P$ を「$s$ は $P$ を満たす」と読む。$P\land Q$ は共通部分、$P\Rightarrow Q$ は $P\subset Q$ のことである。条件 $b$ も、$b$ が真になる状態の集合と同一視する。
$P,Q\subset\Sigma$ とプログラム $c$ について、次のように定める。$P$ を 事前条件、$Q$ を 事後条件 という。
- $\{P\}\,c\,\{Q\}$ が 部分正当 であるとは、$s\in P$ と $\langle c,s\rangle\Downarrow t$ を満たす任意の $s,t$ について $t\in Q$ となることをいう。
- $c$ が $P$ の上で 停止する とは、任意の $s\in P$ について $\langle c,s\rangle\Downarrow t$ となる $t$ が存在することをいう。
- $[P]\,c\,[Q]$ が 完全正当 であるとは、任意の $s\in P$ について、$\langle c,s\rangle\Downarrow t$ かつ $t\in Q$ となる $t$ が存在することをいう。
$[P]\,c\,[Q]$ が完全正当であることと、$\{P\}\,c\,\{Q\}$ が部分正当で $c$ が $P$ の上で停止することは同値である。
後者から前者は、停止性で得た $t$ が部分正当性により $Q$ に属することから従う。前者から後者を示す。停止性は定義から明らかである。$s\in P$、$\langle c,s\rangle\Downarrow t'$ とすると、完全正当性から $\langle c,s\rangle\Downarrow t$、$t\in Q$ となる $t$ があり、lem-ac-deterministic により $t'=t\in Q$ である。$\square$
部分正当性だけでは、止まらないプログラムも正しいことになる。$c_0:=\mathbf{while}\ 0=0\ \mathbf{do}\ \mathbf{skip}$ は止まらないので、どんな $P,Q$ についても $\{P\}\,c_0\,\{Q\}$ が部分正当である。たとえば事後条件を空集合にした $\{\Sigma\}\,c_0\,\{\emptyset\}$ も部分正当であり、部分正当性の主張は「止まったならば」という条件付きの主張にすぎない。
ループを含まない部分は、次の規則で事後条件から事前条件へさかのぼって確かめられる。$Q[e/x]:=\{s\in\Sigma\mid s[x\mapsto[\![e]\!]s]\in Q\}$ とおく。
- （代入）$\{Q[e/x]\}\,x:=e\,\{Q\}$ は部分正当である。
- （合成）$\{P\}\,c_1\,\{R\}$ と $\{R\}\,c_2\,\{Q\}$ が部分正当なら、$\{P\}\,c_1;c_2\,\{Q\}$ も部分正当である。
- （条件分岐）$\{P\land b\}\,c_1\,\{Q\}$ と $\{P\land\lnot b\}\,c_2\,\{Q\}$ が部分正当なら、$\{P\}\,\mathbf{if}\ b\ \mathbf{then}\ c_1\ \mathbf{else}\ c_2\,\{Q\}$ も部分正当である。
- （帰結）$P'\subset P$、$\{P\}\,c\,\{Q\}$ が部分正当、$Q\subset Q'$ なら、$\{P'\}\,c\,\{Q'\}$ も部分正当である。
どれも、部分正当を完全正当に、$\{\ \}$ を $[\ ]$ に読み替えても成り立つ。
どれも def-ac-program の実行の規則をそのまま読めばよい。
詳細
1：$s\in Q[e/x]$ で $\langle x:=e,s\rangle\Downarrow t$ なら $t=s[x\mapsto[\![e]\!]s]$ であり、$Q[e/x]$ の定義から $t\in Q$ である。2：$\langle c_1;c_2,s\rangle\Downarrow t$ の導出の最後は合成の規則なので、$\langle c_1,s\rangle\Downarrow s'$、$\langle c_2,s'\rangle\Downarrow t$ となる $s'$ がある。$s\in P$ なら $s'\in R$、続いて $t\in Q$ である。3：$s\in P$ で $b$ が $s$ で真なら、導出の最後は真の枝の規則で $\langle c_1,s\rangle\Downarrow t$ であり、$s\in P\land b$ から $t\in Q$ である。偽なら $c_2$ について同じ。4：$s\in P'$ なら $s\in P$ なので $t\in Q\subset Q'$ である。
完全正当の場合：1 は $t=s[x\mapsto[\![e]\!]s]$ が存在するので同じ。2 は $s\in P$ から $\langle c_1,s\rangle\Downarrow s'$、$s'\in R$ となる $s'$ をとり、さらに $\langle c_2,s'\rangle\Downarrow t$、$t\in Q$ となる $t$ をとって合成の規則を当てる。3・4 も同様である。$\square$
ループ不変条件
$w:=\mathbf{while}\ b\ \mathbf{do}\ c$ とする。$w$ の実行は、$b$ が真である間 $c$ を繰り返し、$b$ が偽になった状態で止まる。
$I\subset\Sigma$ が $w=\mathbf{while}\ b\ \mathbf{do}\ c$ の ループ不変条件 であるとは、$\{I\land b\}\,c\,\{I\}$ が部分正当であること、すなわち $I$ と $b$ を満たす状態から本体 $c$ を実行して止まれば、再び $I$ を満たすことをいう。
定義は、実際に到達する状態だけでなく、$I\land b$ を満たすすべての状態について維持を求めている（帰納的な不変条件ともいう）。この強さがあるので、次の定理を繰り返しの回数に関する帰納法で証明できる。
$I$ が $w=\mathbf{while}\ b\ \mathbf{do}\ c$ のループ不変条件なら、$\{I\}\,w\,\{I\land\lnot b\}$ は部分正当である。
$\langle w,s\rangle\Downarrow t$ の導出に関する帰納法で、「$s\in I$ ならば $t\in I\land\lnot b$」を示す。
詳細
導出の最後の規則で場合を分ける。$b$ が $s$ で偽の場合、$t=s$ であり、$s\in I$ かつ $b$ が $t$ で偽なので $t\in I\land\lnot b$ である。$b$ が $s$ で真の場合、$\langle c,s\rangle\Downarrow s'$ と $\langle w,s'\rangle\Downarrow t$ となる $s'$ があり、後者の導出は全体より短い。$s\in I\land b$ と不変条件の仮定から $s'\in I$ であり、短い導出についての帰納法の仮定から $t\in I\land\lnot b$ である。$\square$
$P,Q\subset\Sigma$ と $I\subset\Sigma$ が次の 3 つを満たせば、$\{P\}\,w\,\{Q\}$ は部分正当である。
- （初期化）$P\subset I$。
- （維持）$\{I\land b\}\,c\,\{I\}$ が部分正当。
- （終了時）$I\land\lnot b\subset Q$。
2 と thm-ac-while により $\{I\}\,w\,\{I\land\lnot b\}$ は部分正当である。1・3 と prop-ac-rules の 4（帰結）で事前条件を $P$ に、事後条件を $Q$ に替えればよい。$\square$
不変条件 $I$ は、プログラムが何を計算しているかを「途中の状態」について述べたものである。終了時の条件 3 から、$I$ は事後条件 $Q$ を導くだけの強さをもたねばならず、維持の条件 2 から、本体の 1 回の実行で壊れない形でなければならない。多くの場合、$Q$ の中の定数（入力の値）を変数の現在の値で置き換えて一般化したものが $I$ の候補になる（ex-ac-euclid・ex-ac-power）。
停止性と変量
ループが止まることは、繰り返しのたびに真に減り、しかも無限に減り続けることのない量を見つけて示す。「無限に減り続けない」ことを正確に言うのが整礎性である（整礎関係 の定義「整礎関係」）。
$w=\mathbf{while}\ b\ \mathbf{do}\ c$ と $I\subset\Sigma$ について、集合 $W$ 上の整礎関係 $\prec$ と写像 $V\colon\Sigma\to W$ の組が $I$ のもとでの $w$ の 変量（variant、ranking function ともいう）であるとは、$I\land b$ を満たす任意の状態 $s$ について、$\langle c,s\rangle\Downarrow s'$、$s'\in I$、$V(s')\prec V(s)$ を満たす状態 $s'$ が存在することをいう。
$W=\mathbb Z_{\ge0}$ と通常の $<$ をとることが多い。条件は、本体 $c$ そのものが止まることと、止まったあとで $I$ が保たれ $V$ が真に減ることを合わせて要求している。
$I$ のもとでの $w=\mathbf{while}\ b\ \mathbf{do}\ c$ の変量 $(W,\prec,V)$ があれば、$[I]\,w\,[I\land\lnot b]$ は完全正当である。
$W$ の元 $v$ についての主張「$V(s)=v$ を満たす任意の $s\in I$ について、$\langle w,s\rangle\Downarrow t$、$t\in I\land\lnot b$ となる $t$ がある」を、整礎帰納法で示す。
詳細
この主張が成り立つ $v$ の全体を $P\subset W$ とし、$v'\prec v$ となる $v'$ がすべて $P$ に属すると仮定して $v\in P$ を示す（整礎関係 の定理「整礎帰納法」の (b)）。$s\in I$、$V(s)=v$ とする。$b$ が $s$ で偽なら、$t:=s$ について $\langle w,s\rangle\Downarrow s$ で、$s\in I\land\lnot b$ である。$b$ が $s$ で真なら、変量の条件から $\langle c,s\rangle\Downarrow s'$、$s'\in I$、$V(s')\prec v$ となる $s'$ がある。$V(s')\in P$ なので、$\langle w,s'\rangle\Downarrow t$、$t\in I\land\lnot b$ となる $t$ があり、実行の規則（$\mathbf{while}$ の真の場合）から $\langle w,s\rangle\Downarrow t$ である。よって $v\in P$ となり、整礎帰納法により $P=W$ である。$s\in I$ には $v:=V(s)$ を当てればよい。$\square$
cor-ac-three-checks と合わせると、初期化 $P\subset I$、変量の条件、終了時 $I\land\lnot b\subset Q$ から $[P]\,w\,[Q]$ が完全正当であることが従う（prop-ac-rules の 4 を完全正当に読み替えたもの）。$W$ を $\mathbb Z_{\ge0}\times\mathbb Z_{\ge0}$ の辞書式順序にとれば（整礎関係 の命題「逆像・推移閉包・辞書式の積」の 3）、外側の量が減るか、外側が変わらず内側が減る、という形の停止性の議論もこの定理に含まれる。
方法の完全性
不変条件と変量の方法は、正しいループならいつでも使える。つまり、正しいループには必ず不変条件と変量がある。
$\{P\}\,w\,\{Q\}$ が部分正当であるとする。
$$
I:=\{s\in\Sigma\mid \langle w,s\rangle\Downarrow t\ \text{となる任意の}\ t\ \text{について}\ t\in Q\}
$$
とおくと、$I$ は cor-ac-three-checks の 3 つの条件を満たす。
初期化は部分正当性の言い換えである。維持と終了時は、$w$ の実行の規則を 1 段ほどけばよい。
詳細
初期化：$s\in P$ で $\langle w,s\rangle\Downarrow t$ なら部分正当性から $t\in Q$ なので $s\in I$ である。維持：$s\in I\land b$、$\langle c,s\rangle\Downarrow s'$ とする。$\langle w,s'\rangle\Downarrow t$ なら、$b$ が $s$ で真なので実行の規則から $\langle w,s\rangle\Downarrow t$ であり、$s\in I$ から $t\in Q$ である。よって $s'\in I$ である。終了時：$s\in I$ で $b$ が $s$ で偽なら $\langle w,s\rangle\Downarrow s$ なので、$s\in Q$ である。$\square$
この $I$ は、$w$ の実行が止まれば $Q$ に入る状態の全体で、$w$ と $Q$ に対する 最弱の事前条件（weakest liberal precondition）と呼ばれる。初期化の確かめと同じ議論で、$\{P'\}\,w\,\{Q\}$ が部分正当になる $P'$ はどれも $I$ に含まれ、$I$ 自身も $\{I\}\,w\,\{Q\}$ を部分正当にする。つまり $I$ はそのような事前条件のうちで最大のものである。
$I$ が $w=\mathbf{while}\ b\ \mathbf{do}\ c$ のループ不変条件で、$w$ が $I$ の上で停止するとする。$s\in I$ について、$s_0:=s$ から始めて、$b$ が $s_k$ で真である間 $\langle c,s_k\rangle\Downarrow s_{k+1}$ で $s_{k+1}$ を定めると、$b$ が偽になる最初の番号 $N(s)$ が存在する。$V(s):=N(s)$（$s\notin I$ では $V(s):=0$）とおくと、$(\mathbb Z_{\ge0},<,V)$ は $I$ のもとでの $w$ の変量である。
$\langle w,s\rangle\Downarrow t$ の導出に関する帰納法で、列が有限で止まり $N(s)$ が定まることを示し、$N(s')=N(s)-1$ を確かめる。
詳細
lem-ac-deterministic により、列 $s_0,s_1,\dots$ は定まる限り一意である。「$s\in I$ かつ $\langle w,s\rangle\Downarrow t$ なら、ある $n$ について $s_0,\dots,s_n$ が定まり、$b$ は $s_0,\dots,s_{n-1}$ で真、$s_n$ で偽で、$t=s_n$」を導出に関する帰納法で示す。$b$ が $s$ で偽なら $n=0$ である。真なら、導出は $\langle c,s\rangle\Downarrow s'$ と $\langle w,s'\rangle\Downarrow t$ を前提にもち、決定性から $s'=s_1$ である。不変条件から $s_1\in I$ であり、短い導出についての帰納法の仮定を $s_1$ から始まる列（それはもとの列を 1 つずらしたもの）に当てると、ある $m$ で $b$ が初めて偽になるので、$n:=m+1$ でよい。
停止性の仮定から、$s\in I$ には $\langle w,s\rangle\Downarrow t$ となる $t$ があるので、$N(s)$ が定まる。$s\in I\land b$ なら $N(s)\ge1$ で、$s'=s_1$ は $\langle c,s\rangle\Downarrow s'$、$s'\in I$ を満たし、$s'$ から始まる列はもとの列を 1 つずらしたものなので $N(s')=N(s)-1< N(s)$ である。$\square$
完全正当性についても同じことが言える。$[P]\,w\,[Q]$ が完全正当なら、$J:=\{s\in\Sigma\mid\langle w,s\rangle\Downarrow t$ かつ $t\in Q$ となる $t$ がある$\}$ は $P$ を含み、$J\land\lnot b\subset Q$ を満たす。$s\in J\land b$ なら $w$ の導出の前提から $\langle c,s\rangle\Downarrow s'$、$\langle w,s'\rangle\Downarrow t$ となる $s'$ があり（lem-ac-deterministic により $c$ の結果は $s'$ だけ）、$s'\in J$ なので、$J$ はループ不変条件で、$w$ は $J$ の上で停止する。よって thm-ac-count の変量がとれる。
2 つの定理は、最弱の事前条件を不変条件に、繰り返しの回数を変量にとれば、正しいループの証明がいつも thm-ac-while と thm-ac-variant でできることを示している（同じ考え方で、Hoare 論理の推論規則の完全性が示される。NK14 §12.3、§12.5）。ただしこれは状態の集合として不変条件が存在するという意味であって、それを論理式で書けること、まして機械的に見つけられることまでは保証しない。Turing 機械が止まるかどうかは一般には判定できない（停止問題 の定理「停止問題の決定不能性」）。この形の言語でも同様で、どの状態からも止まらないプログラム、すなわち $\{\Sigma\}\,c\,\{\emptyset\}$ が部分正当になるプログラム $c$ の全体は帰納的に数え上げられない（NK14 §12.3.2。この記事では証明しない）。そのため、事前条件と事後条件を論理式で書いた部分正当な三つ組の全体を数え上げる手続きもない（同所）。実際の証明では、不変条件と変量はアルゴリズムの考え方から人が選ぶ。
例
変数 $a,b,r$ について、
$$
E:=\mathbf{while}\ \lnot(b=0)\ \mathbf{do}\ (r:=a\operatorname{mod}b;\ a:=b;\ b:=r)
$$
とする。整数 $A,B\ge0$ を固定し、$P:=\{a=A,\ b=B\}$、$Q:=\{a=\gcd(A,B)\}$ とおく（$\gcd(0,0)=0$ と約束する）。不変条件と変量を
$$
I:=\{a\ge0,\ b\ge0,\ \gcd(a,b)=\gcd(A,B)\},\qquad V(s):=\max(s(b),0)\in\mathbb Z_{\ge0}
$$
にとると、$[P]\,E\,[Q]$ は完全正当である。証明は Euclidの互除法 の定理「互除法の停止と正しさ」の証明を、不変条件と変量の言葉で書き直したものになる。
確かめを開く
初期化：$A,B\ge0$ なので $P\subset I$ である。変量の条件：$s\in I$、$s(b)\ne0$ とし、$a:=s(a)\ge0$、$b:=s(b)>0$ と書く。本体は止まり、$r=a\operatorname{mod}b=a-bq$（$q=\lfloor a/b\rfloor$）は $0\le r< b$ を満たす。実行後の値は $(a,b)\mapsto(b,r)$ で、$b\ge0$、$r\ge0$ であり、$a$ と $b$ の公約数と $b$ と $r=a-bq$ の公約数は同じなので $\gcd(b,r)=\gcd(a,b)=\gcd(A,B)$ である。よって実行後の状態は $I$ を満たし、$V$ は $b$ から $r< b$ に減る。thm-ac-variant から $[I]\,E\,[I\land(b=0)]$ が完全正当である。終了時：$b=0$、$a\ge0$ なら $\gcd(a,0)=a$ なので $a=\gcd(A,B)$ である。
不変条件は、事後条件 $a=\gcd(A,B)$ の左辺の $a$ を「いまの組 $(a,b)$ の最大公約数」に一般化したものである。$b=0$ のとき $\gcd(a,b)=a$ となることが、終了時の条件を満たす鍵になっている。
変数 $x,n,r$ について、
$$
F:=r:=1;\ \mathbf{while}\ 0< n\ \mathbf{do}\ \bigl((\mathbf{if}\ n\operatorname{mod}2=1\ \mathbf{then}\ r:=r\times x\ \mathbf{else}\ \mathbf{skip});\ x:=x\times x;\ n:=n\operatorname{div}2\bigr)
$$
とする。整数 $X$ と $M\ge0$ を固定し、$P:=\{x=X,\ n=M\}$、$Q:=\{r=X^M\}$ とおく（$X^0=1$）。ループの不変条件と変量を
$$
I:=\{n\ge0,\ r\cdot x^n=X^M\},\qquad V(s):=\max(s(n),0)
$$
にとると、$[P]\,F\,[Q]$ は完全正当である。ループは $n$ の 2 進展開の桁数だけ回る。
確かめを開く
初期化：$r:=1$ の実行後の状態は $x=X$、$n=M\ge0$、$r=1$ なので $r\cdot x^n=X^M$ を満たす（prop-ac-rules の 1・2）。変量の条件：$I$ を満たし $n>0$ の状態で、$n=2k+\varepsilon$（$k=n\operatorname{div}2$、$\varepsilon=n\operatorname{mod}2\in\{0,1\}$）と書く。本体は止まり、実行後の値は $r'=r\cdot x^\varepsilon$、$x'=x^2$、$n'=k$ である。$r'\cdot x'^{\,n'}=r\cdot x^\varepsilon\cdot x^{2k}=r\cdot x^n=X^M$、$n'=k\ge0$、$n'< n$ なので、$I$ は保たれ $V$ は減る。終了時：$n\ge0$ かつ $n\le0$ なら $n=0$ で、$r=r\cdot x^0=X^M$ である。
条件を外した反例
cor-ac-three-checks と thm-ac-variant の条件は、どれを外しても結論が成り立たなくなる。$E$ は ex-ac-euclid のプログラムで、$P=\{a=4,\ b=6\}$ とする（$E$ を実行すると $a=2$ で止まる）。$S:=\mathbf{while}\ x< n\ \mathbf{do}\ (y:=y+2x+1;\ x:=x+1)$、$D:=\mathbf{while}\ \lnot(x=0)\ \mathbf{do}\ x:=x-2$ とする。
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 初期化 $P\subset I$ | $E$、$I=\emptyset$、$Q=\{a=0\}$ | $\{P\}\,E\,\{Q\}$ の部分正当性 |
| 維持（$I$ が帰納的） | $S$、$I=\{y\ge0\}$ | $\{I\}\,S\,\{I\land\lnot(x< n)\}$ の部分正当性 |
| 終了時 $I\land\lnot b\subset Q$ | $E$、$I=\Sigma$、$Q=\{a=1\}$ | $\{P\}\,E\,\{Q\}$ の部分正当性 |
| 変量の値の順序が整礎 | $D$、$I=\Sigma$、$V(s)=s(x)$ を $(\mathbb Z,<)$ で | $D$ の $I$ の上での停止性 |
| 停止性（部分正当性だけ） | $c_0:=\mathbf{while}\ 0=0\ \mathbf{do}\ \mathbf{skip}$ | $[\Sigma]\,c_0\,[Q]$ の完全正当性（どの $Q$ でも） |
どの行も、外した条件以外の条件が成り立ち、結論だけが崩れることを確かめればよい。
詳細
1 行目：$I=\emptyset$ では維持と終了時の条件は空の条件として成り立つ。$P$ から $E$ は $a=2$ で止まるので $\{P\}\,E\,\{a=0\}$ は部分正当でない。$P\not\subset\emptyset$ なので初期化だけが崩れている。3 行目：$I=\Sigma$ では初期化と維持が成り立つが、$E$ は $a=2$ で止まるので $\{P\}\,E\,\{a=1\}$ は部分正当でない。$\Sigma\land(b=0)\not\subset\{a=1\}$ なので終了時の条件だけが崩れている。
2 行目：状態 $x=-3$、$y=0$、$n=0$ から $S$ を実行すると、$(x,y)$ は $(-2,-5)$、$(-1,-8)$、$(0,-9)$ と進んで止まり、$y\ge0$ でない。実際、$y=0$、$x=-3< n$ は $I\land(x< n)$ を満たすが、本体の 1 回で $y=-5$ になるので維持が崩れている。一方 $x=0$、$y=0$、$n\ge0$ から始めると、ループの先頭で到達する状態はすべて $y=x^2\ge0$ を満たす。到達する状態で真であっても帰納的とは限らないので、不変条件として使うには $\{y=x^2,\ x\le n\}$ のように強める必要がある（これは帰納的で、$(x+1)^2=x^2+2x+1$ と $x< n\Rightarrow x+1\le n$ から維持され、終了時に $x=n$、$y=n^2$ を導く）。
4 行目：本体 $x:=x-2$ は止まり、$I=\Sigma$ は保たれ、$V$ は $(\mathbb Z,<)$ で真に減る。しかし $x=1$ から始めると $x$ は $1,-1,-3,\dots$ と奇数をとり続けて $0$ にならず、$D$ は止まらない。$(\mathbb Z,<)$ には無限の下降列があって整礎でないことだけが崩れている。$x$ が $0$ 以上の偶数である状態に $I$ を制限すれば、$V$ は $\mathbb Z_{\ge0}$ に値をとり、thm-ac-variant から止まる。5 行目は「部分正当性と完全正当性」の節で見たとおりである。
補足
$C:=\mathbf{while}\ \lnot(n=1)\ \mathbf{do}\ (\mathbf{if}\ n\operatorname{mod}2=0\ \mathbf{then}\ n:=n\operatorname{div}2\ \mathbf{else}\ n:=3\times n+1)$ について、$\{n\ge1\}\,C\,\{n=1\}$ の部分正当性は $I=\Sigma$ と cor-ac-three-checks からすぐ従う。一方、$C$ が $\{n\ge1\}$ の上で停止するという主張は 3x+1 予想（Collatz 予想）そのものであり、未解決である（Lag21 p. 1）。thm-ac-count により、停止するなら変量は存在するが、それを具体的に見つける方法は知られていない。部分正当性と停止性の難しさがまったく別でありうる例である。
- 非決定的なプログラム。 選択や乱択を含む言語では、同じ状態からの実行が複数ありうる。そのときは完全正当性を「すべての実行が止まり、結果がどれも $Q$ を満たす」と定める必要があり、prop-ac-total のような単純な言い換えはそのままでは使えない（NK14 §12.5 の注意）。
- 再帰的な手続き。 再帰的な手続きの正しさも同じ形で示す。部分正当性は再帰呼び出しについての帰納法（呼び出しの深さの帰納法）で、停止性は引数が整礎な順序で減ることで示す（整礎関係 の節「整礎再帰」）。
- 記憶領域を書き換えるプログラム。 番地を読み書きするプログラムの部分正当性は、分離論理 の Hoare 三つ組で扱われる。
関連項目
- 前提: 整礎関係, 数学的帰納法と整列性
- 例: Euclidの互除法, Edmondsの花アルゴリズム, Dijkstra法
- 比較: 分離論理, 停止問題
- 発展: 計算量理論, 計算可能性理論
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
