Categorical Models of Amortized Cost: An Adjoint Relationship between Cost and Potential

問題の定義
型システムは、プログラムの計算コスト $\kappa$ を追跡するために開発されており、通常、最悪ケースの保証を提供するためにコスト追跡モナド $M_\kappa \tau$ を使用する。しかし、最悪ケースの分析は、関数型データ構造において償却計算量（amortized complexity）が適切な指標となる場合、しばに不十分である。償却分析はポテンシャルの手法に依存しており、そこでは安価な操作が、後の高価な操作に支払うためのポテンシャル（クレジット）を蓄積する。$\lambda$-amor [Rajani et al. 2021] のようなシステムは、コストとポテンシャルの両方を型システム内で追跡することに成功しているが、一般的な圏論的モデルを欠いている。既存のモデル、例えばオリジナルの $\lambda$-amor の論文におけるステップインデックス付きクリプケ論理関係モデルは、非常に具体的であり、他の言語機能（再帰、確率的効果など）との合成が困難である。コストとポテンシャルの構造的な関係を説明し、償却分析を他の計算効果と組み合わせることを容易にする、抽象的で合成可能な圏論的フレームワークが必要とされている。

手法
著者らは、コストとポテンシャルを含む型理論の表示モデルに必要な抽象的な数学的性質を特定することによって、この問題に取り組む。

1. コスト領域の一般化： 本論文は、コスト領域を正の実数 ($\mathbb{R}^+$) から任意の順序可換モノイド $\mathcal{C}$ へと一般化する。
2. 計算の洗練： 著者らは、$\lambda$-amor から派生した洗練された計算体系 $\lambda$-amor Core を導入する。このコアは複雑な release プリミティブを取り除き、代わりに 3 つのよりプリミティブな構成要素、すなわち pay（ポテンシャルを用いてコストを支払う）、plet（ポテンシャルの関手的な作用）、および split（コストの分割）に置き換えている。この分解は、基礎となる圏論的構造と構文を一致させる必要性に基づいている。
3. 圏論的モデリング： 著者らは、コストとポテンシャルが随伴関係によってモデル化される必要があると提案する。具体的には：
   • コストは、強（strong）次数付きモナド $M$（コストをシーケンシングするため）であり、同時に強次数付きコモナド（コストを分割するため）である。
   • ポテンシャルは、強次数付き関手 $P$ によってモデル化される。
   • 相互作用： すべてのコスト次数 $p$ に対して、随伴 $P_p \dashv M_p$ が存在する。この随伴の単元（unit）はポテンシャルの蓄積（store）に対応し、余単元（counit）はポテンシャルを用いてコストを支払うこと（pay/release）に対応する。
4. 定式化： 著者らは、型システムおよびモデルの法則の検証を Lean 証明助手を用いて機械化している。

主要な貢献
本論文は、主に 3 つの貢献を行う。

1. 抽象的な随伴モデル： 著者らは、コストとポテンシャルが、強次数付きモナド（コストをモデル化する）と強次数付き関手（ポテンシャルをモデル化する）の間の一族の随伴によって関連付けられている、一般的な抽象モデルを記述する。彼らは、このモデルが $\lambda$-amor Core の等式理論に対して健全であることを証明する。
2. 機械化とクリプケのインスタンス： 著者らは Lean における型システムの機械化を提供し、オリジナルの $\lambda$-amor [Rajani et al. 2021] のクリプケ論理関係モデルが、彼らの一般的な圏論的モデルの特定のインスタンスであることを検証する。この接続は以前は観察されておらず、これを証明するには非自明な技術的詳細を要した。
3. 新しいコプレシェーフ・モデル： 著者らは、コストのモノイダル圏上のコプレシェーフに基づく新しいモデルのインスタンスを提示する。このモデルでは、ペアと関数はデイ（Day）畳み込みとその右随伴を用いてモデル化される。これは、特にコスト次数付きモナドをどのように解釈するかにおいて、Kripke モデルとは異なる、償却コストモデルのための標準的な構成を提供する。

結果

• 健全性： 本論文は、$\lambda$-amor Core におけるすべての型推論が、提案された随伴モデルにおいて解釈可能であることを証明する。
• 等価性： クリプケ論理関係モデルは一般的な圏論的モデルの法則を満たすことが示され、この抽象構造が元のシステムの具体的な意味論を捉えていることが確認された。
• 分解： 本論文は、オリジナルの $\lambda$-amor における release 操作が pay、plet、および split に分解可能であること、およびこれらのプリミティブが release から再構成可能であることを示している。
• モデルの比較： コプレシェーフ・モデルは、ポテンシャル型については Kripke モデルと一致するが、コスト次数付きモナドに対しては異なる解釈を提供し、Kripke モデルで使用される明示的な強制関係（forcing relation）を回避している。

意義
本論文は、型理論における償却コスト分析を理解するための、欠けていた「合成的」なピースを提供すると主張している。コストとポテンシャルが随伴を介して関連していることを確立することで、著者らは、具体的なアドホックなモデルを超えて、償却分析がどのように機能するかについての構造的な説明を提供している。このフレームワークにより、償却コストの追跡を、他の決定論的または確率的な効果と合成的な方法で組み合わせることが可能になる。さらに、圏論的な洞察によって駆動された $\lambda$-amor Core への構文の洗練は、等式理論を簡素化し、コストとポテンシャルの相互作用を明確にしている。著者らは、本研究を、より表現力豊かな定量的解析のための型理論の構築や、償却コストモデルを他の計算の圏論的モデルと統合するための基礎として位置づけている。