Pi-演算中的匹配

我们研究在 Pi-演算中，匹配前缀（一种测试两个名称是否（语法）相等的条件算子）是否可通过其他算子表达。此前，Carbone 和 Maffeis 证明了在相当强的要求（保持和反映可观测性）下，匹配无法以此方式表达。随后，Gorla 提出了一套目前被广泛测试的编码准则，该准则允许更大的自由度（例如，它不要求直接翻译可观测性，而是允许就成功状态的可达性对演算进行比较）。在本文中，我们仅利用 Gorla 的宽松要求，给出了一个关于匹配不可表达性的显著更强的分离结果。