💻 computer science

Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

本論文は、数と直観的ポイントトゥ述語のみからなる分離論理の最小限の断片において、ペアノ算術の $\Pi_0^1$ 論理式の変換を通じてその妥当性の決定不能性を示し、数値を扱う実用的なソフトウェア検証における論理体系の表現力を明らかにするものである。

原著者： Sohei Ito, Makoto Tatsuta

公開日 2026-03-20

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

CC BY 4.0

原著者： Sohei Ito, Makoto Tatsuta

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

この論文は、**「とてもシンプルで小さな『魔法の道具箱』が、実は『すべての数学の真理』を表現できるほど強力だ」**という驚くべき発見について書かれています。

専門用語を避け、日常の例え話を使って解説します。

1. 物語の舞台：メモリの「部屋」と「メモ」

まず、この論文で扱っている「セパレーション・ロジック（分離論理）」とは何かを想像してください。

メモリ（Heap）： 巨大な倉庫のようなものです。そこには無数の「部屋（セル）」があり、それぞれに番号が振られています。
ポインタ（Points-to）： 「部屋 A には、部屋 B の鍵が入っている」というメモです。これがこの論理の唯一の「道具」です。
数字（0 と successor）： 「0」という数字と、「次の数字（+1）」を作るルールだけです。足し算や掛け算は最初からありません。

通常、この「倉庫の部屋と鍵」だけを扱う論理は、計算機科学では**「とても簡単で、答えがすぐにわかる（決定可能）」**ものだと考えられてきました。まるで、単純なパズルを解くようなものです。

2. 驚きの発見：小さな道具箱に「無限」が隠されていた

しかし、この論文の著者たちは、このシンプルな道具箱に**「0」と「次の数字（+1）」**という 2 つのルールを少しだけ加えてみました。

すると、奇妙なことが起きました。
この「シンプルすぎる道具箱」を使って、**「ペアノ算術（私たちが学校で習うような、無限に続く自然数の世界）」**の複雑な問題をすべて表現できるようになったのです。

【例え話】

元の状態： 倉庫に「部屋 A に鍵 B がある」と書くだけの、単純なメモ帳。
変化： そのメモ帳に「0」と「次の数字」を書くルールを少し足しただけ。
結果： そのメモ帳だけで、**「すべての数学の難問（特に『ある計算が永遠に終わらないか』という問題）」**を記述できるようになってしまいました。

3. どのようにして「足し算」や「掛け算」を実現したのか？

不思議なことに、この道具箱には「足し算」や「掛け算」の機能はありません。では、どうやって計算しているのでしょうか？

著者たちは、**「倉庫の中に巨大な『計算表（辞書）』を並べる」**というトリックを使いました。

足し算の表： 「部屋 0, 1, 2, 3」に「0, 1, 2, 3」と並べ、「0+1=1」なら、特定の部屋に「1」が書かれていることを示す。
掛け算の表： 別の部屋に「1, 2, 3, 6」のように「2×3=6」の結果を並べる。

この「計算表」が倉庫の中に正しく並んでいるかどうかをチェックするルール（魔法の呪文）を作ることで、**「倉庫の中に正しい表があれば、足し算や掛け算ができたことになる」**と定義しました。

つまり、**「計算そのもの」ではなく、「計算結果が書かれた表があるかどうかもチェックする」**ことで、複雑な数学を表現しているのです。

4. なぜこれが重要なのか？（「答えがわからない」ことの証明）

この発見がなぜ画期的かというと、**「答えが永遠にわからない問題」**を証明したからです。

従来の常識： 「シンプルな道具箱」なら、コンピュータがすぐに正解を出せるはずだ。
この論文の結論： 「0」と「+1」さえあれば、この道具箱は**「チューリングマシン（計算機）」と同じくらい強力になり、「あるプログラムが止まるかどうか（停止性問題）」**を判定できるほど複雑になる。

つまり、**「このシンプルな道具箱で書かれた式が、本当に正しいかどうかを、コンピュータが自動的に判断することは、原理的に不可能（決定不能）」**であることが証明されました。

