「モノイドの素因数分解(1) - 非専門的シンギュラリティー研究所」の説明が非常にわかりにくいので何とかしたいのですが、今のところ良い説明の方法がありません。停止性についても何も言及していませんが説明した方が良さそうです。
「モノイドの素因数分解(1) - 非専門的シンギュラリティー研究所」の「プログラミング言語形式の証明」は単項イデアル整域の場合にも正しいということがわかりましたが、停止することが明らかとは言えないのでこの場合に使うのはやめておきます。停止することが明らかな場合に使った方が良さそうです。
このブログでは有用と思われるが検索してもすぐには見つからないようなことを主に書いているのですが、この件は ChatGPT ではどうなるのかについても調べてみます。
証明をプログラミング言語の再帰的関数の形に書いて証明する方法の呼び方はありますか？
以下の答えが返されました。
とても興味深い質問です。結論から言うと、**そのような証明方法を指す一つの確立した名称はありません**。しかし、関連する考え方や分野はいくつかあります。
1. 構成的証明 (constructive proof)
最も近いのは構成的証明です。
「存在する」だけでなく、実際に対象を構成するアルゴリズムを与える証明です。
例えば、
Factorize(a)という関数を書いて
- これが停止する。
- 戻り値が既約元のリストになる。
ことを証明すれば、
「既約元の積に分解できる」
という定理を証明したことになります。
2. アルゴリズム的証明 (algorithmic proof)
計算機科学では
- アルゴリズムを与え、その正当性を証明する
という形が非常に一般的です。
この場合は
1. 停止性 (termination)
2. 正当性 (correctness)を証明します。
あなたの `Factorize` なら
- Termination
- Partial correctness
- Total correctness
を示します。
3. 総正当性証明 (total correctness proof)
プログラム検証では
- 部分正当性
「停止したなら結果は正しい」
- 総正当性
「停止するし結果も正しい」
を区別します。
あなたの `Factorize` は
停止性 ＋ 正しい因数分解になるを示すので、
総正当性の証明そのものです。
4. Curry–Howard対応
さらに理論的には、
Curry–Howard対応では
- 証明 = プログラム
という考え方になります。
例えば
- Coq
- Agda
- Lean
では
Factorizeという再帰関数を書き、
停止性を証明すると、
その関数自体が定理の証明になります。
こちらでは
「プログラムを書くこと」が「証明を書くこと」です。
あなたの考えているスタイル
あなたが考えている方法は
- 定理を証明する代わりに、それを実現する再帰関数を書き、その停止性と正しさを証明する
というものです。
これは数学では必ずしも標準的な書き方ではありませんが、
- 構成的数学
- 計算機科学
- 型理論
- 定理証明支援系
では非常によく用いられる方法です。
呼び方を付けるなら
厳密な定着した名称はありませんが、内容を最もよく表す表現としては
- アルゴリズム的証明（algorithmic proof）
- 構成的証明（constructive proof）
- 再帰アルゴリズムによる証明（proof by recursive algorithm）
- 総正当性の証明（proof of total correctness）
あたりが適切です。
特に、あなたが `Factorize` のような再帰関数を定義し、「停止性」と「正しさ」を証明するというスタイルは、総正当性証明を用いたアルゴリズム的・構成的証明と呼ぶのが最も近いと言えるでしょう。
なお、この視点は代数学の証明にも応用できます。例えば「PID の元は既約元の積に分解できる」という定理を、`Factorize` のような再帰関数の総正当性を証明することで示す、という形に書き換えることができます。このように数学の証明をアルゴリズムの正当性証明として捉える考え方は、計算機科学や定理証明の分野では非常に自然なアプローチです。
さらに ChatGPT で以下のように質問しました。
既約元の定義を再帰的に適用することにより、プログラミング言語の再帰的関数にすることができますが、このように「何かの定義を再帰的に適用することによってプログラミング言語の再帰的関数にすること」の呼び方はありますか？
以下の答えが返されました。
これについても、広く定着した一つの名称はありません。しかし、あなたが述べている考え方は、いくつかの既存の概念と非常に近いものです。
あなたの例では、
既約元の定義
- 既約なら終了
- そうでなければ二つの因子に分け、それぞれについて同じことを行う
という**定義そのもの**を
Factorize(x)という再帰関数に翻訳しています。
これは数学的には次のような考え方に対応しています。
1. 定義のアルゴリズム化 (algorithmization of a definition)
最も自然な表現は
- 定義をアルゴリズム化する
です。
つまり、
- 数学的定義
- 帰納的定義
- 存在条件
を、そのまま実行可能な再帰関数へ写すことです。
例えば
既約なら終わる。 そうでなければ分解し、それぞれを既約になるまで分解する。↓
if (IsIrreducible(x)) return ... else { var (a,b)=Divide(x); return Factorize(a)+Factorize(b); }という変換です。
2. 定義の計算内容の抽出 (extracting computational content)
構成的数学や型理論では
- 定義や証明から計算内容 (computational content) を取り出す
という言い方をします。
つまり
数学では
- 「存在する」
と書かれているものを
プログラムでは
- 「どう計算するか」
に変換します。
この考え方は証明抽出 (program extraction) にもつながっています。
3. 帰納的定義から構造的再帰を得る
型理論では特によく知られています。
例えば
木とは ・葉 ・二つの木から木を作るという帰納的定義があると
自然に
f(葉)=... f(Node(l,r)) = ... f(l) f(r)という再帰関数が得られます。
これを
- 構造的再帰 (structural recursion)
と呼びます。
あなたの `Factorize` もかなりこれに近い発想です。
4. データ型の除去規則（Eliminator）
型理論では
帰納的定義には必ず
- Constructor（生成）
- Eliminator（消去）
があります。
たとえば自然数なら
0 Succ(n)から
f(0) f(Succ(n))という再帰関数を作ります。
これも
- 定義から再帰関数が得られる
という考え方です。
あなたの例は少し特殊
ただし、既約元の定義は普通の帰納的定義ではありません。
既約 または 分解して再び同じことをするという自己参照的な操作になっています。
つまり
Factorize(x)は
定義の自己参照をそのまま再帰呼び出しへ変換しています。
これは
- 帰納的データ型の構造的再帰
というより、
定義を実行可能な再帰アルゴリズムへ翻訳している
という見方が最も自然です。
もし名前を付けるなら
この考え方自体には標準的な名称はありませんが、内容を表すなら例えば
- 定義のアルゴリズム化（algorithmization of definitions）
- 定義の再帰的実装（recursive implementation of a definition）
- 定義の計算内容の抽出（extraction of computational content）
- 定義のプログラム化（programming a mathematical definition）
などが適切でしょう。
私は、この発想はかなり興味深いものだと思います。通常は「アルゴリズムを設計してからその正しさを証明する」という順序ですが、あなたが考えているのは逆に
- 数学の定義を読み、それを機械的に再帰関数へ翻訳する方法論
です。これは構成的数学や型理論の考え方に近い一方で、「定義からアルゴリズムを系統的に導く」という独自の視点を強調しています。もしこの方法論を体系化するのであれば、「定義のアルゴリズム化」や「定義駆動アルゴリズム設計（definition-driven algorithm design）」といった名称が内容をよく表しているでしょう。
