技術要約：命題動的論理（PDL）はクレイグ補間性を有する

1. 問題設定

本論文は、命題動的論理（PDL）がクレイグ補間特性（CIP）を持つか否かという、長年の未解決問題に取り組んでいる。CIPとは、任意の妥当な含意 $\phi \to \psi$ に対して、$\phi \to \theta$ および $\theta \to \psi$ が妥当であり、かつ $\theta$ が $\phi$ と $\psi$ の両方に共通する命題文字および原子プログラムのみを含むような補間式 $\theta$ が存在することを指す。

PDLは、決定可能性や完全性の結果が確立された、よく研究されている様相論理であるが、その補間性のステータスは数十年にわたり不明なままであった。文献には、補間の証明に関する3つの過去の試みが記載されている：

1. Leivant (1981): 証明を主張したが、Kracht (1999) によってその理由が誤りであるとして反駁された。ただし、Leivantの証明には真の欠落（ギャップ）が残っている。
2. Borzechowski (1988): 証明を主張した修士論文（Diplomarbeit）であり、ほとんど注目されず、検証不可能であるとして一部で退けられた。
3. Kowalski (2002): 証明を主張したが、これは反駁され、2004年に公式に撤回された。

困難の本質は、PDLが様相不動点論理（反復演算子 $*$ によるもの）である点にある。補間性は、循環的証明系を用いたフル $\mu$-calculus およびその交互作用のない断片については確立されているが、PDL特有の制約により、補間式を特徴付ける不動点方程式の解を、フル $\mu$-calculus の表現力を必要とせず、いかにしてPDLの範囲内で表現するかを保証することが困難となっている。

2. 手法

著者らは、循環的タブロー・システムに基づき、Maeharaの証明論的手法を適応させた構成的な証明を提供している。

2.1. PDLのための循環的タブロー・システム

著者らは、分割されたシーケント（式の集合のペア）上で動作する、PDLのための新しいタブロー・システムを定義している。主な特徴は以下の通りである：

• 局所的推論と様相的推論: システムは、局所的な推論（単一の状態内での命題論理およびプログラムの展開）と、様相的な推論（クリプキ・モデルにおける状態間の移動）を区別する。
• 展開メカニズム: 各プログラム構成子に対する標準的な簡約ルールの代わりに、システムは「ローディング（loading）」メカニズムを使用する。$[\alpha]\psi$（ここで $\alpha$ は非原子的）という形式の式は、「テスト・プロファイル」に基づき、有限個のシーケントの集合へと展開される。この集合 $\text{unfold}_\square(\alpha, \psi)$ は、特定のテストが成功または失敗する場合の、$\alpha$ のすべての可能な実行パスの選言を表す。
• 反復の処理: $[\alpha^*]\psi$ のような式の無限の局所展開を防ぐため、システムは展開プロセス中に再生成された式の出現を排除する。これは、$[\alpha^*]\psi$ が最大不動点であるという観察に基づいている。
• 循環的証明: システムは「リピート（繰り返し）」（祖先となるノードと同じラベルを持つノード）を許容する。
  • ロードされたパスのリピート (Loaded-path repeats): 祖先（コンパニオン）から現在のノードまでのパスがすべてロードされたノードで構成されているリピート。これらは「成功した」リーフとして扱われる（式を満たすループであることを示す）。
  • 自由なリピート (Free repeats): パースにアンロードされたノードが含まれるリピート。これらは「失敗した」リーフとして扱われ、潜在的な反例モデルを示唆する。
• 停止性: すべての自由なリピートおよびロードされたパスのリピートがリーフであることを強制し、またFischer-Ladner閉包を利用することで、式の集合を限定することにより、有限性を確保する。

2.2. 準タブローと不動点方程式による補間

補間式を構成するために、著者らは循環的な設定においてMaeharaの手法を適応させている：

