我们给出了一类简单类型语言（如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. Science [2] Ahrens，B.：类型化抽象类的扩展初始化。Logical Methods in计算机科学8（2），1-35（2012）
英文摘要：
We give an algebraic characterization of the syntax and semantics of a class of simply-typed languages, such as the language PCF: we characterize simply-typed binding syntax equipped with reduction rules via a universal property, namely as the initial object of some category. For this purpose, we employ techniques developed in two previous works: in [2], we model syntactic translations between languages over different sets of types as initial morphisms in a category of models. In [1], we characterize untyped syntax with reduction rules as initial object in a category of models. In the present work, we show that those techniques are modular enough to be combined: we thus characterize simply-typed syntax with reduction rules as initial object in a category. The universal property yields an operator which allows to specify translations - that are semantically faithful by construction - between languages over possibly different sets of types.
We specify a language by a 2-signature, that is, a signature on two levels: the syntactic level specifies the types and terms of the language, and associates a type to each term. The semantic level specifies, through inequations, reduction rules on the terms of the language. To any given 2-signature we associate a category of models. We prove that this category has an initial object, which integrates the types and terms freely generated by the 2-signature, and the reduction relation on those terms generated by the given inequations. We call this object the (programming) language generated by the 2-signature.
[1] Ahrens, B.: Modules over relative monads for syntax and semantics (2011), arXiv:1107.5252, to be published in Math. Struct. in Comp. Science
[2] Ahrens, B.: Extended Initiality for Typed Abstract Syntax. Logical Methods in Computer Science 8(2), 1-35 (2012)
咖喱风格的系统F，即。从程序设计语言的角度来看，系统F没有显式的类型，可以被看作是多态性的核心表示。本文利用一个博弈模型，从语法和博弈语义域两方面给出了该语言类型同构的一个刻画。该模型包括：一个非类型化部分解释术语，一个博弈概念解释类型，一个类型化部分表示一个非类型化策略在一个博弈中起作用的事实。通过分析模型中的同构，我们证明了Curry型系统F的型同构所对应的方程组是Church型同构方程组的推广，并给出了一个新的非平凡方程：对于所有X. A = A[对于所有Y.Y/X]，如果X只在A中出现.
