Towards Weak Stratification for Logics of Definitions

技術要約：定義の論理に向けた弱層化に向けて

問題提起
定義の論理は、推論規則によって規定される判断をエンコードし、推論するための論理のファミリーである。そこでは、原子述語がそれ自体に依存する論理式に関連付けられる。このような定義に内在する明白な循環性を解決するため、標準的な手法は「層化条件（stratification condition）」を課す。これは、述語が自身の定義の本体において負の出現（含意の左側）をしないことを保証するものである。この条件は、定義を単調な不動点演算子として扱うものである。

しかし、多くの有用な仕様、特にプログラミング言語の性質を証明するための論理関係（logical relations）を伴うものにおいては、述語が負に出現することを必要とする定義が必要となる。Abella証明支援システムの基礎となる論理 $\mathcal{G}$ では、このような定義は許可されていない。Tiu [19] は以前、層化条件を「弱層化（weak stratification）」（ヘッドのレベルが負の出現のレベルよりも厳密に大きい場合に限り、負の出現を許可すること）へと緩和した $\mathcal{LD}$ という論理を導入したが、$\mathcal{LD}$ はコアフラグメントに限定されていた。それは、名前やフレッシュネス（freshness）を名目定数を通じて扱うために不可欠なナブラ量化子（$\nabla$）や、自然数帰納法を超えた一般的な帰納的定義をサポートしていなかった。本研究が取り組む課題は、$\nabla$ および一般的な帰納的定義を伴う場合においても一貫性を維持しながら、定義の論理を弱層化へと拡張することである。

手法
本論文では、Tiuの $\mathcal{LD}$ にナブラ量化と一般的な帰納的定義を拡張した新しい論理 $\mathcal{LD}\mu\nabla$ を定義する。手法は主に以下の3つの段階で進行する。

1. $\mathcal{LD}\mu\nabla$ の構文と意味論：
   本論理は、定義の集合 $\mathcal{D}$ と帰納的定義の集合 $\mathcal{I}$ を持つ、一次述語シーケント計算の拡張として定式化される。

• 弱層化： 定義の集合 $\mathcal{D}$ は、すべての節 $H \triangleq_X B$ と接地代入 $\rho$ に対して $\text{lvl}(H\rho) \ge \text{lvl}(B\rho)$ であるとき、弱層化されているという。決定的なのは、ヘッドのレベルが負の出現のレベルよりも厳密に大きい場合に限り、負の出現を許容できる点である。
• 帰納のための厳密な層化： 本論文では、帰納的定義 $\mathcal{I}$ に対してより厳格な条件を課している。すなわち、それらは「厳密に」層化されていなければならない（接地原子述語のレベルは、その引数に依存しない）。この制限は、帰納法と弱層化を組み合わせた際に生じる不整合を防ぐために必要である。
• ナブラ量化子： 本論理は、名前の生成的インスタンスと特定のインスタンスを区別し、名目定数を通じて名前の扱いを制御するために $\nabla$ 量化子を取り入れている。

2. 基底論理と解釈：
   一貫性を証明するために、著者らはすべての公式が接地（ground）である（固有変数が存在しない）バージョンの論理 $\mathcal{LD}\mu\nabla_\infty$ を構築する。

• 接地補題（Grounding Lemma）： 重要な技術的ステップは、$\mathcal{LD}\mu\nabla$ における任意の導出が、接地代入を介して $\mathcal{LD}\mu\nabla_\infty$ における導出として解釈できることを証明することである。これにより、フル論理の一貫性の問題を、基底論理の一貫性の問題へと還元できる。
• 無限規則： $\mathcal{LD}\mu\nabla_\infty$ において、標準的な $\forall R$ および $\exists L$ ルールは、すべての接地項に対して量化を行う無限規則に置き換えられ、帰納のための $\mu L$ ルールも同様にすべての接地インスタンスをカバーするように拡張される。

3. カット除去（Cut Elimination）：
   一貫性証明の核心は、$\mathcal{LD}\mu\nabla_\infty$ におけるカット規則（具体的にはマルチカット規則）の除去である。

• 簡約関係： 導出に対する簡約関係が定義され、カットをどのように上方へ押し上げたり、あるいは除去したりするかが規定される。
• 還元可能性： McDowellとMillerによって適応されたTait-Martin-Löfの手法に従い、著者らは導出に対する「還元可能性（reducibility）」（および正規化可能性）の概念を定義する。彼らは、$\mathcal{LD}\mu\nabla_\infty$ におけるすべての導出が還元可能であることを証明する。
• 帰納的ケースの扱い： 証明における極めて重要な側面は、弱層化と帰納の相互作用を扱うことである。著者らは、一般的な定義には弱層化が十分であるが、帰納的定義には厳密な層化が必要であることを示す。彼らは、帰納的定義に対して弱層化を許容すると論理的不整合が生じることを示す反例（セクション3.3）を提示している。

主な貢献

• $\mathcal{LD}\mu\nabla$ の定義： 本論文は、弱層化、ナブラ量化、および一般的な帰納的定義を組み合わせた論理を形式的に定義する。
• 一貫性の証明： 主要な貢献は、$\mathcal{LD}\mu\nabla$ が一貫していることの証明である。これは、$\mathcal{LD}\mu\nabla_\infty$ に対するカット除去を証明し、接地解釈を確立することによって達成される。
• 層化の制約： 本研究は、許容される定義と許容されない定義の境界を明確にする。弱層化は一般的な定義（論理関係を可能にする）には十分であるが、帰納的定義は一貫性を保持するために厳密な層化を必要とすることを実証している。
• 反例： 本論文は、帰納的定義に対して層化条件を緩和することが論理的不整合を招くことを示す具体的な反例を提供し、$\mathcal{I}$ に課された制限を正当化している。

結果

• 一貫性： $\mathcal{LD}\mu\nabla$ は一貫していることが証明されている。その結果、$\mathcal{LD}\mu\nabla_\infty$ はすべての証明可能なシーケントに対してカットフリーの導出を許容する。
• 反転特性（Inversion Properties）： 本論文は、$\mathcal{LD}\mu\nabla_\infty$ に関する様々な導入ルールの可逆性（例：$\wedge R, \vee L, \nabla R$）および、コンテキストが空である場合の $\vee R, \exists R$, および定義ルール（$\Delta R$）の特定の部分的な可逆性を確立している。これらの特性は証明探索手順にとって極めて重要である。
• 限界： カット除去定理は、基底論理 $\mathcal{LD}\mu\nabla_\infty$ に対してのみ確立されている。論文では、この結果を固有変数を持つフル論理 $\mathcal{LD}\mu\nabla$ へと拡張することは依然として未解決の課題であると述べている。

意義
本研究の意義は、Abella証明支援システムの能力を拡張する可能性にある。Abellesは現在、定義を厳密に層化することを制限している論理 $\mathcal{G}$ に基づいている。弱層化された定義の包含を正当化することにより、本研究は、プログラミング言語の意味論的性質（型安全性やコンパイラの正当性など）を証明するための基本的な手法である「論理関係」をAbellaがネイティブにサポートするための道を開くものである。

本論文は、この作業を $\mathcal{G}$ のより広範な拡張に向けた基礎的なステップとして位置づけている。現在の結果は、$\nabla$ と帰納を伴う弱層化を扱っているが、著者らは、Abellaのための完全な正当化には、共帰納（co-induction）と名目抽象化（nominal abstraction）を含むさらなる拡張が必要であると指摘している。また、本研究は、帰納的定義に対して厳密な層化を維持する必要性を強調しており、この制約こそが、弱層化を帰納と混合させた際に生じうる不整合を防いでいるのである。