【例え話】
「シンプルなパズル」だと思っていたら、実はそのパズルの中に「神様しか解けない難問」が隠されていたようなものです。

5. 逆説的な弱点：「存在する」は言えない

面白いことに、この方法は「すべての数について成り立つか（∀）」という問いには完璧に機能しますが、「ある数が見つかるか（∃）」という問いには弱いです。

成功： 「すべての数字について、足し算の表が正しいか？」→ 表が小さければ「わからない（＝真とみなす）」というルールで、数学的な真理を再現できる。
失敗： 「ある数字が見つかるか？」→ 表が小さすぎて答えが見つからない場合、論理が破綻してしまう。

これは、「完璧な辞書（無限の表）」があれば何でも言えるが、「不完全な辞書」では「何かがある」という主張は裏付けられないという、論理の限界を示しています。

まとめ

この論文は、**「非常に制限された、シンプルな論理体系（倉庫と鍵）でも、数字のルール（0 と +1）を少し加えるだけで、人類が抱える最も難しい数学的真理（ペアノ算術）をすべて表現できてしまう」**ことを示しました。

それは、**「最小限のツールで、最大限の複雑さを描き出す」**という、論理の世界における驚くべき「魔法」の発見です。

一言で言えば：
「シンプルすぎる道具箱に、たった 2 つの数字のルールを加えただけで、実は『すべての数学』を表現できてしまうほど強力だった。だから、その道具箱の正しさを機械でチェックするのは、永遠に不可能なんだよ！」

論文「Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic」の技術的サマリー

1. 概要と問題設定

本論文は、数値（自然数）を拡張した分離論理（Separation Logic）の最小限のフラグメントの表現力について調査したものである。具体的には、直感的なポイントトゥ述語（intuitionistic points-to predicate: $t_1 \mapsto t_2$ ）、定数 $0 $、および後継関数$ s$ のみからなるフラグメント（SLN と呼称）が、ペアノ算術（Peano Arithmetic: PA）のすべての $\Pi^0_1$ 式を符号化できることを示している。

従来の分離論理の研究では、メモリ状態の記述に特化しており、数値計算を含む場合の決定可能性が課題となっていた。Presburger 算術（加算のみ）は決定可能であるため、これと分離論理を組み合わせれば決定可能になるという期待があったが、本論文は極めて単純な構文（ $0, s, \mapsto$ のみ）であっても、算術の $\Pi^0_1$ 式を表現可能にすることで、妥当性判定問題が決定不可能（undecidable）になることを証明した。

2. 手法と主要な技術的貢献

2.1 算術演算のヒープ内符号化

本論文の核心は、ヒープ（メモリ）上に**演算テーブル（operation table）**を構築し、加算、乗算、不等式関係をヒープの構造として表現する点にある。

タグ付きセル構造:
- 加算（Add）: タグ 0 を持つセル列 [0, x+3, y+3, x+y+3]
- 乗算（Mult）: タグ 1 を持つセル列 [1, x+3, y+3, x*y+3]
- 不等式（Ineq）: タグ 2 を持つセル列 [2, x+3, y+3]
- ここで $3$ はタグ（0, 1, 2）との衝突を避けるためのオフセットである。
テーブル条件 $H$ :
- 加算と乗算の基底ケースおよび帰納ステップを強制する論理式（ $HAdd_1, HAdd_2, HMult_1, HMult_2$ ）と、不等式の推移性を保証する式（ $HIneq_1, HIneq_2$ ）を定義する。
- この条件 $H$ を満たすヒープが存在すれば、そのヒープ内のテーブルはペアノ算術の演算結果を正しく反映する。

2.2 PA から SLN への翻訳

ペアノ算術の $\Pi^0_1$ 式（ $\forall x \le t. B$ のような有界量化子のみを含む式）を SLN 式へ翻訳する変換 $(\cdot)^\circ$ を定義した。

