Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages
TItouan Carette, Louis Lemonnier and Vladimir Zamdzhiev
分类理论中的Monads是代数结构,可用于在编程语言中建模计算效应。 我们展示了如何“中心”的概念,以及更普遍的“中心性”,即与所有其他效果一起通勤的效果属性,可以制定为对称一氧化二甲类作用的强单体。 我们确定了三个等价的条件,这些条件表征了一个强大的monad中心的存在(其中一些将其与Power和Robinson的premonoidal中心有关),我们表明,许多众所周知的自然发生的类别中的每一个强monad都承认一个中心,从而表明这个新概念无处不在。 更一般地说,我们研究中央子单体,它们必然是交换的,就像强单的中心一样。 我们通过制定配备中央子单体的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 Pow...
