ループ不変条件とは何ですか？
1. 序章
このチュートリアルでは、 loop 不変条件とは何か、およびそれを使用してアルゴリズムの正当性を証明する方法について説明します。
2. ループ不変条件とは何ですか？
ループ不変条件は、アルゴリズムとプログラムのプロパティに関するステートメントを証明するために使用されるツールです。 当然、正確さは私たちが最も関心を持っている特性です。 アルゴリズムを使用する前に、アルゴリズムが常に正しい結果を生成することを確認する必要があります。
3. ループ不変条件とは何ですか？それをどのように証明しますか？
ループ不変条件は、次のようなアルゴリズムのループに関するステートメントです。
- ループの最初の反復の前にtrueであり、
- 反復の前にtrueの場合、次の反復の前にtrueのままになります。
これらの2つの条件がステートメントに当てはまることを証明できれば、ループの各反復の前にステートメントが真になるということになります。 さらに、最後の反復は不変条件に影響を与えないため、2つの条件により、ループ後も不変条件が真になることが保証されます。
多くのアルゴリズムがメインループで実際の作業を繰り返して解を更新するため、後の不変条件は解を保持する変数のプロパティを示します。 さらに、不変条件は、変数と実行された反復回数の間に意味のある関係を確立する必要があります。 その関係は、ループが終了した後に変数に含まれる解が、アルゴリズムが見つけるはずだった正しい解であることを示しているはずです。
3.1. ループ不変条件を定式化する方法は？
実数の配列を合計したいとしましょう。
アルゴリズムが機能することを確認するには、ループが終了した後、次の数値の合計に等しいことを証明する必要があります。
そのための1つの方法は、変数について不変なループを定式化することです。
-番目の反復の開始時に、はの最初の要素の合計に等しくなります。
これが適切な不変条件であるかどうかをどのように確認しますか？ ループの後に適用される不変条件が正しい解を記述していることを確認する必要があります。 この例では、ループは次の場合に終了するため、不変条件はループの終了時に
これが、アルゴリズムに返してほしいものです。 それで、証明すべき不変量を特定しましたが、どのようにして証明を考え出すのでしょうか？
3.2. ループ不変条件を証明する方法
不変量の証明は、数学的帰納法に似ています。
最初の反復の前に不変量が保持されるという要件は、誘導の基本ケースに対応します。
2番目の条件は、誘導ステップに似ています。
ただし、無限に続く誘導とは異なり、ループ不変条件はループが終了するまで保持する必要があります。
残念ながら、各アルゴリズムは一意であるため、証明を作成するための普遍的なレシピはありません。 すべての証明は同じ構造になります。
- 最初の反復の前に不変量が成り立つことを証明する
- 不変量が反復の前に成立する場合、次の反復の前にも成立することを証明します
ただし、プロセスの各ステップは実際のアルゴリズムによって異なります。
アルゴリズム1の場合、2つのステップで不変量を証明します。
ループの開始時、および。合計は数値なしの合計です。 その値として使用できるので、最初の反復の前に不変条件が成り立つことがわかります。
不変量が-番目の反復の開始時に成立するとしましょう：
反復中に、に追加するので、
反復の終わりに。 反復の終了は反復の開始と同じであるため、2番目の条件も満たされます。
私たちが示したように
ループの最後で、不変条件を証明することで、アルゴリズムが正しいことも確認されました。
ループがfor–loop の場合、反復の開始は、ループカウンターがインクリメントされた後、ループ終了テストの前のポイントです。 これは、ループの前に不変条件をチェックする場合にも当てはまります。
次に、さらに2つの例を考えてみましょう。
4. 2つの2進数の合計
2ビットの2進数があるとしましょう：と（それぞれ）。 それらの加算の結果は、ビットの2進数です。 以下からのキャリーオーバーを加算して一緒に計算することにより、各桁を計算できます。
4.1. ループ不変条件を定式化する
その正しさを検証するために、正しい結果であることを示すループ不変条件を使用します。
-番目の反復の開始時、数値はとの合計です。
この不変条件を証明することで、返された変数、が本当に正しい解であることを確認できますか？ ループの終わりでは、、したがって、不変条件ごとに、数はとの合計になります。 これは、正しい不変条件を選択したことを意味します。それを証明すると、アルゴリズムが正しいことも証明されます。
4.2. 最初の反復の前に不変ホールドを証明する
メインループの最初の反復の前、および。 数字がないので、私たちは解決策であり、唯一の数字であると見なします。 同様に、数字と数字がないため、実際に追加する数字はありません。 数がない場合の合計は、に等しいものとして扱うことができます。 したがって、不変量は最初の反復の前に真です。
4.3. 各反復後に不変条件が真のままであることを証明する
不変量が反復の開始時に成立する場合、それは反復の開始時に成立しますか？それが実際にとの合計であると仮定しましょう。 数字を計算するにはどうすればよいですか？ 数字を合計し、最後に計算した反復からのキャリーオーバー項と一緒に。 で割ると、整数の余りは数字になり、商は次の反復のキャリーオーバー項になります。これは、次の反復の開始時に不変量が真になることを証明します。
5. 挿入ソート
5.1. ループ不変条件を定義する
メインループの不変条件を定義しましょう：
forループの各反復の開始時に、サブ配列は、元々はからの位置にあるが、ソートされた順序の要素で構成されます。
これは良い不変量ですか？ forループの終わりに、、、不変条件は全体がソートされていることを示します。
5.2. 最初の反復の前に不変ホールドを証明する
最初の反復の前にそれがわかります。 したがって、不変条件は、[]がソートされた配列であると主張します。 これは（自明に）ゼロが数のない合計と見なすことができると仮定したのと同じように成り立ちます。
5.3. 各反復後に不変条件が真のままであることを証明する
それと、反復の開始時に設定したと仮定しましょう。 内側のwhileループの後、要素が（元の）より大きく、。以下であることを証明する必要があります。
whileループに対応するループ不変条件を証明することにより、これを正式に証明できます。 ただし、非公式には、whileループは、ある場所の要素が。より大きい限り、その要素を右に移動することがわかります。 ループが停止すると、それは。以下の要素（）が見つかったためです。 したがって、右に移動されたすべての要素、およびそれらは、より大きいです。 whileループの影響を受けないものはすべて、：よりも低くなります。 したがって、の-番目の位置に配置すると、サブ配列全体がソートされます。
6. ささいな声明
最初の反復の前に不変条件が成り立つことを証明する際に、通常、次のようなステートメントに依存します。
- 数字がない場合の合計はゼロになります。
- 要素が1つしかない配列がソートされます。
これらは、証明なしで真実であると見なすことができるステートメントです。これらは些細なものと呼ばれ、ベースケースの証明に広く使用されています。
7. 結論
この記事では、ループ不変条件とは何かを説明し、それを証明する方法を示しました。 また、ループ不変条件を使用してアルゴリズムの正しさを検証する方法を示すために、いくつかの例を作成しました。
