一句话:提出一个范畴框架,模块化地刻画带操作的幺半群的理论与模型,统一代数操作与作用域/绑定操作。
论文研究带操作的幺半群的等式理论与模型,旨在统一处理代数操作以及带作用域和变量绑定的操作,并支持理论与模型的模块化组合。受代数效应和“计算即幺半群”启发,作者建立范畴框架,证明代数操作的理论范畴与幺半群范畴等价,并表明更复杂的操作可核心反射为代数操作且保持初始代数。在模型侧,提出 modular models,使其可在存在其他操作时解释抽象语法,并给出由 monoid transformer、自由代数、复合以及对称幺半范畴构造模块化模型的方法。
Inspired by algebraic effects and the principle of notions of computations as monoids, we study a categorical framework for equational theories and models of monoids equipped with operations. The framework covers not only algebraic operations but also scoped and variable-binding operations. Appealingly, in this framework both theories and models can be modularly composed. Technically, a general monoid-theory correspondence is shown, saying that the category of theories of algebraic operations is equivalent to the category of monoids. Moreover, more complex forms of operations can be coreflected into algebraic operations, in a way that preserves initial algebras. On models, we introduce modular models of a theory, which can interpret abstract syntax in the presence of other operations. We show constructions of modular models (i) from monoid transformers, (ii) from free algebras, (iii) by composition, and (iv) in symmetric monoidal categories.