A proof-theoretic approach to abstract interpretation

巨大で混沌とした都市（具体的な世界）を、簡略化された記号的な言語しか話さない友人（抽象的な世界）に説明すると想像してください。その都市には無限の通り、建物、そして複雑なパターンで移動する人々がいます。友人はそのような詳細な情報を処理できないため、嘘をつかずに都市の振る舞いを要約する方法が必要です。これが抽象解釈の核心的な問題、すなわち複雑な現実の安全で簡略化された地図を作成することです。

本論文は、その簡略化された地図のための「文法」または論理を構築する新しい方法を提案しています。地図が従うべき規則を単に推測するのではなく、著者たちは、その地図と完全に一致する完璧な論理体系を生成するための機械的なレシピを提案しています。

以下に、日常の比喩を用いた彼らのアイデアの概要を示します。

1. 翻訳者と地図

複雑な都市を、ありうるすべてのシナリオの巨大な集合だと考えてください。「抽象格子（Abstract Lattice）」は、有限で管理可能な特性のチェックリストです（例：「信号は赤か？」「橋は開いているか？」）。

都市とチェックリストを結びつけるには、2 人の翻訳者が必要です。

• アップ翻訳者（抽象化）: 散らかった現実世界の状況を扱い、「これはカテゴリ A に当てはまる」と言います。
• ダウン翻訳者（具体化）: チェックリストからカテゴリを取り出し、「これはここに当てはまるすべての現実世界の状況を表す」と言います。

著者たちの目標は、その論理の「辞書」がチェックリストと完全に同一であるような論理（推論の規則の集合）を作成することです。チェックリストが「A は B を含む」と述べていれば、その論理は「A は B を含む」を疑いようなく証明できなければなりません。

2. カスタム論理のレシピ

本論文は、任意の有限のチェックリストに対してこの論理を構築するためのステップバイステップの「レシピ」を提供しています。

1. ツールの選択: チェックリストを確認します。都市とチェックリストの間を行き来する翻訳時に正しく機能するツール（「AND」「OR」「NOT」など）はどれかを見極めます。それらのツールのみを保持します。
2. 項目の命名: チェックリストのすべての項目に名前をつけます（箱のラベルのようなものです）。
3. 規則の記述:
   • チェックリストが「箱 A は箱 B の部分集合である」と述べている場合、論理に規則を書きます。「A を持っていれば、B も持っている」。
   • チェックリストが「箱 A と箱 B を組み合わせると箱 C になる」と述べている場合、規則を書きます。「A AND B は C に等しい」。
4. 結果: 著者たちは、このレシピに従えば、生成された論理体系は健全（都市について決して嘘をつかない）であり、完全（チェックリストについて真であるすべてを証明できる）であることを証明しています。

「単純な」警告: 著者たちは、このレシピがナッツを割るために金槌を使うようなものだと認めています。これは任意のチェックリストに対して機能しますが、規則が多くなりすぎ、その中には冗長なものも含まれる可能性があります。これは正しさを保証する「力技」的な方法ですが、最も効率的な方法ではありません。

3. 「デカルト的」対「非デカルト的」なパズル

本論文は、$x$ と $y$ のような 2 つの変数がある場合に何が起こるかを検討します。

• デカルト的アプローチ（グリッド）: $x$ と $y$ を個別にチェックするグリッドを想像してください。これは、台所の温度と寝室の温度を独立してチェックするようなものです。グリッド全体の規則が台所の規則と寝室の規則の単なる和であるため、扱いやすいものです。
• 非デカルト的アプローチ（形状）: 時には、$x$ と $y$ が奇妙な形状でリンクしています。例えば、「$x$ と $y$ の和は 10 未満でなければならない」といった場合です。これはグリッドを斜めに切断します。$x$ と $y$ を個別に見るだけでは不十分で、それらが一緒に作る形状を見る必要があります。

著者たちは、これらの「奇妙な形状」（非デカルト的抽象化）を扱うことが、単純なグリッドに無理やり押し込めようとするよりも、彼らの論理構築レシピにとっては実際には容易であると指摘しています。彼らは次のような戦略を提案しています。複雑でリンクした形状の理論を先に構築し、その後、単純なグリッドのケースがどのようにそれに適合するかを確認する。

4. 八角形の例

彼らの理論を検証するために、「八角形」（$x + y \geq 5$ などの述語）と呼ばれる特定の形状のタイプを検討しました。

• 彼らは、「NOT ($x+y \geq 5$)」を言うことは容易ですが、彼らの特定の規則セットを用いて「($x+y \geq 5$) AND ($x-y \geq 5$)」を言うことは容易ではないことを発見しました。なぜなら、それら 2 つの形状の交差部分が、彼らのチェックリストの単純な「線」形式に適合しないからです。
• これは限界を明らかにしました。「NOT」のみを許可し「AND」を許可しない場合、論理は非常に弱くなります。
• 解決策: 彼らは、「AND」と「OR」を、チェックリストの厳密な一部ではなく、規則に関する規則（メタ規則）として許可することを提案しました。これにより、彼らのシステムを壊すことなく、複雑な矛盾（状況が不可能であることを証明するなど）を処理できるようになります。

要約

簡単に言えば、この論文は、コンピュータ・プログラムの簡略化されたモデルと完全に一致するカスタム言語の設計図です。

• 問題: 複雑なソフトウェアを検証する必要がありますが、すべての可能性をチェックすることはできません。そのため、簡略化されたモデルを使用します。
• 解決策: 著者たちは、その簡略化されたモデルについて推論するために必要な論理規則の正確なセットを生成する機械的な方法を提供します。
• 洞察: 時には、リンクした変数を個別の独立したバケット（デカルト的）に無理やり押し込めるよりも、単一の複雑な形状（非デカルト的）として扱う方が数学的に整理されています。

この論文は、すべてのソフトウェアのバグを解決したり、将来の医療結果を予測したりするとは主張していません。これは厳密に、検証に使用される「簡略化された地図」が一貫性があり信頼できる論理規則のセットを持っていることを保証するための数学的機械を提供するものです。