AI 中文总结
该研究以 $\lambda$-amor 系统为基础，明确代价与潜能类型理论指称模型的抽象属性，提出代价与潜能为分级函子伴随对的方案，并给出三个具体模型实例。
AI 中文摘要
已有多种类型系统被开发，用于使用代价跟踪单子 $M\\ \kappa\\ \tau$ 跟踪计算的代价 $\kappa$，但这仅能跟踪计算的最坏情况代价。若要跟踪摊销代价，可添加类型 $[\kappa]\tau$，其存储具有类型 $\tau$ 的潜能 $\kappa$，并配套存储与释放潜能的操作。本研究基于此类系统之一的 $\lambda$-amor：$\lambda$-amor 可在类型系统中跟踪代价与潜能，涵盖基于效应和协效应的系统、按值调用及按名调用的语言。本文明确了代价与潜能类型理论的指称模型必须满足的抽象属性：代价与潜能需由分级函子的伴随对建模，其中建模代价的函子同时构成分级单子与兼容的分级余单子。本文给出该通用抽象方案的三个具体实例：（1）忽略类型系统所跟踪代价的简单集合论模型；（2）原始 $\lambda$-amor 论文中的克里普克逻辑关系模型（本文证明其可转化为伴随模型的实例）；（3）基于代价的幺半范畴上的余预层的新模型，其中通过 Day 卷积及其右伴随对建模积与函数。
英文摘要
Various type systems have been developed to track the cost $κ$ of a computation using a cost-tracking monad $M\ κτ$. On its own, this only tracks the worst-case cost of a computation. If we also want to track amortized cost, then we can add a type $[κ]τ$ which stores potential $κ$ with a type $τ$, together with operations for storing and releasing potential. In this work, we build on one such system, $λ$-amor: $λ$-amor allows to track cost and potential in the type system and subsumes effect and coeffect-based systems, call-by-value and call-by-name based languages. In this paper, we identify the abstract properties that denotational models of type theories for cost and potential have to satisfy: Cost and potential must be modelled by an adjoint pair of graded functors, where the functor modelling cost forms both a graded monad and a compatible graded comonad. We present three concrete instances of this general abstract scheme: (1) A simple set-theoretic model that ignores the cost tracked by the type system, (2) the Kripke logical relations model in the original $λ$-amor paper (which we show can be turned into an instance of the adjoint model), and (3) a novel model based on copresheaves on a monoidal category of costs, where we model pairs and functions by Day convolution and its right-adjoint.
Comments25 pages, 5 pages appendix
