## 定義 整列原理(Well Ordering Principle, WOP)とは、「非負整数の空でない部分集合には必ず最小元が存在する」という命題である。空集合には当てはまらず(最小元を持つ元自体が存在しない)、負の整数の集合や正の有理数の集合にも当てはまらない(いずれも最小元を持たない)。この原理を一般化したものが**整列集合(well ordered set)**で、空でないすべての部分集合が最小元を持つような数の集合を指す。非負整数の集合はその一例だが、すべての有限集合や `{rn : n ∈ N}`(`r` は正の実数)のような集合も整列集合になる。一方、非負有理数の集合は最小元(0)自体は持つが、正の有理数という空でない部分集合が最小元を持たないため整列集合ではない——「最小元を持つこと」と「整列であること」は別の性質である。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 2 The Well Ordering Principle]] §2.4) ## 中核概念 - **最小反例法による証明テンプレート**: 命題 `P(n)` をすべての非負整数 `n` について証明したいとき、反例の集合 `C := {n ∈ N | NOT(P(n))}` を定義し、背理法として `C` が空でないと仮定する。整列原理により `C` の最小元 `n` が存在するので、`P(n)` が実は真であること、あるいは `n` より小さい `C` の要素が存在することを示して矛盾を導き、`C` が空である(=反例が存在しない)と結論する。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 2 The Well Ordering Principle]] §2.2) - **停止性証明への応用**: 計算の各ステップに整列集合の値を単調減少に割り当てられれば、計算は無限には続かない。無限に続くと仮定すると、各ステップの値の集合が最小元を持たない部分集合になり整列性に矛盾するためである。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 2 The Well Ordering Principle]] §2.4) - **整列集合の判定条件**: 非負整数 `n` 以上の整数の集合は整列集合である(定理2.4.1)。この帰結として、下界を持つ整数の集合は整列集合であり(系2.4.3、下界の床関数を取り直すことで整列原理に帰着)、上界を持つ空でない整数の集合は最大元を持つ(系2.4.4、符号反転で下界の場合に帰着)。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 2 The Well Ordering Principle]] §2.4) ## 横断的知見 - 第1章の [[証明]] concept は証明の基本パターンを直接法・対偶法・場合分け・背理法の4種に整理しているが、整列原理に基づく「最小反例法」はこの4分類のどれか一つには単純に収まらない。形式としては背理法(反例の集合が空でないと仮定して矛盾を導く)だが、それに加えて「反例集合の最小元を取る」という整列原理固有の構造的な一手が加わっている。第1章の4パターンの記述は「対偶・背理法は直接法が難しいときの代替」という緩い指針にとどまっており、整列原理の証明テンプレートはその枠組みを具体化・拡張する特殊形として位置づけられる。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 1 What is a Proof?]], [[@2015__MIT__Mathematics for Computer Science - Chapter 2 The Well Ordering Principle]]) - 第5章§5.3は、整列原理・通常の帰納法・強帰納法が機械的な書き換えで相互変換可能な「同じ数学的推論の異なる提示形式」であることを明示的に示している。強帰納法の証明は帰納法の仮定に全称量化子を付け加えることで通常の帰納法の証明へ、通常の帰納法の証明は反例の集合を取ってその最小元を検討する形に書き換えることで整列原理の証明へ変換できる(逆方向の変換も可能)。第2章時点で提示されていた最小反例法は、この観点から見ると「整列原理による証明の標準形」であり、3手法の使い分けは論理的な強弱の問題ではなく、背理法を要さない明快さ(帰納法)・再帰的手続きの提供(帰納法)・簡潔さ(整列原理)という実務上の見やすさの選択にすぎないことが第5章で確定した。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 2 The Well Ordering Principle]], [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]]) - 整列集合を用いた計算の停止性証明(第2章§2.4で「整列集合の値を単調減少に割り当てれば計算は無限に続かない」として抽象的に述べられていた原理)は、第5章§5.4.5–§5.4.6で状態機械上の**導出変数(derived variable)**という具体的な道具立てに落とし込まれる。高速べき乗算プログラムでは、レジスタzの値が遷移ごとに(整数値のまま)少なくとも半分になることを示し、南東ジャンプロボットの例では値域が非負整数ではなく整列集合N+F(第2章補題2.4.5)である導出変数v(x,y):=y+x/(x+1)を用いることで、個々の実行の所要ステップ数を事前に上界づけられない場合にも停止性を証明する。第2章が原理を、第5章がプログラム検証(部分正当性と停止性への分解)への応用方法を担うという相補関係にある。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 2 The Well Ordering Principle]], [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]]) ## 未解決の問い - 整列集合という概念は、後続章(たとえば第7章 無限集合、可算・非可算の議論)でどう拡張・相対化されるか。 - 導出変数による停止性証明(第5章)は、整列原理そのものの適用範囲(非負整数以外の整列集合)をどこまで一般化できるか。本章で扱われたN+Fより複雑な整列集合の実例は ingest 後の後続章で確認する。 ## 関連 - source: [[@2015__MIT__Mathematics for Computer Science - Chapter 2 The Well Ordering Principle]] / [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]] - 概念: [[証明]] —— 証明の基本パターンを扱う姉妹concept。整列原理の最小反例法はその特殊形にあたる。/ [[帰納法]] —— 整列原理と相互変換可能な証明手法。/ [[不変条件]] —— 整列原理を状態機械の停止性証明に応用する際の道具立て(導出変数)を扱う。 ## 出典 - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 2.