証明路開発支援システム(8) - 非専門的シンギュラリティー研究所

ChatGPT で調べてみました。

整数の場合(絶対値が減少する)や多項式の場合(次数が減少する)は明らかに停止するので「プログラミング言語形式の証明」で証明できるのですが、単項イデアル整域の場合はどうなるのか？

単項イデアル整域の元が既約元の積に分解できることの一般的な証明は分解の存在を示すだけなので、「プログラミング言語形式の証明」の停止性と関係なく成立します。
単項イデアル整域の場合の「プログラミング言語形式の証明」は停止します。よって単項イデアル整域の場合も証明できます。これについては後で見ていきます。

以下のように質問しました。

以下の C# の関数 Factorize (素因数分解する関数)は停止しますか？ここで IsIrreducible は既約元かどうかを調べる関数、Divide は既約ではない元を二つの(1ではない)因子に分解する関数です。

        private List<int> Factorize(int number)
        {
            var factors = new List<int>();
            if (IsIrreducible(number))
            {
                factors.Add(number);
            }
            else
            {
                var (factor1, factor2) = Divide(number);
                factors.AddRange(Factorize(factor1));
                factors.AddRange(Factorize(factor2));
                factors.Sort();
            }
            return factors;
        }

以下のような答えが返されました。

結論から言うと、このコードだけでは停止するとは証明できません。停止性は `Divide` の仕様に依存します。
停止性を考えるには、再帰呼び出しのたびに「必ず小さくなる量」が存在することを示す必要があります。
整数の素因数分解の場合

`number` が 2 以上の整数で、

`IsIrreducible(number)` は素数判定である。

`Divide(number)` は

$number = factor1 \times factor2$
を満たし、

`factor1 > 1`

`factor2 > 1`

であるとします。
すると
$factor1 < number,\qquad factor2 < number$
が必ず成り立ちます。
実際、もし `factor1 = number` なら
$factor2 = 1$
となり条件に反します。
したがって、再帰呼び出しでは引数が必ず小さくなります。
Factorize(number)
    ↓
Factorize(factor1)   (factor1 < number)
Factorize(factor2)   (factor2 < number)
自然数は無限に小さくなれないので、この再帰は有限回で終了します。
これは数学的帰納法（または自然数の整礎性）による停止証明です。
一般の環の場合

質問文では

IsIrreducible は既約元かどうかを調べる関数

となっています。
一般の整域では、既約元への分解が必ず存在するとは限りません。
例えば、

一意分解整域 (UFD)

より一般には原子整域 (atomic domain)

であれば
a
↓
bc
↓
...
↓
既約元
という分解は有限回で終わります。
しかし、整域によっては
a = b1 c1
b1 = b2 c2
b2 = b3 c3
...
のように無限に分解できてしまう場合（非原子的整域）が存在します。
そのような環では
Factorize(b1)
    ↓
Factorize(b2)
    ↓
Factorize(b3)
    ↓
...
となり停止しない可能性があります。
停止性を保証する条件

この関数が停止することを保証するには、例えば次のような条件が必要です。

`Divide(x)` が返す `factor1`, `factor2` は、ある「大きさ」を表す関数 μ に対して
```
μ(factor1) < μ(x)
μ(factor2) < μ(x)
```

を満たす。

整数では
μ(n) = n
とすれば十分です。
ガウス整数や多項式環では

ノルム

次数

などを μ とできます。
まとめ

整数の素因数分解として考えるなら、この関数は停止します。`Divide` が返す因子はどちらも元の整数より小さいため、自然数の整礎性により再帰は有限回で終了します。

一般の環では、このコードだけから停止性は証明できません。既約元への分解が有限回で終わること（例えば環が原子的であること）や、各再帰で必ず減少する適切な評価関数（ノルムや次数など）が存在することを仮定する必要があります。

続いて以下のように質問しました。

単項イデアル整域の元が既約元の積に分解できることの一般的な証明は、このプログラムと同様のことをやっていると考えられますが、その場合は停止しますか？

以下のような答えが返されました。

はい、その見方は本質的に正しいです。ただし、プログラムが停止する理由と数学の証明で停止する理由には対応する概念があります。
単項イデアル整域 (PID) の証明を見てみましょう。
証明の流れ

既約元でない元 (a) を考えます。
すると
$a = bc$
と分解でき、しかも (b,c) はどちらも単元ではありません。
ここであなたのプログラムでは
Factorize(a)
    ↓
Factorize(b)
Factorize(c)
という再帰を行っています。
問題は、この再帰が無限に続かないことです。
PIDではなぜ停止するのか

PIDでは
$(a)\subsetneq (b)$
という真の包含が起こります。
なぜなら
$a=bc$
より
$(a)\subseteq(b)$
ですが、もし等号なら
$b=ua$
となる単元 (u) が存在し、
$a=(ua)c$
から
$1=uc$
となって (c) が単元になってしまい矛盾します。
したがって
$(a)\subsetneq(b)$
です。
同様に
$(a)\subsetneq(c)$
でもあります。
無限再帰するとどうなるか

もし
a
↓
b1
↓
b2
↓
b3
↓
…
と無限に分解できたとすると
$(a)\subsetneq(b_1)\subsetneq(b_2)\subsetneq\cdots$
という真に増加する単項イデアル列ができます。
ところがPIDはネーター環なので、イデアルについて昇鎖条件 (ACC) を満たします。
つまり
$I_1\subseteq I_2\subseteq I_3\subseteq\cdots$
という増加列は有限段階で止まります。
真の包含ばかりの列は存在できません。
したがって無限分解は起こらず、再帰は有限回で終了します。
プログラムとの対応

プログラムでは停止性は

引数が毎回小さくなる

ことで保証していました。
整数では
$\mu(n)=n$
という「大きさ」があります。
PIDでは数値ではなく
$(a)$
という生成する単項イデアルが「大きさ」の役目をしています。
再帰一回ごとに
(a)
    ↓
(b)
と必ず大きいイデアルへ移る（真の包含になる）ため、
ACCによって無限には続けられません。
さらに一般化すると

実は、この証明はPIDである必要もありません。
必要なのは

イデアルがACCを満たす（ネーター環）

分解するたびに生成イデアルが真に大きくなる

という2点だけです。
したがって
「ネーター整域ならすべての非零非単元は既約元の積に分解できる」
という定理になります。
つまり、あなたの C# の `Factorize` は、整数では「自然数が減少する」ことを停止性の根拠にしていますが、PID の一般的な証明では「生成イデアルが真に増加し、その増加列が ACC により有限で止まる」ことを停止性の根拠にしています。アルゴリズムとしては同じ「再帰的分解」であり、停止性を保証する「大きさ」の概念だけが、自然数からイデアルの順序へと抽象化されていると考えることができます。