アルゴリズムイントロダクション2章まとめ(1) 2.1まで

アルゴリズムイントロダクション第3版、2章のまとめです。
長くなりそうなので 2.1 までを先に記事にします。

自分が重要だと思った部分、興味のある部分に絞っていますが、省いた部分は教科書の該当ページを示しています。
基本的には教科書からの抜粋・引用が多いですが、理解した範囲で、自分の言葉を使って一部書き換えています。

---

2. さあ、始めよう

この章では、挿入ソートとマージソートを題材に、アルゴリズムの実行時間の解析方法を学ぶ。

具体的には、以下のテーマを扱う。
・ループ不変式を用いたアルゴリズムの正当性の証明
・疑似コードの定義
・RAM計算モデル
・入力サイズ
・マージソートを題材にした分割統治アルゴリズムの解析

2.1. 挿入ソート

この節では、ソーティング問題を解くアルゴリズムである挿入ソートを紹介する。
・ソーティング問題の定式化
・挿入ソートの疑似コード
・挿入ソートのループ不変式
・ループ不変式を用いた挿入ソートの正当性の証明
・疑似コードの定義

まず、ソーティング問題(sorting problem)を定式化する。

入力：n 個の数の列<a1, a2, ..., an>
出力：a1' <= a2' <= ... <= an' である入力列の置換 <a1', a2', ..., an'>

挿入ソートは、トランプで手札をソートする時のことを思い浮かべると理解しやすい(教科書p.14)。

挿入ソートに対する疑似コード INSERTION-SORT を示す。
INSERTION-SORT は、長さ n の配列 A[1..n] を引数として取る（疑似コード中では n を A.length で表現している）。
このアルゴリズムは、入力された数列を「その場でソート」する。すなわち、Aを記憶する以外に必要な記憶領域は、高々定数でしかない（必要な記憶領域が n に依存しない）。

INSERTION-SORT(A)

for j = 2 to A.length
    key = A[j]
    // A[j] をソート済みの列 A[1..j-1]に挿入する
    i = j - 1
    while i > 0 かつ A[i] > key
        A[i+1] = A[i]
        i = i - 1
    A[i+1] = key

ループ不変式と挿入ソートの正当性

今まさにソートしようとしている要素をキー(key)と呼ぶ。
配列のj番目にあるキーを挿入しようとしているとき、1番目からj-1番目までにあった A[1..j-1] はすでにソートされている。この性質をループ不変式(loop invariant)として定式化する。

挿入ソートのループ不変式：

第1~8行のfor文の各繰り返し開始されるときには、部分配列 A[1..j-1] には開始時点で A[1..j-1]に格納されていた要素がソートされた状態で格納されている。

アルゴリズムの正当性を容易に証明するためにループ不変式を利用する。
ループ不変式に対して３つの性質を示す必要がある：

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

最初の２つの性質が成立するならば、すべての繰り返しの直前でループ不変式は真である。
このやり方は、数学的帰納法と似ている。
ただし、３つ目の停止性を用いた証明方法が、普通の数学的帰納法との大きな相違点である。
多くの場合、ループ不変式を、ループを停止に導いた条件と一緒に用いる。

挿入ソートについてこれらの性質が成立しており、このアルゴリズムが正当であることを証明しよう。

初期条件：j=2のとき、部分配列は A[1] のみから構成され、これは元々 A[1] に格納されていた要素である。よって、明らかにソート済みであるから、最初の繰り返しの直前においてループ不変式は真である。

ループ内条件：for分の本体が行っているのは、A[j]（キー）を入れるべき場所が見つかるまで、A[j-1], A[j-2], A[j-3],... を1つずつ右に移し(4~7行)、空いた場所にその値（キー）を挿入する(8行)ことである。これにより、部分配列 A[1..j] は元々 A[1..j] に格納されていた要素から構成されており、かつソート済みである。for分の次の繰り返し時にはjに1が加えられ、ループ不変式が維持される。
厳密には、while文(5~7行)に対するループ不変式を記述し、それが実際にループ不変式であることを証明する必要がある。ここでは形式的な取り扱いを追求せず、上記の簡単な解析を信頼し、ループ不変式が外側のループに対して成立していることが証明できたと考えることにする。

終了条件：for文が停止するのは条件 j > A.length = n を満たすときである。ループの各繰り返しでは、jを1だけ増加させるから、停止時に j = n + 1 が成立する。このとき、部分配列 A[1..n]には、開始時に A[1..n] に格納されていた要素が、ソートされて格納されている。部分配列 A[1..n] が入力された配列全体であることに注意すると、配列全体がソート済みであると結論できる。

以上より、アルゴリズムは正当である。

疑似コードに関する約束

教科書p.p.16-18を参照