翻訳の戦略:
- 算術式 $x = y + z$ や $x \le y$ を、直接の算術演算子ではなく、ヒープ内のテーブルを参照する述語（$Add, Mult, Ineq$）に置き換える。
- ヒープのサイズ問題への対処: 翻訳された式は「任意のヒープに対して成り立つ」ことを要求する。ヒープが演算テーブルを十分に持たない場合、テーブル参照は失敗（真となる）し、式は自明に真となる。逆に、十分なサイズの「単純テーブルヒープ（simple table heap）」が存在すれば、算術的真理と SLN の真理が一致する。
- この「不十分なヒープでは真になり、十分なヒープでは算術真理と一致する」という性質を利用し、 $\Pi^0_1$ 式の妥当性（すべてのモデルで真か）を保存する翻訳を実現した。

2.3 $\Sigma^0_1$ 式への限界

翻訳は $\Pi^0_1$ 式に対しては妥当性を保存するが、 $\Sigma^0_1$ 式（ $\exists x. B$ ）に対しては成立しないことを示した。

反例: $\exists x (x + 0 \neq x)$ は PA で偽であるが、翻訳後は「ある大きな $x$ に対してヒープがテーブルを持たない場合、 $x+0$ の計算が定義されず、結果として式が真になる」という挙動を示し、SLN において妥当（すべてのヒープで真）となってしまう。これは、 $\Sigma^0_1$ 式が「存在する witness」を要求する性質と、ヒープが不完全な場合の翻訳の振る舞いが矛盾するためである。

3. 主要な結果

表現定理（Representation Theorem）:
- PA の任意の $\Pi^0_1$ 式 $A$ について、 $A$ が標準モデルで妥当であることと、その翻訳 $A^\circ$ が SLN の標準解釈で妥当であることは同値である。
- これにより、SLN の妥当性判定問題は PA の $\Pi^0_1$ 式の問題に帰着される。
決定不可能性（Undecidability）:
- PA の $\Pi^0_1$ 式（およびその否定である $\Sigma^0_1$ 式）の妥当性は決定不可能（停止問題と関連）であるため、SLN の妥当性判定も決定不可能であることが導かれる。
- 極めて単純な構文（分離論理の最小コア＋算術の基礎）だけで、計算理論上の難問を表現できることが示された。
$\Pi^0_1$ -完全性（ $\Pi^0_1$ -Completeness）:
- 下限: 上記の翻訳により $\Pi^0_1$ -困難（ $\Pi^0_1$ -hard）であることが示された。
- 上限: SLN のモデルチェッキング問題（与えられたヒープと変数割り当てに対する式の真偽判定）が決定可能であることを証明し、これを用いて妥当性判定問題を $\Pi^0_1$ 式として記述可能であることを示した。
- 結論として、SLN の妥当性判定問題は $\Pi^0_1$ -完全である。
代替証明:
- 有限モデル理論（Trakhtenbrot の定理）からの帰着を用いた、より簡潔な決定不可能性の証明も提示されている。

4. 意義と結論

理論的意義:
- 分離論理の決定可能性の境界を明確にした。従来の研究では、分離論理に算術を組み合わせると決定不可能になるケースが多かったが、本論文は「分離論理の最小コア（1 フィールドのポイントトゥ）＋ 0 と後継関数」という極めて制限された環境であっても、 $\Pi^0_1$ 完全な計算能力を持つことを示した。
- これは、メモリ操作と数値計算が組み合わさることで、論理の表現力が飛躍的に高まることを示唆している。
実用的含意:
- プログラム検証において、数値計算を含むヒープ操作を扱う場合、その論理体系が決定可能であることを保証するのは極めて困難であることを示している。
- 一貫性（consistency）や強正規化（strong normalization）といった、ペアノ算術で記述される重要な性質が、この最小限の分離論理フラグメント内でシミュレート可能であることは、形式手法の限界と可能性の両面から重要な知見である。

本論文は、分離論理の表現力の理論的限界を再定義し、数値を含むメモリ操作の検証における決定可能性の問題について、新たな視点を提供する重要な成果である。