Nonlinear Arithmetic with SMTLIB Division is Undecidable

あなたが非常に厳格な一連の規則を用いて謎を解こうとする探偵だと想像してください。コンピュータ科学の世界では、これらの規則は「理論」と呼ばれ、数学的なパズルに解が存在するかどうかをコンピュータが判断するのを助けます。

この論文は、**非線形実数算術（NRA）**と呼ばれる特定の規則セットについて扱っています。これは、3.14、-5、0.001 などの実数を用いて、それらを足し算、引き算、掛け算、割り算を行うゲームだと考えてください。

ゲームを破綻させる「魔法」の規則

長らく、数学者たちはこのゲームが完全に解けると信じていました。コンピュータにこれらの数値を用いたパズルを与えれば、いずれ「はい、解があります」とか「いいえ、解はありません」と答えることができるはずです。

しかし、著者であるデヤン・ヨヴァノヴィッチは、公式の規則書（SMTLIB 標準）に隠された罠を発見しました。その罠は、規則がゼロによる割り算をどのように扱うかにあります。

通常の数学では、ゼロで割ることは大きな「ダメ」です。しかし、この特定のコンピュータ規則書では、規則はこう述べています。「ゼロで割る場合、答えが何であれ構いません。ゼロ以外で割らない限り、それが通常の数のように振る舞う限り、何でも構いません」

著者はこれを**「解釈されていない関数」**と呼びます。比喩を使えば、すべてのスナック菓子に対して完璧に機能する自動販売機を想像してください。しかし、「ゼロ・スナック」を買おうとすると、機械はクラッシュするのではなく、単に「何か」を吐き出します。もしかしたらチョコレートバーかもしれませんし、岩かもしれませんし、雲かもしれません。規則はそれが何になるかを教えてくれません。「何かが出てくる」と言うだけです。

これがゲームを解けないようにする仕組み

この論文は、この「何でもあり」のゼロ除算規則が、混沌への扉を開く鍵であると主張しています。

以下に、その論理を簡略化して示します。

1. 目的: 著者は、この「魔法」の割り算規則があれば、コンピュータを騙して整数のパズル（1、2、3 などの整数を用いたパズル）を解かせることができることを証明したいと考えています。
2. 問題: 整数のパズルを解くことは、すべてのケースに対してコンピュータが完璧に行うことが有名な不可能です（これはヒルベルトの第 10 問題として知られています）。それは、常に成長し続ける干し草の山から針を見つけるようなものです。
3. トリック: 著者は、「魔法」のゼロ除算を用いることで、数学的な橋を構築できることを示しています。この割り算のトリックを用いて、難しい整数パズルを実数パズルに変換できます。
   • 比喩: 人間だけが理解できる言語（整数）で書かれた秘密の暗号があると想像してください。そして、この暗号をコンピュータが理解できる言語（実数）に翻訳する機械（割り算のトリック）を構築します。コンピュータの言語にはこの「魔法」のゼロ除算規則があるため、コンピュータは偶然にも人間の暗号を解いてしまうのです。
4. 結果: 全ての整数パズルをコンピュータが解くことはできないと分かっています。そして、このトリックはコンピュータに実数を用いて整数パズルを解かせようとさせるため、コンピュータは全ての実数パズルも解くことはできません。ゲームは決定不能になります。

「床」関数の比喩

これを証明するために、著者は巧妙なトリックを用います。もしこの「魔法」の割り算があれば、コンピュータを床関数（3.9 を 3 などに、最も近い整数に切り捨てる関数）のように振る舞わせることができることを示しています。

一度、コンピュータが数を切り捨てることができれば、整数を数え始めることができます。整数を数えることができれば、それらの不可能な整数パズルを解こうと試みることができます。それらのパズルは一般的に解くことが不可能であるため、この割り算規則を含む実数数学のシステム全体も、一般的に解くことが不可能になります。

現実世界への意味（論文によると）

この論文は、将来の AI や医療用途については言及していません。現在のコンピュータベンチマーク（テスト問題）の現状に焦点を当てています。

• 罠: SMTLIB ライブラリ（コンピュータをテストするために使用される膨大な数学パズルのコレクション）の多くの既存のテスト問題は、変数を用いた割り算（例えば x / y）を使用しています。もし y がたまたまゼロであれば、これらのパズルは「決定不能」の罠に陥ります。
• 解決策？: 著者は、規則書を修正するための 2 つの方法を提案しています。
  1. 特定の答えを選ぶ: 整数の扱い方と同様に、ゼロで割ることを常に特定の数（0 や 1 など）に等しいと決定します。
  2. ゲームを分割する: 変数で割る問題のための新しい、独立したカテゴリを作成し、既知の数（定数）でしか割らない問題のための「安全な」カテゴリを維持します。

結論

この論文は、コンピュータが「ゼロで割る」ことをどのように扱うかについての、一見無害な特定の規則が、偶然にもコンピュータが実数を含むすべての数学的問題を解く能力を破綻させていると主張しています。これは、コンピュータが本来解くことができないはずの問題をこっそり解くことを許すことで、解けるゲームを解けないものに変えてしまいます。