Core Concepts
ESCにおける良い戦略を実装する環境ベースの抽象機械を設計し、その実行時間が入力サイズと戦略の長さに線形であることを示す。
Abstract
本論文では、Intuitionistic Multiplicative Exponential Linear Logic (IMELL)の証明項である指数置換計算(ESC)のための新しい抽象機械を提案する。この機械は、Accattoliによって導入された良い戦略を実装し、その実行時間が入力サイズと戦略の長さに線形であることを示す。
具体的には以下の点が明らかにされている:
良い戦略は部分項性質を持ち、ダイアモンド性を持つ。これにより、戦略の長さが良いコストモデルとなる。
提案する抽象機械SEASAMEは、良い戦略を決定的に実装する。SEASAMEの実行時間は入力サイズと戦略の長さに線形である。
SEASAMEの正しさは、非決定的な良い戦略と決定的な機械の関係を抽象的に捉えることで示される。これは、通常の実装定理とは少し異なる。
OCamlによる実装も提供される。
本研究は、線形論理における初めての線形オーバーヘッドの結果であり、複雑性理論などでの応用が期待される。また、抽象機械の設計手法としても興味深い。
Stats
ESCの項の大きさ|t|は、良い戦略によって削除または複製される値vの大きさ|v|を上界する。
良い戦略の実行長さkは、RAMで多項式時間で実装可能である。
Quotes
"Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed with rewriting rules at-a-distance for cut elimination."
"Here, we refine Accattoli's result by introducing an abstract machine for ESC and proving that it implements the good strategy and computes cut-free terms/proofs within a linear overhead."