Modular Bisimulation Theory for Computations and Values
Modular Bisimulation Theory for Computations and Values
复制标题
用于计算和值的模块化互模拟理论
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Peter D. Mosses
中科院分区：
文献类型：
--
作者：
Martin Churchill;Peter D. Mosses
对于进程代数的结构操作语义（SOS），互模拟的各种概念已经被研究，以及确保双相似性是一个同余的规则格式。然而，对于编程语言，SOS通常涉及辅助实体（例如存储）和计算值，并且标准互模拟和规则格式不直接适用。
在这里，我们首先介绍一个概念的互模拟计算和值之间的区别的基础上，相应的自由同余格式。然后，我们提供了一个模块化的SOS（MSOS）的变体，它提供了一个系统的辅助实体治疗的元理论。这是基于高阶形式的互模拟，我们制定了一个适当的同余格式。最后，我们将展示如何代数法可以证明声音互模拟仅参考（M）SOS规则定义的编程结构中涉及的。这样的规律对于涉及进一步结构的语言来说仍然是合理的。
For structural operational semantics (SOS) of process algebras, various notions of bisimulation have been studied, together with rule formats ensuring that bisimilarity is a congruence. For programming languages, however, SOS generally involves auxiliary entities (e.g. stores) and computed values, and the standard bisimulation and rule formats are not directly applicable.
Here, we first introduce a notion of bisimulation based on the distinction between computations and values, with a corresponding liberal congruence format. We then provide metatheory for a modular variant of SOS (MSOS) which provides a systematic treatment of auxiliary entities. This is based on a higher order form of bisimulation, and we formulate an appropriate congruence format. Finally, we show how algebraic laws can be proved sound for bisimulation with reference only to the (M)SOS rules defining the programming constructs involved in them. Such laws remain sound for languages that involve further constructs.