読者です 読者をやめる 読者になる 読者になる

大学院生(情報科学)のブログ

モチベーション維持のためのブログです。

ループ不変式

前回の記事で挿入ソートのソースコードを示したが、その正当性を今回は示す.

def insert_sort(A):
		for j in range(1,len(A)):
			key = A[j]
			i = j - 1
			while i >= 0 and A[i] > key:
				A[i+1] = A[i]
				i = i - 1
			A[i+1] = key
		return A

for文の{j}は、トランプで言うところの、左手に挿入しようとしている「現在のカード」を示す.
したがって、部分配列A[0,{\cdots},j-1]はソート済みの配列であり、A[j+1,{\cdots},n]はソートが行われいない配列である.
ここで、既にソートされているA[0,{\cdots},j-1]が持つループ不変式を定式化する.

  • 初期条件 : ループ実行開始直前ではループ不変式は真
  • ループ内条件 : あるk回目の繰り返しの直前でループ不変式が真ならば、{k+1}回目の直前でも真
  • 終了条件 : ループが停止した時、アルゴリズムの正当性の証明に繋がる有力な性質が不変式から得られる

初期条件とループ内条件を見ると数学的帰納法に類似しているように見える.
実際この二つを示されたら全ての繰り返しにおいてループ不変式は死んである.
しかし、ループ不変式を用いて正当性を示すのに最も重要なのは第3の性質である.
この停止性が数学的帰納法の相違点である.(数学的帰納法は無限に適用するのに対し、今回はループが停止すると「帰納」を停止する.)

これらを用いて、挿入ソートの不変性を示す.

  • 初期条件 : ループ開始直前{(j=1)}の直前はソート済み部分配列は{A[0]}と要素を一つしか含まないので、ソート済みなのは明らか.したがって、開始直前では真.
  • ループ内条件 : キーである{A[j]}を挿入するべき場所が見つかるまで{A[j-1],A[j-2],\cdots}をそれぞれ1つずつ右に移し、空いた場所に{A[j]}の値(キー)を挿入する.こうすることで、部分配列{A[0\cdots,j]}はソート済みになる.(厳密には{while}文についての正当性も示す必要があるがここでは割愛)
  • 終了条件 : {for}文の終了条件は{j > n-1}を満たすときである.

したがって、停止時には{j = n}である.
部分配列{A[0\cdots,n-1]}はソート済みであり、配列全体であるので、配列全体がソート済みであると結論できる.

以上より、アルゴリズムは正当であることが示された.

今後も、余力があればアルゴリズムの正当性についても考えて行きたいが、アルゴリズムの紹介だけで終わってしまうかもしれない...