技術的サマリー：記号的モデル性質を介した一階述語論理フラグメントの決定可能性結果

問題定義

一階述語論理（FOL）は、連結リストや木構造のデータ構造など、非有界ドメインを伴うシステムの検証条件を指定するための強力な形式体系である。しかし、FOL は一般的に決定不可能である。有限モデル性質（充足可能な式はすべて有限モデルを持つという性質）は決定可能性を意味するが、FOL の多くの有用なフラグメントはこの性質を持たない。それらは無限モデルのみを許容する可能性がある。その結果、FOL に依存する検証ツールは、無効な式に対する反モデルを見出せず、ユーザーに実行可能なフィードバックを提供できない場合がある。

既存の決定可能なフラグメント、例えば Stratified Formulas（SF）フラグメント（EPR の多様型変種）は、有限モデル性質を保証するために量化子交代グラフに厳密な非循環制約を課す。これらの制約は複雑なシステムをモデル化する際にしばしば過度に制限的であり、仕様を適応させるために多大なユーザーの努力を要する。本論文は、有限モデル性質を享受しない FOL フラグメント、特に特定の順序論的制限が満たされる場合に、特定のソートにおける量化子交代グラフ上の自己サイクルを許容するフラグメントの決定可能性を確立するという課題に取り組む。

手法

著者は、標準モデルを許容する任意の基底理論に対して、もともと [15] で線形整数算術（LIA）を用いて導入された「記号的構造（symbolic structures）」の一般化を提案する。

1. 一般化された記号的構造

記号的構造とは、潜在的に無限の一階構造の有限表現である。これは以下の要素から構成される：

• ノード： 基底理論 $T$ の標準モデルのドメインの部分集合を表すノードの有限集合。
• 束縛式： 各ノードは、それが表す要素の集合を定義する $T$ の言語における式に関連付けられる。
• 記号的解釈： 定数、関数、関係の解釈は、$T$ からの項と式を用いて記号的に定義される。

記号的構造の鍵となる性質は、モデル検査（構造が式を満たすかどうかを決定すること）が基底理論 $T$ における式の妥当性帰着することである。$T$ が決定可能であれば、記号的構造に対するモデル検査も決定可能である。

2. 記号的モデル性質

本論文は、FOL の特定のフラグメントに対して記号的モデル性質を確立する。あるフラグメントがこの性質を許容するとは、そのフラグメント内のすべての充足可能な式が、決定可能な基底理論上の充足可能な記号的構造を持つことを意味する。そのような構造に対するモデル検査が決定可能であるため、この性質の存在は、そのフラグメントの充足可能性問題の決定可能性を意味する。

3. 順序付き自己サイクル（OSC）ファミリー

著者は、区別されたソート $s_\infty$ 上の厳密順序関係 $\prec$ の公理化 $\alpha$ によってパラメータ化された、**Ordered Self-Cycle（OSC）**と呼ばれるフラグメントのファミリーを定義する。

• SF の緩和： OSC は、非循環性の要件を緩和することで Stratified Formulas フラグメントを拡張する。量化子交代グラフに他のサイクルが存在しない限り、ソート $s_\infty$ 上で関数記号が自己ループ（サイクル）を導入することを許容する。
• 基底理論： 本論文は 2 つの主要な基底理論を利用する：
  • 線形整数算術（LIA）： 全順序のために使用される。
  • 決定可能な文字列理論（STR）： 接頭辞順序のために使用される。

4. 証明の構成

決定可能性の証明は、式 $\phi$ の任意のモデル $M$ から記号的モデル $S$ を構築する一般的な「証明レシピ」に従う。この構築には以下が含まれる：

