π-演算中的互模拟等价 我们先从π-演算的基本概念讲起。π-演算是一种用于描述并发和移动系统的进程演算。其核心特点是通信通道本身可以作为消息进行传递，这使得系统拓扑结构可以动态改变。一个进程通过通道与其他进程通信，通道名是首要的实体。 在π-演算中，进程的行为由一系列动作构成，例如： 发送动作： x̄〈y〉.P 表示沿通道 x 输出名字 y ，然后继续执行进程 P 。 接收动作： x(z).P 表示从通道 x 接收一个名字，并将其绑定到变量 z ，然后在 P 中使用 z 。 并行组合： P | Q 表示进程 P 和 Q 并行执行。 通道限制： (νx)P 表示创建一个新的私有通道 x ，其作用域限于进程 P 。 现在，我们引入行为等式的概念。我们如何判断两个进程在行为上是不可区分的？一种强有力的方法是 互模拟 。互模拟是一个二元关系 R ，它关联着两个进程。如果 (P, Q) 在 R 中，那么： 每当 P 能执行一个动作（如通信）变为 P‘ 时， Q 也必须能执行一个“匹配”的动作变为 Q’ ，并且 (P‘, Q’) 仍然在 R 中。 反过来， Q 的任何动作也必须能被 P 匹配。 如果存在这样的互模拟关系 R 包含 (P, Q) ，我们就称 P 和 Q 是 互模拟等价的 。 π-演算中的互模拟需要处理名字的传递和限制，这带来了复杂性。最基本的形式是 早期互模拟 。在早期互模拟中，当比较输入动作时，例如 P = x(z).P‘ 和 Q = x(z).Q’ ，要求对于 所有 可能接收到的名字 w （即使是未来才创建的名字）， P‘[w/z] 和 Q’[w/z] 都必须是互模拟的。这是一种“早”的、全面的测试。 与早期互模拟相对的是 晚期互模拟 。在晚期互模拟中，当比较输入动作时，只要求存在一个互模拟关系，使得在接收到 某个具体 名字 w 之后， P‘[w/z] 和 Q’[w/z] 在该关系下。测试被推迟到名字实际接收之后。 早期和晚期互模拟在定义上有所不同，但一个关键的理论结果是，在π-演算中， 早期互模拟等价和晚期互模拟等价是重合的 。也就是说，尽管定义策略不同，但它们最终区分进程的能力是一样的。 为了得到一个更鲁棒、更符合数学直觉的等价关系，我们引入 强弱互模拟 的区分。上述的互模拟要求严格匹配每一个动作（包括内部通信 τ ），这被称为 强互模拟等价 。然而，内部通信通常是不可观察的。如果我们允许忽略这些内部步骤，就得到了 弱互模拟等价 。 弱互模拟将一系列内部通信 τ 视为一个（可能为空的）序列。它只要求匹配可观察的动作（即输入和输出）。弱互模拟等价是π-演算中更常用的行为等价概念，因为它抽象了内部实现细节。 π-演算互模拟等价的顶峰是 同义互模拟 。为了确保等价关系在代换下保持稳定（即如果 P 和 Q 等价，那么对任何名字代换 σ ， Pσ 和 Qσ 也应等价），我们需要对互模拟关系施加额外的条件。一个关系 R 是同义的，如果每当 (P, Q) 在 R 中，那么对于任何名字代换 σ ， (Pσ, Qσ) 也在 R 的闭包中。 同义互模拟等价 就是被包含在某个同义互模拟关系中的等价。它是π-演算中标准且极其重要的行为等价形式。