• クラスター: タブローは、リピートからコンパニオンへの逆向きのエッジを持つグラフとして捉えられる。このグラフの強連結成分（SCC）を「クラスター」と呼ぶ。
• 準タブロー (Quasi-tableaux): 正当なクラスター（非単一のSCC）に対して、著者らは「準タブロー」を定義する。この構造は、補間式を特徴付ける一連の方程式を設定するために使用される。
• 前補間式 (Pre-interpolants): 手法は、リーフからルートへの帰納法を通じて、準タブロー内のノードに対する「前補間式」を定義する。
  • 脱出ノード (Exit nodes): クラスターの一部ではないリーフにおいて、前補間式は、帰納法の仮定に基づき、その脱出ノードの補間式となる。
  • リピート・リーフ (Repeat leaves): リピート・リーフにおける前補間式は、内部の命題変数 $q_x$ である。
  • コンパニオン・ノード (Companion nodes): コンパニオン $x$ の子が、前補間式 $\iota_y \equiv \bigwedge_i [\alpha_i]q_x \wedge \bigwedge_j [\beta_j]q_{z_j} \wedge \psi$ を持つ場合、コンパニオン $x$ の前補間式は $\iota_x := [(\bigcup_i \alpha_i)^*](\bigwedge_j [\beta_j]q_{z_j} \wedge \psi)$ として定義される。
• PDLにおける解法: この特定の構成の核心的な洞察は、不動点方程式の解がPDLの言語内に留まることを保証している点にある。$\iota_x$ の定義における反復演算子 $*$ の使用は、この $\iota_x \equiv \iota_y\langle q_x \mapsto \iota_x \rangle$ という方程式をPDL内で効果的に解いている。
• 最終的な補間式: クラスターのルートに対する最終的な補間式は、ルートの前補間式に含まれる内部変数を、対応するリージョン式（分割されたシーケントの左辺の選言）で置換することによって得られる。

3. 主な貢献と結果

• PDLに対するCIPの証明: 本論文は、PDLがクレイグ補間特性を持つことを確立した。
• ベス定義可能性: 補題として、本論文はPDLがベス定義可能性を持つことを証明している（演繹定理が存在する場合、CIPはベス定義可能性を導くため）。
• 構成的アルゴリズム: 証明は構成的である。著者らは、閉じたタブローから補間式を計算するための明確なアルゴリズムを提供している。
• 形式検証: 著者らは、証明の一部をインタラクティブ定理証明器 Lean 4 で形式化した。論文執筆時点では、健全性と完全性の定理、およびいくつかの補助的な補題が検証されている。
• 実装: タブロー・システムと補間式構成のHaskell実装が提供されており、ウェブインターフェース経由で利用可能である。

4. 意義と主張

本論文は、PDLの補間性のステータスに関する文献上のパズルを解決し、以前の試みの欠陥を克服する最初の検証済み証明を提供していると主張している。

• 歴史的問題の解決: 著者らは、Borzechowski (1988) の核心的なアイデアに基づきつつ、循環的証明の扱いとPDLの言語内での補間式の構成を厳密に形式化することで、過去の失敗した試みの歴史に明示的に対処している。
• 手法の新規性: Maeharaの手法は非循環的な証明には標準的であるが、循環的証明（不動点論理）に適用するには不動点方程式を解く必要があることを強調している。著者らは、PDLにおいては、これらの解がPDL自身の反復演算子を用いて表現できることを示しており、これは、そのような解がフル $\mu$-calculusを必要とする他の断片とは異なる、非自明な結果である。
• 未解決問題: 著者らは、彼らの手法がテスト・プログラム ($\tau?$) の存在に依存していることを謙虚に述べている。したがって、テストを含まないPDLの断片が補間性を持つかどうかは依然として未解決の問題である。なぜなら、彼らの構成は、入力がテストフリーであっても、一般にテストを含む補間式を生成するためである。また、彼らの手法を他のPDLの変種（共役や交差を含むもの）へ拡張することや、Kleene Algebra with Tests (KAT) への影響についても、今後の課題として残している。

要約すると、本論文は、新しい循環的タブロー・システムと、補間式のための特殊な不動点解法を用いた、PDLに対するクレイグ補間性の決定論的かつ構成的な証明を提供するものであり、Haskellによる実装と、Leanによる部分的な形式検証の両方によって裏付けられている。