论过渡制度规范的含义
On the Meaning of Transition System Specifications
摘要：
转换系统规范为编程和规约语言提供了语义。它们提供了一个封闭术语作为过程图的含义：一个标记转换系统中的状态。与此同时，它们提供了一个n元运算符的含义，或者更一般地说，一个具有n个自由变量的开放项，作为过程图上的n元运算。这样做的经典方法，闭项语义学，将开放项的含义简化为其闭实例的含义。它使运算符的含义依赖于它所使用的上下文。在这里，我提出了一个替代的过程图语义的TSS，不受这个缺点。流程图上的语义等价可以被提升，以使开放项符合封闭项或流程图语义。对于纯TSS，后者更具鉴别力。我认为五个健全的要求配备了递归结构的编程和规约语言的语义：组合性，适用于n元运算符，递归和变量，不变性下$α$ -转换，递归定义原则，说递归调用的意义应该是相应的递归方程的解决方案。我建立了四个这些要求下的TSS的闭项语义的满意度意味着他们的满意度下的过程图语义。
英文摘要：
Transition System Specifications provide programming and specification languages with a semantics. They provide the meaning of a closed term as a process graph: a state in a labelled transition system. At the same time they provide the meaning of an n-ary operator, or more generally an open term with n free variables, as an n-ary operation on process graphs. The classical way of doing this, the closed-term semantics, reduces the meaning of an open term to the meaning of its closed instantiations. It makes the meaning of an operator dependent on the context in which it is employed. Here I propose an alternative process graph semantics of TSSs that does not suffer from this drawback. Semantic equivalences on process graphs can be lifted to open terms conform either the closed-term or the process graph semantics. For pure TSSs the latter is more discriminating. I consider five sanity requirements on the semantics of programming and specification languages equipped with a recursion construct: compositionality, applied to n-ary operators, recursion and variables, invariance under $α$-conversion, and the recursive definition principle, saying that the meaning of a recursive call should be a solution of the corresponding recursion equations. I establish that the satisfaction of four of these requirements under the closed-term semantics of a TSS implies their satisfaction under the process graph semantics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
