kenkovlog

けんこふたんっオフィシャユブヨグッ
アンッ!アンッ!アンッ!アンッ!

Loop Invariant

最近、 Thomas さんのIntroduction to Algorithms を購入して読んでいます。

今日はループ不変条件(loop invariant) の部分をまとめようと思います。

loop invariant とは

loop invariant とは
ループを回る前と後とで不変な条件のこと

loop invariant はアルゴリズムが正しいかどうかを証明するときに 役立つ概念です。 loop invariant が正しいかどうかを示すには次の二つを示せばよいです。

Initialization:
ループが開始する前の状態でloop invariant が成立する。
Maintenance:
ループを回る前にloop invariant が成立しているならば、 一周ループを回った後もloop invariant が成立する。

これは数学的帰納法と似ているのですぐに理解できるかと思います。

loop invariant は何のために使うのかというと、アルゴリズムが正しい(correct) かどうかを示すために使います。逆に言えば、アルゴリズムが正しいかどうかを 判定できるようなloop invariant を探さなければ意味がありません。 この意味で、loop invariant は次の性質を満たさなければなりません。

Termination:
ループが停止する時、loop invariant を使うことでアルゴリズムが正しいことを示せる。

練習問題の2.1-3 線形探索(searching problem) を考えてみましょう。

Input:
  • リスト lst = <a1,…,an>
  • キー key
Output:
  • key = lst[i] となる、先頭から一番初めに見つかったインデックスi
  • 上記のようなi がない場合はNone

これをPython でかくと

def linear_search(val, lst):
    for (i, val) in enumerate(lst)
        if val == key:
            return i
    return None

となります。loop invariant は

0 <= i <= len(lst)-1 について、lst[0], lst[1], ..., lst[i-1] の中にkey と一致するものは存在しない

です。ではこれがloop invariant であることを証明してみましょう。

Initialization:
i == 0 の時(変数を初期化しただけでまだ一回もループしていない時)、条件は空になるので成立します。
Maintenance:
i == nまで正しいとしましょう。つまりlst[0], lst[1], …, lst[n-1] の中にはkey と一致するものは存在しないとします。 ループ変数i がn+1 の時(n 回目ループを終えてi をインクリメントした直後)、そもそもn 回目のループで return していたらn+1 回目のループは起こりえません。return していないということはlst[n] != key ということです。 つまりn+1 で成立します。
Termination:

停止条件は二つ存在します。

  • return する時
  • ループが終了する時。

n 回目のループで return する場合は、loop invariant よりlst[n-1] までにはkey は出現しないことが保証されていて、かつ lst[n] == key なので正しいouput 返すことが分かります。

ループが終了する時、i の値はlen(lst)-1 です。しかし、最後のループでも値をreturn しないので結局

0 <= i <= len(lst) について、lst[0], lst[1], ..., lst[i-1] の中にkey と一致するものは存在しない

が成立することになります(i == len(lst) についても成立する)。 ということは、loop invariant (をi == len(lst) の場合に拡張したもの) によりlst の中にkey と一致するものが存在しないことが分かり、 かつNone がreturn されますので、こちらも正しいoutput を返すことがわかります。

以上によりアルゴリズムが正しい(corect) ことが、loop invariant を使って証明されました。

まとめ

loop invariant を使うことでアルゴリズムが正しい(correct) ことを証明できる。

けんこふたん