A Proof of Coincidence of Labeled Bisimilarity and Observational Equivalence in Applied Pi Calculus
A Proof of Coincidence of Labeled Bisimilarity and Observational Equivalence in Applied Pi Calculus
复制标题
应用Pi演算中标记双相似性与观察等价性的一致证明
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Jia Liu
中科院分区：
文献类型：
--
作者：
Jia Liu
然而，这个问题可以通过要求仅在基本排序上定义活动替换来解决（参见，例如，[3]）。本文的目的是提供定理的一个证明。在[1]的原始语义中，结构等价的使用引入了许多可能性，并且使得很难写出严格的证明。为了克服这个困难，我们将使用最初在[3]中提出的中间语义作为桥梁。将讨论四个等价物：
However, this problem can be fixed by requiring active substitutions be defined on the base sort only (see, for instance, [3]). The purpose of this note is to supply a proof for the theorem. In the original semantics in [1], the use of structural equivalence introduces many possibilities and makes it difficult to write a rigorous proof. To overcome the difficulty we shall use intermediate semantics, originally proposed in [3], as a bridge. Four equivalences will be discussed: