Modules over relative monads for syntax and semantics
Benedikt Ahrens
备注：
v2: - Abstract and Introduction completely rewritten - Addition of examples and remarks in Secs. 1 and 2 - Sec 3 now describes the implementation in proof assistant Coq of the main theorem v3: - final version for publication in MSCS
We give an algebraic characterization of the syntax and semantics of a class of languages with variable binding.
We introduce a notion of 2-signature: such a signature specifies not only the terms of a language, but also reduction rules on those terms. To any 2-signature $S$ we associate a category of "models" of $S$. This category has an initial object, which integrates the terms freely generated by $S$, and which is equipped with reductions according to the inequations given in $S$. We call this initial object the language generated by $S$. Models of a 2--signature are built from relative monads and modules over such monads. Through the use of monads, the models---and in particular, the initial model---come equipped with a substitution operation that is compatible with reduction in a suitable sense.
The initiality theorem is formalized in the proof assistant Coq, yielding a machinery which, when fed with a 2-signature, provides the associated programming language with reduction relation and certified substitution.
图里和普洛特金的双代数语义是一种抽象的方法来指定一个系统的操作语义，通过它的语法（编码为单子）和它的动态（内函子）之间的分配律。这种设置有助于表明语义规范（余代数）满足期望的性质：特别是，它是合成的。在这项工作中，我们使用双代数方法来推导出字符串图的行为良好的结构性操作语义，这是一种越来越多地用于不同学科交互系统研究的图形语法。我们的分析依赖于代表二维操作的基础上弦图在各种类别作为一个单子，和他们的双代数语义的分配法在单子。作为一个概念的证明，我们提供了一个多功能的字符串图形语言，已被用来模拟信号流图（控制理论）和Petri网（并发理论）的双代数组成语义。此外，我们的方法揭示了两种不同的解释Frobenius方程的字符串图和两个同步机制的过程中，à la Hoare和à la米尔纳之间的对应关系。
我们给出了一类简单类型语言（如PCF语言）的语法和语义的代数刻画：我们刻画了简单类型绑定语法，通过一个普适属性，即作为某个类别的初始对象，配备了归约规则。为了这个目的，我们采用了在以前的两个工作中开发的技术：在[2]中，我们在不同类型集上对语言之间的句法翻译建模，作为一类模型中的初始态射。在[1]中，我们在一类模型中用归约规则刻画了无类型语法作为初始对象。在目前的工作中，我们表明，这些技术是模块化的，足以结合起来：因此，我们的特点是简单类型的语法与减少规则的初始对象在一个类别。泛属性产生了一个操作符，它允许在可能不同的类型集上指定语言之间的翻译-通过构造在语义上忠实。我们通过2-签名来指定一种语言，也就是说，在两个级别上的签名：语法级别指定语言的类型和术语，并将类型与每个术语相关联。语义层通过不等式指定语言术语的归约规则。对于任何给定的2-签名，我们关联一类模型。我们证明了这个范畴有一个初始对象，它集成了由2-签名自由生成的类型和项，以及由给定不等式生成的这些项的约化关系。我们称这个对象为由2-签名生成的（编程）语言。[1]Ahrens，B.：Modules over relative monads for syntax and semantics（2011），arXiv：1107.5252，to be published in Math. Struct. in Comp. Sci…
