💻 computer science

A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem

この論文は、排中律や対角線論法を用いずにヒルベルトの第 10 問題の未決定性に帰着させる「二重の証拠」構成により、直観主義論理の枠組みでライス定理と停止性問題を構成的に証明し、Rocq 証明支援系で形式化されたことを示しています。

原著者： Jonathan Brossard

公開日 2026-04-21

📖 1 分で読めます☕ さくっと読める

原著者： Jonathan Brossard

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

この論文は、計算機科学における「究極の壁」である**「プログラムがどんな性質を持つかを、機械的に判断できるか？」**という問いに対して、新しい視点から「いや、それは不可能だ」と証明した画期的な研究です。

著者のジョナサン・ブロッサード氏は、これまで使われてきた「古典的な証明方法」を捨て去り、**「ヒルベルトの第 10 問題」**という数学の難問を足がかりにして、よりシンプルで論理的な証明を完成させました。

以下に、専門用語を排し、日常の比喩を使ってこの論文の核心を解説します。

1. 従来の証明：「鏡と迷路」のジレンマ

これまでの証明（ライス定理や停止問題）は、少し複雑な「鏡合わせ」のような方法を使っていました。

従来の方法： 「もし、あるプログラムが『止まる』か『止まらない』かを判定する機械があったとしよう。では、その機械を自分自身に適用したらどうなる？」という**自己言及（自分自身を鏡に映すような）**のトリックを使います。
問題点： この方法は、「止まるか？止まらないか？」という二択を前提とするため、論理的に少し強引な部分（排中律と呼ばれる古典的な論理）が含まれていました。まるで、「迷宮で出口を見つけるために、壁を壊して強引に進む」ような方法でした。

2. この論文の新手法：「双子の探偵」と「方程式の謎」

この論文は、その「鏡合わせ」や「強引な壁破壊」を一切使いません。代わりに、**「双子の探偵」と「数学の方程式」**という 2 つの要素を組み合わせた、非常にエレガントな方法を採用しています。

① 双子の探偵（2 つのプログラム）

ある「性質 P」（例えば「このプログラムは止まるか？」）を判定する機械があると仮定します。
著者は、ある数学の方程式（ディオファントス方程式） $D$ に対して、2 つの双子のようなプログラムを作ります。

兄（ $S_1$ ）： 方程式 $D$ に「解（答え）」がある場合、**「止まる」**ように振る舞う。
弟（ $S_0$ ）： 方程式 $D$ に「解」がある場合、**「止まらない（永遠に動き続ける）」**ように振る舞う。

しかし、ここがミソです。
もし方程式 $D$ に**「解がない」**場合、**兄も弟も同じように「永遠に動き続ける」**ことになります。

② 判定機械の試練

ここで、判定機械（ DecideP ）にこの双子を見せます。

ケース A（解がある場合）：
兄は止まり、弟は止まらない。判定機械は「兄は〇、弟は×」と明確に区別できます。
ケース B（解がない場合）：
兄も弟もどちらも「永遠に動き続ける（同じ振る舞い）」です。判定機械は、**「兄と弟は全く同じだ」**と判断せざるを得ません。

③ 矛盾の発見

もし「どんなプログラムでも正しく判定できる機械」が本当に存在するなら、それは**「方程式に解があるか否か」**を、この双子の振る舞いの違いだけで見抜くことになります。
つまり、「判定機械」は「方程式の解の有無」を判定する機械になってしまいます。

しかし、数学の「ヒルベルトの第 10 問題（MRDP 定理）」という大定理は、**「方程式に解があるかどうかを、機械的に判定することは不可能だ」**と断言しています。

結論：
「判定機械」が存在すると仮定すると、「不可能なことが可能になる」という矛盾が生まれます。
したがって、「判定機械」は存在しない。 これがこの論文の証明です。

3. なぜこれが重要なのか？（「建設的」な証明の意味）

この証明のすごいところは、**「構成可能（Constructive）」**である点です。

従来の証明： 「もし存在すれば矛盾するから、存在しない」という**「否定」**の形でした。まるで「幽霊がいるか？いない。なぜなら、いるとすれば変だから」と言っているようなものです。
この論文の証明： 「もし判定機械を作ろうとすれば、必ず『方程式の解』を見つけるという、不可能なタスクを課されることになる」という**「具体的な仕組み」**を示しました。
- これは、幽霊の存在を否定するのではなく、「幽霊を捕まえるには、空を飛ぶ必要があるが、人間には飛べないから捕まえられない」というように、「なぜできないのか」の具体的な理由を提示しています。

