论文标题
状态结构操作语义
Stateful Structural Operational Semantics
论文作者
论文摘要
语法语义的组成性是编程语义中的重要问题。在Turi和Plotkin的意义上，数学操作语义可以保证组成性，但是从状态计算的角度看，它仅适用于非常细粒度的等效性，这些等效基本上假设了任何两个陈述之间的环境的无限制干扰。我们介绍了更严格的状态SOS规则格式的状态语言。我们表明，通过假设仅读取的干扰或步骤之间没有干扰给出的两个更粗粒语义的组成性，即使对于状态SOS，也是不可决定的。但是，我们以凉爽的GSOS格式和Van Glabbeek启发的方式进一步限制了规则格式，我们获得了简化且凉爽的状态SOS格式，该格式分别保证了两个更抽象的等价的组成性。
Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences.
