Ordered Adjoint Logic (Extended Version)

「順序付き随伴論理」の技術的概要

問題定義
順序付き論理および型システムは、計算言語学からセキュリティプロトコルの強制まで、リソース使用の順序が重要となる多様な応用において不可欠である。ほとんどの定式化において、順序付き型は線形であり、リソースは正確に一度使用されなければならない。Kanovich らの先行研究は、線形順序付き論理内の副指数（subexponentials）を用いてこの制約を緩和する計算論を調査したが、このアプローチはすべての推論が行われる「基本モード」に依存している。順序付き論理において、この基本モードはすべての構造規則（弱め、縮約、交換）を禁止しなければならないため、応用は頻繁にこの制限的なモードを行き来しなければならない。さらに、既存の副指数システムは、片側の構造的特性（例えば、右への移動なしの左への移動）の可能性を十分に探求していない。著者らは、単一の制限的な基本モードに依存することなく、弱め、左/右縮約、左/右移動の独立した制御を含む、多様で微細な構造的特性を持つモードの順序を支援するために、これらの枠組みを一般化することを目的としている。

手法
著者らは、随伴モダリティの構造的柔軟性と順序付き論理の順序制約を組み合わせる「順序付き随伴論理」というシステムを導入する。手法は主に 2 つの段階で進行する。

1. シークエント計算の定式化:
   著者らは、前件がラベル付けされた仮説の順序列であるシークエント計算を定義する。構造規則はグローバルではなく、モードの順序（$k \geq m$）によって管理される。各モード $m$ は、構造的特性の集合 $\sigma(m) \subseteq \{W, C, M_{\leftarrow}, M_{\rightarrow}\}$（弱め、縮約、左移動、右移動）に関連付けられる。

   • シフトモダリティ: 基本モードの代わりに、システムは異なるモード間での推論を切り替えるシフトモダリティ（$\downarrow^k_m$ および $\uparrow^m_l$）を使用する。これらのシフトは Benton の随伴論理から導出されたものであるが、順序付き文脈を処理するように一般化されている。
   • 構造規則: 著者らは、移動と縮約を片側の変種に分解する。移動規則は、命題のモードが対応する方向の移動を認める場合、単一の命題が前件シーケント内で任意に左または右へ移動することを許可する。縮約は、標準的な線形論理の局所的縮約とは異なり、切断除去を確保するために非局所的（隣接しない重複の結合）に許可される。
   • 論理結合子: 言語には、順序付き含意（$\multimap$ および $\multimap$）、融合およびねじれた論理積、およびシフトが含まれる。規則はモードに対してパラメトリックであり、結論から前提へ規則を読み取る際にモードの独立性の保存を確保する特定の条件（例えば、$k \geq m \geq r$）を有する。

2. 自然演繹と決定可能性:
   著者らは、構造的規則が暗黙的であり、プログラミング言語に適した基盤となることを目指して、自然演繹の定式化に移行する。

   • 明示的対暗黙的: 当初、シークエント計算とのギャップを埋めるために、明示的な構造規則を持つシステムを提示する。その後、構造的規則（弱め、縮約、移動）が暗黙的であるシステムを定義する。
   • 証明検査のアルゴリズム: 暗黙的な構造規則（特に弱めの無制限の適用と、除去規則における変数の配置）によって導入される非決定性に対処するため、著者らは「正規形」判定（$\Omega \gg_{\Gamma, r} \Omega_{nf}$）を定義する。このアルゴリズムは、与えられた文脈 $\Omega$、仮説集合 $\Gamma$、およびモード $r$ に対して、すべての可能な正規形（重複変数を持たない文脈）の集合を計算する。
   • 集合ベースの判定: 自然演繹規則は、正規形文脈の集合（$\Xi$）上で動作するように引き上げられる。例えば、論理積の導入は文脈集合のデカルト積を計算し、交差は（加法的論理積のような）文脈の一致を必要とする規則に使用される。

主要な貢献

• 一般化された随伴論理: 本論文は、各モードが弱め、縮約、片側移動を独立に制御するモードの順序を導入することで、順序付き設定に随伴論理を一般化する。
• 片側の構造的特性: システムは、左移動と右移動、および縮約を独立した構造的特性として明示的にモデル化し、証明する。これは先行する副指数の研究で予期されていたが、探求されていなかった特徴である。
• 切断除去: 著者らは、順序付き随伴シークエント計算が（マルチカットを介して）切断除去および恒等式除去を許容することを証明し、システムを適切に振る舞う論理的枠組みとして確立する。
• 証明検査の決定可能性: 本論文は、暗黙的な構造規則を持つ自然演繹システムを提供し、このシステムの証明検査が決定可能であることを証明する。これは、正規形文脈の集合を計算する終了するアルゴリズムを構築することによって達成される。

結果

• 理論的健全性: シークエント計算は切断および恒等式除去を満たすことが示される。自然演繹システムは、シークエント計算に対して健全かつ完全であることが証明される。
• 決定可能性: 正規形を計算するアルゴリズム（$NF_{\Gamma, r}(\Omega)$）は終了することが証明される。したがって、暗黙的自然演繹システムにおける証明の検査問題は決定可能である。
• 部分構造包含: この結果は、部分構造包含の決定可能性を意味する。これは、明示的な世界を持つクリプキ意味論を使用する言語（QRTT など）の型検査アルゴリズムの中核的な構成要素である。

意義と主張
著者らは、順序付き随伴論理が、表現力豊かな随伴プログラミング言語または論理的枠組みに適した基盤を提供すると主張する。構造的特性を単一の基本モードから切り離し、随伴シフトを使用することで、システムは、線形、順序付き、無制限など、さまざまな分野でのネイティブ推論を、シームレスな切り替えを伴って可能にする。暗黙的な構造規則を伴う証明検査の決定可能性は、微細な構造的特性を持つコードを処理できる関数型プログラミング言語向けの双方向型チェッカーの実装に向けた重要なステップとして強調されている。本論文は、決定手続きが確立されている一方で、実用的な効率性（例えば、不要な弱めによる指数関数的複雑さを回避すること）は将来の最適化の課題であると指摘している。この研究は、Kanovich らの副指数順序付き論理の直接的な一般化であり、Jang らの随伴型に順序を含めるための拡張として位置づけられている。