Pi-演算中的匹配（技术报告）

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