[解決済み] ループ不変量によるマージソートの正しさの証明 (初期化 , 保守 , 終了)

質問

ループ不変量の状態を推論して、マージソートの正しさを証明するにはどうしたらよいでしょうか？各フェーズで何が起こるか説明してください。

a) 初期化 b) メンテナンス c) 終了

ありがとうございました。

解決方法は？

マージソートの疑似コード

MERGE-SORT(A、p、r)

    1 if p < r
    2    then q <-- [(p + r) / 2]
    3          MERGE-SORT(A, p, q)
    4          MERGE-SORT(A, q + 1, r)
    5          MERGE-SORT(A, p, q, r)

MERGE-SORT(A、p、q、r)

    1  n1 <-- q - p + 1 
    2  n2 <-- r - q
    3  create arrays L[1 ... n1 + 1] and R[1 ... n2 + 1]
    4  for i <-- 1 to n1
    5       do L[i] <-- A[p + i - 1]
    6  for j <-- 1 to n2
    7      do R[j] <-- A[q + j]
    8  L[n1 + 1] <-- infinite 
    9  R[n2 + 1] <-- infinite
    10 i <-- 1
    11 j <-- 1
    12 for k <-- p to r
    13     do if L[i] <= R[j]
    14           then A[k] <-- L[i]
    15                i <-- i + 1
    16           else A[k] <-- R[j]
    17                j <-- j + 1

2つのカードの山を並べ替えようとしますが、基本的な各ステップでどちらかの山が空かどうかをチェックすることを避け、コードを単純化するために無限をセンチネルカードとして使用します。そのため、センチネルカードのinfinieが公開されたときはいつでも、両方の山にセンチネルカードが公開されていない限り、小さい方のカードになることはできません。しかし、そうなれば、センチネルカードでないカードはすべてすでに出力側の山に置かれています。ということがあらかじめ分かっているので r - p + 1 のカードが出力されることになるので、それだけの基本ステップを踏んだらやめることができるのです。

• ループ・インバリアント。

  • 初期化：ループの最初の反復の前に、我々は k = p になるように、サブアレイ A[p ... k - 1] は空です。この空のサブアレイには k - p = 0 はLとRの最小の要素であり、そのため i = j = 1 L[i]とR[j]は共にAへコピーバックされていない配列の最小の要素です．

  • メンテナンス 各反復がループ不変性を維持することを確認するために、まず、l[i] <= R[j]と仮定しよう。このとき、L[i]はまだAにコピーバックされていない最も小さい要素である。 A[p ... k - 1] には k - p 最小の要素、14行目でL[i]をA[k]にコピーした後、サブアレイの A[p ... k] を含むことになります。 k - p + 1 最小の要素です。k (forループの更新) と i (15行目) をインクリメントすると、次の反復でループ不変性が再確立される。代わりに L[i] > R[j] があれば、16-17行目でループ不変性を維持するための適切なアクションが実行されます。

  • 終了。終了時。 k = r + 1 . ループ不変性により、サブアレイ A[p ... k - 1] である。 A[p ... r] を含む。 k - p = r - p + 1 の最小要素である L[1 ... n1 + 1] と R[1 ... n2 + 1] であり、ソート順である。配列LとRを合わせると n1 + n2 + 2 = r - p + 3 要素で構成されています。最も大きい2つの要素以外は全てAにコピーバックされており、この最も大きい2つの要素がセンチネルである。