ループと不変条件

ループ不変条件は反復を検証可能な証明にします。最大値の走査では、ループ先頭ごとに best が処理済みの接頭部分 values[0:i] の最大値であると保証します。初期化が条件を成立させ、各反復が回復し、終了時に最終結果へつなげます。

不変条件は明確なチェックポイントに結び付けます。本例では i < len(values) を調べる直前です。本体では一時的に次の要素まで含む形になっても、戻る前に元の形を回復します。

二分探索、二ポインター、複雑な while で境界を誤りやすい場合は、処理済み領域が何を保証するかを書きます。最初に成立しないチェックポイントが、誤りの位置を示します。

ループ不変条件の仕組み

証明には三つの段階があります。

1. 初期化：最初の条件確認前に成立することを示します。
2. 維持：一回の先頭で成立すると仮定し、反復後も成立することを示します。
3. 終了：不変条件と偽のループ条件から結果を導きます。

最大値の走査では best = max(values[0:i]) です。スライスは i を含まず、処理済み部分と一致します。best = values[0]、i = 1 なら最初の前半部分は [values[0]] で、最大値は values[0] です。

一回の候補は未処理の values[i] です。best = max(best, values[i]) によって best = max(values[0:i + 1]) が成立します。その後 i = i + 1 で同じ境界を新しい i と呼び、先頭の形 best = max(values[0:i]) を回復します。

ステップごとの解説

既定は values = [3, 1, 4, 2, 5] です。

1. 1 行目で best = 3、2 行目で i = 1 とします。処理済み部分は [3] で、初回の確認前に成立します。
2. 1 < 5 は真です。候補 values[1] = 1 に対して max(3, 1) は best = 3 を保ちます。i を 2 にすると [3, 1] について回復します。
3. 2 < 5 は真です。候補は 4 で、best は 4 になります。i = 3 の処理済み部分 [3, 1, 4] の最大値は 4 です。
4. 3 < 5 は真です。候補は 2 なので best は 4 のままです。i を 4 にし、証明済み部分をインデックス 3 まで伸ばします。
5. 4 < 5 は真です。候補は 5、best も 5 になり、i を 5 にすると全リストを覆います。
6. 5 < 5 は偽になり、停止して 6 行目で 5 を表示します。
7. 1 行目だけ best = 0 にし、入力を [-8, -3, -11, -2, -5] にします。最初から 0 ≠ max([-8]) = -8 なので、証明を開始できません。
8. 候補はすべて負のため best は 0 に残り、真の最大値 -2 ではなく 0 を表示します。

動く括弧はループ先頭の証明境界です。確認と更新の途中では、best が候補を取り込んだ後も、候補は括弧の外に残ります。i を進めると括弧が移り、先頭の式が回復します。

初期値が証明を壊す理由

全要素が負なら、best = 0 は入力にない値を持ち込み、すべての候補より大きくなります。最初の先頭で既に不変条件が偽で、更新も 0 を保ち、リストにない値を返します。

終了によって証明が完成する理由

停止時は i < len(values) が偽です。i は一ずつ増え、長さを越えないため i = len(values) になります。不変条件へ代入すると、

best = max(values[0:i]) = max(values[0:len(values)])。

後のスライスは全リストです。初期化と維持で best の意味を証明し、終了条件が境界を全入力へ広げるため、その値を出力できます。

時間計算量と空間計算量

長さ n の空でないリストでは、最初の値で初期化してから n - 1 個の候補を調べます。各回は定数の仕事なので時間は O(n) です。best、i、一時的な候補だけを保存するため、追加領域は O(1) です。

境界ケース

• 一要素。 初期化で全リストを覆い、初回の条件が偽です。本体を実行せず、その値を出します。
• 空リスト。 values[0] が IndexError を発生させます。この実装は一要素以上を要求し、空入力の実験は番兵で隠さずその前提を示します。
• 全要素が負。 先頭要素からの初期化なら正しく、0 からでは失敗します。
• 最大値が重複。 不変条件は値について述べるので、同じ最大値を再び見ても best は変わりません。
• 最大値が末尾。 最後の反復も不変条件を回復してから、最終の偽の確認へ進みます。

よくある間違い

• 各文の後で常に不変条件が成立すると言う。更新中は i + 1 の形で、インクリメント後に先頭の形へ戻ります。
• 入力条件を証明せず best = 0 を選ぶ。便利な番兵は問題を変えることがあります。本例の前半部分の最大値という不変条件は、最初の前半部分との一致も要求します。
• values[i] を読む前に i を増やす。候補を飛ばし、範囲外を読むこともあります。
• 初期化と維持だけで証明を終える。終了状態で処理済み部分が全入力を覆って初めて、事後条件を導けます。
• 数例の正しい出力を証明と呼ぶ。例は反例を見つけられますが、有効な全入力を覆うのは三つの証明義務です。

このレッスンでの簡略化

Python の文を一つずつハイライトします。4 行目は二拍で、max(best, values[i]) を評価してから best に書き込みます。内部の細かな操作、オブジェクト、フレーム、例外処理は省きます。証明は、有限かつ空でない比較可能な値の列と通常の整数インデックスを仮定し、並行した変更や独自の比較処理は扱いません。