この「具体的な理由」があるおかげで、この証明は直観主義論理（古典的な「A か B か」の二択を認めない、より厳密な論理）でも成立します。つまり、この証明はコンピュータが実際に検証できる形（Coq という証明支援系）で書かれており、**「数学的に 100% 確実」**であることが保証されています。

4. まとめ：何が変わったのか？

昔の考え方： 「自分自身を鏡に映して、矛盾させる」→ 複雑で、古典的な論理に依存していた。
新しい考え方： 「数学の方程式（解があるかないか）を、双子のプログラムの振る舞いに翻訳する」→ シンプルで、論理的な矛盾を「方程式の難しさ」に直接結びつけた。

この論文は、**「プログラムが何をするか（意味）を、機械的に全部判断することは、数学の難問（方程式の解）を解くことと同じくらい不可能だ」**という事実を、より美しく、より堅固に証明したものです。

まるで、**「すべての料理の味を瞬時に判定する魔法の舌」が存在すると仮定すると、「すべての数学の問題を瞬時に解く魔法の頭脳」**が必要になることがバレてしまい、それは不可能だから「魔法の舌」も存在しない、という論理です。

論文「Hilbert の第 10 問題を通じたライス定理と停止問題の構成的証明」の技術的概要

本論文は、計算機科学における古典的な結果であるライス定理（Rice's Theorem）と停止問題（Halting Problem）の非決定性を、直観主義論理（Intuitionistic Logic）の枠組み内で、排中律（LEM）や対角化法（Diagonalization）を用いずに証明する新しいアプローチを提示しています。著者 Jonathan Brossard は、ヒルベルトの第 10 問題（Diophantine 方程式の可解性）の非決定性（MRDP 定理）を基盤とした「二重証人構成（Two-witness construction）」を用いて、これらの定理を構成的に再構築しました。

以下に、問題、手法、主要な貢献、結果、および意義について詳細にまとめます。

1. 問題の背景と課題

ライス定理と停止問題: ライス定理は、「プログラムに関する任意の非自明な意味論的性質（例：停止するかどうか）は決定不可能である」と主張します。停止問題は、この定理の最も有名な具体例です。
古典的証明の限界: 従来の教科書的な証明は、以下の古典的な論理原則に依存しています。
1. 排中律（LEM）: 「あるプログラムが停止するか、しないか」を前提とした場合分け（特に、常に発散するプログラム $\bot$ が性質 $P$ を満たすかどうかの分岐）。
2. 対角化法・自己言及: 仮定された決定機が矛盾を導くようなプログラムを構成する際、自己言及（Recursion Theorem など）を用いる。
構成的証明の必要性: 直観主義論理や Coq/Agda などの証明支援系では、排中律や二重否定除去が使えないため、古典的な証明はそのまま実行可能なコード（プログラム抽出）に変換できません。また、どの非構成的原理が定理に必須かを特定する「構成的逆数学」の観点からも、より弱い仮定での証明が求められています。

2. 手法：MRDP 定理に基づく二重証人構成

著者は、停止問題への還元ではなく、ヒルベルトの第 10 問題（Diophantine 方程式の可解性）への直接還元という戦略を採用しました。

MRDP 定理の活用:
- MRDP 定理（Davis-Putnam-Robinson-Matiyasevich）は、「任意の帰納的列挙可能集合はディオファントス集合である」ことを示しており、その非決定性は構成的に確立されています（Larchey-Wendling と Forster による Coq 形式化済み）。
- 本証明では、この非決定性を唯一の外部公理（Axiom）として使用します。
二重証人構成（Two-witness Construction）:
- 非自明な意味論的性質 $P$ に対して、 $P$ を満たすプログラム $e_1$ と満たさない $e_0$ が存在すると仮定します。
- 任意のディオファントス多項式 $D$ $D$ に対して、2 つのプログラム $S^0_D$ $S_{D}^{0}$ と $S^1_D$ $S_{D}^{1}$ を構成します。
  - $D$ が可解な場合: 検索が成功した時点で、 $S^0_D$ は $e_0$ の振る舞いをし、 $S^1_D$ は $e_1$ の振る舞いをします。
  - $D$ が不可解な場合: 検索が永遠に続くため、 $S^0_D$ と $S^1_D$ の両方がすべての入力に対して発散（ $\bot$ ）します。
