比较同步 pi-calculus 与异步 pi-calculus 的表征力度
编程语言
2020-11-17 v1 计算机科学中的逻辑
摘要
异步 pi-calculus 由 Boudol 和独立地由 Honda 与 Tokoro 最近提出，是 pi-calculus 的一个子集，不包含显式的选择和输出前缀运算子。然而，该计算的通信机制足够强大，以至于可以仿真输出前缀，如 Boudol 所示；以及输入护卫选择，如 Nestmann 与 Pierce 最近所证明的。于是，一个自然的问题随之而来：是否可能在其中嵌入完整的 pi-calculus。我们展示这是不可能的，即不存在从 pi-calculus 翻译到异步 pi-calculus 的任何均匀、并行保持的翻译，除非考虑到任何“合理”的等价概念。该结果基于异步 pi-calculus 无法打破初始通信图中可能存在的某些对称性的能力。通过类似的论证，我们证明了 pi-calculus 与 CCS 之间的分离结果。
引用
@article{arxiv.cs/9809008,
title = {Comparing the expressive power of the Synchronous and the Asynchronous pi-calculus},
author = {Catuscia Palamidessi},
journal= {arXiv preprint arXiv:cs/9809008},
year = {2020}
}
备注
10 pages. Proc. of the POPL'97 symposium