打破对称性

Palamidessi 的一个著名结果表明，πmix（带混合选择的 π-演算）比 πsep（其仅含分离选择的子集）更具表达力。该结果的证明依据了它们在对称网络中关于领导者选举的不同表达力。后来，Gorla 提出了一个可以说更简单的证明，该证明没有采用对称网络中的领导者选举，而是利用了“乱伦”过程（包含同一信道上既允许发送者又允许接收者的混合选择）在并行运行两个副本时的可归约性。在这两个证明中，打破（初始）对称性的作用或多或少是明显的。在本文中，我们通过基于对“打破对称性”含义的恰当形式化来重新证明上述结果，从而更清晰地阐明这一作用，且无需参考领导者选举这一不同的问题域层次。Palamidessi 和 Gorla 都将他们的结果表述为：不存在从 πmix 到 πsep 的、统一且合理的编码。我们指出了如何调整各自的证明，并展示了不同的一致性和合理性概念所带来的后果。在每种情况下，打破初始对称性的能力都被证明是至关重要的。