- 観測的同等性: 構成において、 $D$ が可解でない場合、両プログラムは完全に同じ振る舞い（発散）をするため、 $P(S^0_D) \iff P(S^1_D)$ が成り立ちます。このとき、 $P(\bot)$ の真偽を知る必要はありません。
決定子の矛盾:
- もし $P$ を決定する決定子 $Decide_P$ が存在すると仮定すると、 $D$ の可解性に応じて $Decide_P(S^1_D) - Decide_P(S^0_D)$ の値が 1（可解）または 0（不可解）となります。
- これは、ディオファントス方程式の可解性を決定するアルゴリズムが存在することを意味し、MRDP 定理（非決定性）と矛盾します。
- この証明は「 $D$ は可解か不可解か」という排中律的な分岐を行わず、2 つの独立した含意（可解 $\Rightarrow \delta=1$ , 不可解 $\Rightarrow \delta=0$ ）として構成されます。

3. 主要な貢献と新規性

排中律と対角化の完全排除:
- 証明全体が直観主義論理で有効であり、排中律（LEM）や二重否定除去を一切使用していません。
- 自己言及や固定点定理（Recursion Theorem）を用いた対角化法を回避し、明示的な検索アルゴリズムに基づいています。
- $P(\bot)$ （発散プログラムの性質）に関するケース分けを不要にしています。
燃料（Fuel）:
- 形式化において、プログラム $S^b_D$ は内部で検索を行う際、発見されたステップ数以降は、ターゲットプログラム $e_b$ に「燃料（計算ステップの上限）」をそのまま渡す設計を採用しました。
- これにより、以前の問題解決で必要とされていた「証人プログラムの全性（Totality）」の条件が不要となり、任意の部分関数（発散する可能性のあるプログラム）に対して定理が成立します。
**Rocq **(Coq):
- 論文の主張は、Rocq 証明支援系（Coq の派生）で完全に形式化され、検証されています。
- 形式化は「ステップ付インデックスモデル（Step-indexed model）」に基づいており、外部公理は MRDP の非決定性（H10C_SAT_undec）のみです。
- Print Assumptions コマンドにより、ライス定理と停止問題の証明が「グローバル文脈の下で閉じている（Closed under the global context）」ことが確認されています。

4. 結果

ライス定理の構成的証明: 任意の非自明な意味論的性質は決定不可能であることが、MRDP 定理から構成論理的に導かれました。
停止問題の導出: ライス定理の直ちに導かれる帰結（Corollary）として、停止問題の非決定性が証明されました。
- 従来の構成的証明では、停止問題を最初に証明し、そこから他の問題を導出する流れでしたが、本論文ではMRDP $\to$ ライス定理 $\to$ 停止問題という逆の方向で導出しています。
- 停止問題の証明は、Rocq 上で 1 行のコード（exact (Rice Theorem Terminates Terminates_NonTrivial)）で完了します。

5. 意義と応用

計算的含意（Computational Content）:
- 構成的証明は、証明から直接「決定不可能性」を検証するアルゴリズムや変換を抽出できる可能性があります。
- 証明支援系（Coq, Agda）内で、排中律なしに決定不可能性を扱えるようになるため、形式検証の信頼性が向上します。
構造的特徴:
- 単一のプログラムに対するケース分けではなく、2 つのプログラムの関係性（ $\delta_D$ ）に情報をエンコードする「非分岐還元（Non-branching reduction）」という新しい構造を提供しています。
逆数学への寄与:
- ライス定理と停止問題が、ヒルベルトの第 10 問題の非決定性という「最も弱い」非構成的仮定のみで十分であることを示しました。
実用的な側面:
- 論文では、この構成に基づいた C 言語の実装例（undecidable.c）も提示されており、数論的な未解決問題（3 つの立方数の和）に関連するプログラムの停止性が、ディオファントス方程式の可解性と等価であることを示唆しています。

結論

本論文は、計算理論の根幹をなすライス定理と停止問題に対して、古典的な対角化法や排中律に頼らない、純粋に構成的な証明を初めて提示した画期的な成果です。ヒルベルトの第 10 問題の非決定性を基盤とし、Rocq による完全な形式化によってその正当性が担保されています。これは、形式検証、構成的論理、および計算複雑性の理論的基盤を強化する重要なステップです。