打破对称性

Palamidessi的一个著名结果表明，\pimix（具有混合选择的\pi-演算）比\pisep（其仅具有分离选择的子集）更具表达能力。该结果的证明基于它们在对称网络中领导者选举问题上的不同表达能力。后来，Gorla提供了一个可以说更简单的证明，该证明不依赖于对称网络中的领导者选举，而是利用了乱伦过程（包含同一通道上已启用的发送者和接收者的混合选择）在并行运行两个副本时的可归约性。在这两个证明中，打破（初始）对称性的作用或多或少是明显的。在本文中，我们通过重新证明上述结果来进一步阐明这一作用——该证明基于对打破对称性含义的适当形式化，而不涉及领导者选举这一区分问题领域的另一层次。Palamidessi和Gorla都通过陈述不存在从\pimix到\pisep的均匀且合理的编码来重新表述他们的结果。我们指出了如何调整各自的证明，并展示了均匀性和合理性概念变化所带来的后果。在每种情况下，打破初始对称性的能力都被证明是至关重要的。