Mechanized Undecidability of Higher-order beta-Matching (Extended Version)

無限の機械の壮大な謎

あなたは探偵として、謎を解こうとしています。しかし、その犯罪現場は、論理と規則だけで構成された世界です。これはコンピュータサイエンスの世界、具体的には「計算可能性理論」と呼ばれる分野であり、「コンピュータはあらゆる問題を解決できるのか？」という根本的な問いを投げかけています。1930年代、数学者たちはその答えが明確な「ノー」であることを発見しました。あまりにもトリッキーなために、どれほど強力なコンピュータであっても、どれほど長い時間を与えても、決して解を保証できないパズルが存在するのです。これらは「決定不能」な問題と呼ばれます。

この論理の世界における最も有名な道具の一つが、ラムダ計算です。これを、ターミナルに入力するプログラミング言語としてではなく、巨大で抽象的な「置換のゲーム」と考えてみてください。あなたには、パズルのピースを入れ替えるためのルールがいくつかあります。例えば、「すべての『A』を『B』に置き換える」というルールがあり、それを『A』だらけの文章に適用すると、新しい文章が得られます。ゲームは「高階（higher-order）」の動きを許容すると、はるかに難しくなります。標準的なゲームでは、単純なアイテムを入れ替えます。しかし、高階のゲームでは、ルールや関数そのものを入れ替えることができます。それは、ゲームの途中で「AをBに置き換える」というルールを、「AをCに置き換える」という新しいルールへと入れ替えることが許されるようなものです。

この論文が扱う特定の謎は、**高階ベータ・マッチング（Higher-Order Beta-Matching）**と呼ばれるものです。想像してみてください。あなたは「テンプレート（複雑な関数）」と「ターゲット（特定の実行結果）」を与えられました。問題は、「テンプレートを、ターゲットと正確に一致するように変形させるために、どのような特定のピースをそこに組み込めるか？」ということです。長い間、数学者たちはその答えは「いいえ、常に判別できるわけではない」と推測してきましたが、それを証明することは、素手で煙を捕まえようとするような困難な作業でした。その証明には、もしこのマッチング・パズルを解くことができるならば、「停止問題（プログラムが終了するか、あるいは無限ループに陥って動かなくなるかという究極の未解決問題）」をも解けることを示す必要がありました。

論文の発見：不可能への新しい地図

アンドレイ・ドゥデンヘフェナー（Andrej Dudenhefner）によるこの論文は、高階ベータ・マッチングが確かに決定不能であることを示す、新鮮で明快な証明を提供しています。言い換えれば、いかなる複雑な論理式に対しても、一方が他方に変形可能かどうかを確実に判定できる一般的な手法やアルゴリズムは存在しないということです。

著者は単に古い証明を繰り返したわけではありません。彼らは、答えへと至る新しい架け橋を築きました。以前の試みは、「ラムダ定義可能性（lambda-definability）」という非常に複雑で抽象的な概念を用いた、折れそうなほど精巧で過剰に設計された橋を使って峡谷を渡ろうとするようなものでした。それらの古い橋はあまりにも複雑であったため、専門家でさえすべてのボルトを検証することに苦労し、エラーをチェックするためのコンピュータプログラムへと翻訳することもほぼ不可能でした。

ドゥデンヘフェナーのアプローチは異なります。彼らは、ラムダ定義可能性という重厚で複雑な機構から始めるのではなく、もっとシンプルなもの、すなわち**文字列書き換え（String Rewriting）**から出発しました。想像してみてください。あなたは言葉を変化させるためのルールを持っています。例えば、「『00』を見つけたら『22』に変える」というルールや、「『02』を見つけたら『11』に変える」というルールがあるとします。パズルはこうです。「ゼロの列（例：『0000』）から始めて、これらのルールを何度も繰り返し適用することで、最終的に『1』の列（例：『1111』）に変えることができるか？」

この論文は、この単純な言葉遊びが、一般的なケースにおいてすでに解決不可能であることを証明しています。次に、著者は巧妙な手品を行います。この言葉遊びのルールを、高階ベータ・マッチングの言語へと直接翻訳するのです。もしマッチング・パズルを解けるのであれば、この言葉遊びも解けるはずであることを示します。言葉遊びがすでに解決不可能であると分かっている以上、マッチング・パズルもまた解決不可能であるはずです。

この証明が特別な理由は、それが**機械化されている（mechanized）**点にあります。著者は単に紙の上に証明を書いたのではありません。彼は、Rocq Prover（旧称 Coq）と呼ばれる「証明支援系」にその証明を読み込ませました。これは、超厳格な論理学者のように振る舞うソフトウェアです。それは、議論のあらゆるステップをチェックし、隙や仮定、そして人間によるミスがないことを保証します。その結果、機械によって検証された「認定済み」の証明が得られました。これは、論理の不備を排除するという意味で、数学において非常に大きな意味を持ちます。

また、この論文は驚くべき関連性を明らかにしています。このマッチング問題が解決不可能であることを証明するために用いられたのと同じ論理構造は、他の二つの有名なパズルが解決不可能であることを証明するためにも使用できます。それは型包含問題（Intersection Type Inhabitation）（特定の型のコードが存在し得るかという問題）と、ラムダ定義可能性（以前の証明で使用されていた元の複雑な問題）です。まるで著者が、コンピュータサイエンスの世界にある三つの異なる扉の「不可能」な性質を解き明かす、たった一つのマスターキーを見つけ出したかのようです。

要約すれば、この論文は単に「この問題は難しい」と言っているだけではありません。古い論理の絡まり合った網を、誰にでも（あるいはコンピュータにでも）辿ることができるクリーンで直線的な道へと置き換え、なぜそれが解決不可能なのかを、シンプルで検証可能な、機械にチェックされた経路を通じて示しているのです。この論文は、これらの特定の論理パズルに関して、計算の宇宙には明確な限界が存在し、我々はその限界を越えるプログラムを書くことは決してできないということを裏付けています。