さらに ChatGPT で以下のように質問しました。
再帰的呼び出しの「呼び出しの深さ」がどの経路を通っても有限であるならば、停止しますか？
以下の答えが返されました。
「ケーニッヒの補題」は『グラフ理論入門(原書第4版)』定理 16.3 に書かれていました。以前グラフ理論関連の本を調べたときは見落としていました。
はい、その条件なら停止します。ただし、「呼び出しの深さ」が何を意味するかを少し正確にすると、停止性との関係がはっきりします。
この `Factorize` の再帰呼び出しを木で表すと、
Factorize(a) ├── Factorize(b) │ ├── ... │ └── ... └── Factorize(c) ├── ... └── ...という再帰木になります。
このプログラムでは、各呼び出しから新たに呼び出される関数は高々2つです（分岐数が有限）。
各経路の深さが有限なら停止するか
もし
- 根から葉までのどの経路も有限長である
だけでは、一般には十分ではありません。
例えば、数学には
- 深さはすべて有限
- しかし深さに上限がない
ような木が存在します。
● / | | | ... ● ● ● ● | |||| ● | ●各枝は有限ですが、長さは 1,2,3,… といくらでも長くできます。
しかし、このような木は各節点から無限個の子が生えるので、あなたのプログラムでは起こりません。
このプログラムでは停止する
あなたの `Factorize` は
- 各呼び出しから子は高々2つ
- 各経路の深さが有限
という条件を満たします。
このとき、Kőnig（ケーニッヒ）の補題の対偶より、
- 有限分岐の木で無限個の節点があるなら、無限の経路が存在する。
したがって、
- 無限の経路が存在しない（＝すべての経路が有限）
ならば、木全体の節点数も有限です。
節点数が有限ということは、`Factorize` の呼び出し回数も有限なので、プログラムは停止します。
数学の証明との対応
実は、既約分解の証明でも本質的には同じことをしています。
- 整数では「毎回自然数が小さくなる」ので、無限経路は存在しません。
- PIDでは「生成イデアルが真に増加する」ので、ACCにより無限経路は存在しません。
そして `Factorize` のように各段階で高々2つにしか分岐しないので、Kőnig の補題を使えば、無限経路がないことから再帰木全体が有限であること、つまりアルゴリズムが停止することが従います。
したがって、このプログラムについては
「再帰呼び出しのどの経路も有限である」
という条件は、有限分岐であることと合わせれば、停止性を保証する十分条件になります。
続いて以下のように質問しました。
ケーニッヒの補題を説明してください
以下の答えが返されました。
ケーニッヒの補題（Kőnig's Lemma）は、無限木に関する非常に重要な定理で、再帰アルゴリズムの停止性や数理論理などでよく使われます。
木とは
ここでは木を
- 根（root）がある
- 各頂点は有限個の子を持つ
グラフとします。
例えば
● / | \ ● ● ● / \ | ● ● ●のようなものです。
有限分岐 (finitely branching)
各頂点から出る枝の本数に有限の上限があることです。
例えば
- 二分木（子が高々2個）
- 三分木（子が高々3個）
などです。
あなたの `Factorize` は
Factorize(a) ├── Factorize(b) └── Factorize(c)なので二分木です。
無限経路
根から
● | ● | ● | ● | ...と永遠に下っていける経路をいいます。
ケーニッヒの補題
定理
- 有限分岐な無限木には、必ず無限経路が存在する。
つまり
● / \ ● ● / \ / \ ● ● ● ● / \ ...のように頂点が無限個あるなら、
どこかに
● ↓ ● ↓ ● ↓ ● ↓ ⋮という無限に続く枝があります。
対偶
停止性ではこちらを使うことがほとんどです。
対偶は
有限分岐な木で、すべての経路が有限ならば、木全体も有限である。
これが再帰停止性に直接使われます。
なぜ有限分岐が必要なのか
これが一番重要です。
例えば
● / /|\ \ ... ● ● ● ● ● ... | | | | ● ● ● | | ●根から
- 長さ1
- 長さ2
- 長さ3
- …
- 長さn
という枝を一本ずつ生やします。
すると
- 頂点は無限個
- 無限経路はない
という木になります。
しかし根から無限本枝が出ています。
つまり有限分岐ではありません。
したがってケーニッヒの補題は使えません。
Factorizeとの関係
あなたのプログラムでは
Factorize(a)を根と考えると
各呼び出しは高々2つしか子を持ちません。
Factorize(a) ├── Factorize(b) └── Factorize(c)つまり有限分岐です。
そこで
もし
- 再帰呼び出しが無限回続く
なら、
ケーニッヒの補題より
- 無限に深い呼び出し列
Factorize(a) → Factorize(b) → Factorize(d) → Factorize(e) → ⋯が存在します。
逆に
- どの呼び出し列も有限である
ことが分かれば、
対偶より
- 再帰木全体も有限
となり、
プログラム全体が停止します。
証明のアイデア
証明自体は比較的簡潔です。
根を
とします。
木が無限なので、根の子のうち少なくとも1つは無限部分木を持っています（もし全部有限なら、それらを合わせても有限になってしまいます）。
その子を
と選びます。
同様に、
と選びます。
これを繰り返すと
という無限列が得られ、これは無限経路になっています。
この「必ず無限部分木を持つ子が選べる」という点で、「各頂点の子が有限個しかない」という有限分岐性が決定的に重要になります。
この補題は、あなたが最初に示した `Factorize` の停止性と非常によく対応しています。数学では「無限分解が存在しない」ことを示し、ケーニッヒの補題（対偶）を通して「再帰木全体が有限である」、すなわちアルゴリズムが停止する、と理解することができます。
続いて以下のように質問しました。
単項イデアル整域の元が既約元の積に分解できることの証明には、ケーニッヒの補題は必要ですか？
以下の答えが返されました。
- この証明は『可換環論の勘どころ (数学のかんどころ 32)』定理 2.54 と同様のようです。これは停止性とは無関係です。
- 『代数学２ 環と体とガロア理論 第２版』定理 1.11.18 の証明も存在を示すだけなので停止性とは無関係です。
結論から言うと、通常の証明にはケーニッヒの補題は必要ありません。
実際、教科書でよく見られる証明は、極小反例法（well-founded induction）を使っており、ケーニッヒの補題を経由しません。
標準的な証明
PID（実はネーター整域で十分）で、既約元の積に分解できない非零非単元があると仮定します。
そのような元全体が生成するイデアルの集合を考え、その中で極大のもの（あるいは包含について極小の反例に対応するもの）を選びます。
その元を
とします。
と分解でき、
はどちらも非単元です。
さらに
です。
ところが
は反例の中で極大に選ばれているので、
や
に対応する元は反例ではありません。したがって
は既約元の積に分解できる。
も既約元の積に分解できる。
よって
も既約元の積に分解できてしまい、矛盾です。
したがって反例は存在しません。
あなたのプログラムとの関係
一方、あなたの `Factorize` は実際に再帰を実行するアルゴリズムです。
アルゴリズムの停止性を考えるなら、
- 再帰木を考える。
- 「無限経路が存在しない」ことを示す。
- 有限分岐なのでケーニッヒの補題の対偶から再帰木全体が有限。
という議論は自然です。
つまり
- 「数学の存在証明」をするだけならケーニッヒの補題は不要。
しかし
- 「この再帰アルゴリズムが停止すること」を、再帰木を使って証明したいなら、ケーニッヒの補題（正確にはその対偶）は非常に自然な道具です。
本質的な違い
実は、この二つの証明はかなり近いものです。
- 極小反例法は、「無限降下列は存在しない」という整礎性を直接使っています。
- ケーニッヒの補題による証明は、「無限降下列（無限経路）が存在しないなら、有限分岐の再帰木は有限」という形で整礎性を木全体へ拡張しています。
そのため、理論的にはどちらも「整礎性」を利用していますが、
- 教科書の標準証明では 極小反例法だけで十分であり、ケーニッヒの補題は不要です。
- プログラムの停止性との対応を明確にしたい場合には、ケーニッヒの補題を介した説明は非常に見通しがよく、アルゴリズムと数学的証明の対応関係を理解しやすくします。
