Translational Expressiveness. Comparing Process Calculi using Encodings
Translational Expressiveness. Comparing Process Calculi using Encodings
复制标题
翻译表达力。
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Kirstin Peters
中科院分区：
文献类型：
--
作者：
Kirstin Peters
没有业务上通信，离子就没有多大用处。由于选择这两个等价的可能性不同，通常不可能比较不同的完全抽象结果，这是该标准的主要缺点。3.2.3.操作通信直觉上，操作通信需要保存和反映执行。再次，它由一个完整性和健全性的一部分.完备性条件，也称为充分性，要求对于所有源项步骤S 7−→S S′或源项执行S Z=<$S S′，有一个目标语言的模拟执行使得J S K Z =<$T T J S′ K，其中T <$PT × PT是目标语言的一些等价。请注意，在考虑单个源项步骤或源项执行方面没有区别。直观地说，完整性条件要求任何源项执行都是由目标项模某个等价T来模拟的。同样，完整性通常是最简单的部分。对于可靠性条件，我们基本上找到两个公式。更严格的公式要求，对于目标J S K Z = T T的所有执行，存在源S Z= S S′的一些执行，使得J S′ K T T。直观地说，可靠性要求J S K所能做的任何事情都是S模T [FL 10]的某些行为的翻译。较弱的公式要求对于目标J S K Z = T T的所有执行，存在源S Z= S S′的一些执行和目标T Z= T T ′的一些执行，使得J S′ K T T ′。直观地说，它声明目标的任何执行都是对源模T [Par 08，Gor 10 b]中执行的模拟的一部分。主要区别在于，后面的表述允许中间或部分承诺状态，即，对于不需要与相应源项的状态直接相关但必须属于源项步骤的某种仿真的状态。在这个意义上，中间状态是由源项步骤的部分仿真产生的。我们将在第6.3.1节讨论这个问题。同样，操作对应的不同变体可能源于对目标语言的假设等价T的不同要求。注意，[Nes 96，NP 00]表示没有等价性的操作对应，即，当S 7−→S S′时，要求J S K Z=<$T J S′ K，且J S K Z =<$T T意味着对于某些S′，S Z=<$S S S′，使得T Z=<$T J S′ K，这再次导致比上面更严格的公式。他们还提出了可靠性部分的一个更严格的变体-J S K 7−→T T蕴涵S 7−→S S S′，对于某些S′使得T T J S′ K-，并指出只有提示编码才能满足这个更严格的变体。此外，在[FL 10]中，在假设存在从源术语的标签到目标术语的标签的映射·k的情况下，考虑标记的步骤而不是约简语义。因此，所得到的要求--当S λ =<$S′且J S K λ =<$T时，J S K λ <$=<$T J S′ K--意味着对于某些λ′，S′，S ′，S′，使得J S′ K T T且λ <$′ = λ-，可以被认为比上述运算对应的变体更严格，因为在某种意义上也必须保持和反映可观测量。事实上，如果不加强标记语义，
ion is not of much use without operational correspondence. Because of the various possibilities two choose these two equivalences, it is often not possible to compare different full abstraction results, which is a major drawback of this criterion. 3.2.3. Operational Correspondence Intuitively, operational correspondence requires preservation and reflection of executions. Again, it consists of a completeness a soundness part. The completeness condition, also called adequacy, requires that for all source term steps S 7−→S S′ or source term executions S Z=⇒S S′ there is one emulating execution in the target language such that J S K Z =⇒T T J S′ K, where T ⊆ PT × PT is some equivalences on the target language. Note that there is no difference in the consideration of single source term steps or source term executions. Intuitively, the completeness condition requires that any source term execution is emulated by the target term modulo some equivalence T . Again, completeness is usually the easiest part. For the soundness condition we basically find two formulations. The stricter formulation requires that for all executions of the target J S K Z =⇒T T there exists some execution of the source S Z=⇒S S′ such that J S′ K T T . Intuitively, soundness requires that whatever J S K can do is a translation of some behaviour of S modulo T [FL10]. The weaker formulation requires that for all executions of the target J S K Z =⇒T T there exists some execution of the source S Z=⇒S S′ and some execution of the target T Z=⇒T T ′ such that J S′ K T T ′. Intuitively, it states that any execution of the target is some part of the emulation of an execution in the source modulo T [Par08, Gor10b]. The main difference is that the later formulation allows for intermediate or partial commitment states, i.e., for states that do not need to be related directly to the states of the respective source term but that have to belong to some emulation of a source term step. In this sense, an intermediate state results from the partial emulation of a source term step. We discuss this issue in Section 6.3.1. Again different variants of operational correspondence may arise from different requirements on the assumed equivalence T on the target language. Note that [Nes96, NP00] present operational correspondence without the equivalence, i.e., require J S K Z=⇒T J S′ K whenever S 7−→S S′ and J S K Z =⇒T T implies S Z=⇒S S′ for some S′ such that T Z=⇒T J S′ K, which again leads to a stricter formulation than above. They also present a stricter variant of the soundness part—J S K 7−→T T implies S 7−→S S′ for some S′ such that T T J S′ K—and state that only prompt encodings can satisfy this stricter variant. Moreover, in [FL10] labelled steps are considered instead of a reduction semantics under the assumption that there exists a mapping ·̂ from the labels of the source term into the labels of the target term. Hence, the resulting requirement—J S K λ̂ =⇒ T J S′ K whenever S λ =⇒ S′ and J S K λ =⇒ T implies S λ ′ =⇒ S′ for some λ′, S′ such that J S′ K T T and λ̂′ = λ—can be considered as stricter than the above variant of operational correspondence, because also observables have to be preserved and reflected in some sense. In fact, without this strengthening to labelled semantics, operational correspondence