1. 分割： $M$ のドメインを、それらが満たす原子式（アトム）に基づいて同値類に分割する。これらのクラスが記号的構造のノードとなる。
2. 解釈： 定数、単項関係、および順序 $\prec$ の解釈を、$M$ で満たされるアトムを「観測」するように定義する。
3. 混合順序アトムの処理： 核心的な難しさは、混合順序アトム（例：$f(x) \prec g(x)$）と順序公理 $\alpha$ を満たすことにある。これは、基底理論内でノード（サマリーノード）と関数項に対して特定の内部形状を定義することで達成される。
   • 全順序（tot）の場合： サマリーノードは双方向に無限の直線（整数）としてモデル化され、項順序の「普遍的有限埋め込み性」を可能にする。
   • 接頭辞順序（pref）の場合： サマリーノードは、接頭辞順序の非線形な性質に対応するために、「普遍的木」（特定の分岐因子を持つ双方向に無限の木）としてモデル化される。

主要な貢献

1. 記号的構造の一般的な定義： 本論文は、LIA に限定された以前の作業を一般化し、標準モデルを持つ任意の基底理論上の記号的構造のパラメトリックな定義を提供する。
2. OSC ファミリーの導入： 特定の公理の下で順序付きソート上の自己サイクルを許容することで Stratified Formulas を拡張する、Ordered Self-Cycle ファミリーを定義する。
3. 新たな決定可能性結果： 著者は、OSC ファミリー内のいくつかの新しいフラグメントの決定可能性を証明する。具体的には：
   • OSC[pref]： 文字列理論を用いた接頭辞順序付き自己サイクル。このフラグメントは、非循環木構造データ構造および共有を伴う連結リストにおける到達可能性をモデル化する。
   • 後継者/先行者を持つ変種： 全順序/接頭辞順序と、後継者の存在（prosucc）または先行者の存在（regpred）を保証する公理を組み合わせたフラグメント。
4. 汎用的な証明フレームワーク： これらのフラグメントに対して記号的モデルを構築する統一された証明技法が提示され、充足可能性がそれぞれの決定可能な基底理論（LIA または STR）における式の妥当性へ帰着することを示す。
5. 実装： 文字列理論上のモデル検査を含む汎用的な記号的構造をサポートするよう拡張されたオープンソースの FEST ライブラリを用いた概念実証ツールが実装された。

結果

本論文は、以下のフラグメント（ここで $\alpha$ は順序公理）に対して充足可能性問題が決定可能であることを確立する：

• $\alpha \in \{ \text{tot}, \text{tot} \land \text{prosucc}, \text{tot} \land \text{regpred}, \text{pref}, \text{pref} \land \text{prosucc}, \text{pref} \land \text{regpred} \}$。

tot に関する結果は先行研究 [15] を再述するものであるが、pref およびその変種に関する結果は新規である。特に OSC[pref] の決定可能性は、有限モデル性質を許容しないが文字列理論を用いて記号的に表現可能な構造を扱う点で極めて重要である。

意義と主張

本論文は、有限モデル性質を超えた決定可能性への新たなアプローチを提供すると主張する。記号的構造を利用することで、有限の反モデルの欠如により以前は処理が困難だった非有界ドメインを持つシステムの検証を可能にする。

• 理論的影響： 有限モデル性質と無限モデル表現の間のギャップを埋め、無限モデルが必要であっても、それらが決定可能な基底理論によって捉えられる限り、決定可能性を達成し得ることを示す。
• 実用性： OSC[pref] フラグメントは、厳密な階層化フラグメントではモデル化が困難な、木構造データ構造および共有を伴う連結リストに関連する一般的な検証シナリオに直接対応する。
• 一般性： このフレームワークは他の基底理論や順序関係へ拡張可能に設計されており、さらなる決定可能フラグメントを発見する道筋を示唆している。

著者は、決定手続きが充足可能性を基底理論における式の妥当性（文字列理論の場合は非要素級である可能性がある）へ帰着させるものの、主要な貢献は決定可能性の確立と、検証失敗時に記号的な反モデルを生成する能力にあると指摘する。実装は、このアプローチの実現可能性に関する概念実証として機能する。