论文标题
计算中央次级和概念：健全性，完整性和内部语言
Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages
论文作者
论文摘要
类别理论中的单元是代数结构，可用于模拟编程语言中的计算效应。我们展示了“中心”和更普遍的“中心性”的概念，即可能与所有其他效果通勤的属性，可以用于对对称单体类别作用的强元。我们确定了三个等效的条件，这些条件表征了强大的单子中心的存在（其中一些将其与胸前的权力和鲁滨逊中心相关），我们表明，许多众所周知的自然发生类别上的每个强大的单调都可以接受一个中心，从而表明这个新的noteion是普遍的。更普遍地，我们研究了中央亚膨胀，这必然是可交换的，就像强大的单子中心一样。我们通过制定配备了中央次层的Lambda calculi的方程理论来提供计算解释，我们描述了这些理论的分类模型，并证明了我们语义学的健全性，完整性和内部语言结果。
Monads in category theory are algebraic structures that can be used to model computational effects in programming languages. We show how the notion of "centre", and more generally "centrality", i.e. the property for an effect to commute with all other effects, may be formulated for strong monads acting on symmetric monoidal categories. We identify three equivalent conditions which characterise the existence of the centre of a strong monad (some of which relate it to the premonoidal centre of Power and Robinson) and we show that every strong monad on many well-known naturally occurring categories does admit a centre, thereby showing that this new notion is ubiquitous. More generally, we study central submonads, which are necessarily commutative, just like the centre of a strong monad. We provide a computational interpretation by formulating equational theories of lambda calculi equipped with central submonads, we describe categorical models for these theories and prove soundness, completeness and internal language results for our semantics.
