论文标题
函数的计算半效应和分类胶合的逻辑
Logic of computational semi-effects and categorical gluing for equivariant functors
论文作者
论文摘要
在本文中，我们从逻辑的角度（ActeGory）重新访问了Moggi著名的计算效应计算。我们的发展采取以下步骤。首先，我们对Moggi的计算术语进行了证明理论的重建，并获得具有模态类型$ \ rhd $的类型理论作为改进。通过命题-As类型范式，它的逻辑可以通过Benton的伴随微积分视为LAX逻辑的分解。该演算模型为一种编程语言，一种较弱的效果版本，我们称之为\ emph {emi-effects}。其次，我们使用Actegories和Ebivariant函子提供其语义。与以前的效应和actegories研究相比，我们的方法更为综合，因为模型是由均值函数直接给出的，其中包括弗雷德类别（因此很强的单调）作为一种特殊情况。第三，我们表明，沿均值函数的分类胶合是可能的，并得出了$ \ rhd $ - 模式的逻辑谓词。我们还表明，在自然假设下，这种粘合产生了逻辑谓词，与Katsumata的分类$ \ top \ top \ top $ lifftings衍生出的逻辑谓词相吻合。
In this paper, we revisit Moggi's celebrated calculus of computational effects from the perspective of logic of monoidal action (actegory). Our development takes the following steps. Firstly, we perform proof-theoretic reconstruction of Moggi's computational metalanguage and obtain a type theory with a modal type $\rhd$ as a refinement. Through the proposition-as-type paradigm, its logic can be seen as a decomposition of lax logic via Benton's adjoint calculus. This calculus models as a programming language a weaker version of effects, which we call \emph{semi-effects}. Secondly, we give its semantics using actegories and equivariant functors. Compared to previous studies of effects and actegories, our approach is more general in that models are directly given by equivariant functors, which include Freyd categories (hence strong monads) as a special case. Thirdly, we show that categorical gluing along equivariant functors is possible and derive logical predicates for $\rhd$-modality. We also show that this gluing, under a natural assumption, gives rise to logical predicates that coincide with those derived by Katsumata's categorical $\top\top$-lifting for Moggi's metalanguage.
