computer-science - 在 Milner 的 Pi 演算中，当多个进程从同一个通道读取时，评估语义是什么？

Question

在 Milner 的 Pi 演算中，当多个进程从同一个通道读取时，评估语义是什么？

规则说

!x(a). P | ?x(b) Q ~> P | Q[a/b]

但是像这样的情况呢

!x(a). P | ?x(b) Q | ?x(c) R

?

Answer 1

我知道这个问题有点老了，但为了下一个人来寻找答案，我会尝试一个。

答案是：它是不确定的。Pi演算过程：

?x(b).Q | ?x(c).R

说“要么接受 x 上的输入然后作为 Q 继续，要么接受 x 上的输入并作为 R 继续”。两种执行对于这个过程都是有效的。您可以考虑与这些流程相关的标记转换系统 --- 正如您所期望的那样，它将是分支的。

正是这种不确定性使过程演算（如 Pi 演算和朋友）变得“特别”，并且与 lambda 演算之类的东西不同，在 lambda 演算中，你评估事物的顺序并不重要（你会得到相同的结果）。Pi 演算精确地具有所有这些机制，例如双模拟和转换系统语义，因此它可以捕获这些情况并使其易于分析。