concurrency - 在巴科斯-瑙尔形式中，定义符号时逗号“，”是什么意思

Question

我对 Pi-Calculus 的了解与对 Backus Naur Form 的了解一样多。这是 Pi Calculus 的核心 BNF 之一（在 Peter Sewell 的“Applied Pi - A Brief Tutorial”中找到）

P,Q ::= 0                        nil
        P | Q                    parallel composition of P and Q
        ~cv                      output v on channel c
        cw.P                     input from channel c
        new c in P               new channel name creation

事实上，我专注于学习 Pi 微积分。但我确实想知道 BNF 定义中 P,Q ::= 的含义。

我会理解 P ::= 意味着 Pi 演算的过程 P 是这个或这个或这个。但是 P,Q ::= 代表什么？

Answer 1

在这里，这意味着字母P和Q都用于表示进程。例如，在 中P | Q，P是一个过程，Q是一个过程。作者本可以写

P ::= 0
      P1 | P2
      ~cv
      cw.P
      new c in P

但更喜欢允许两个不同的字母指代相同的概念，以使公式更具可读性。

顺便说一下，BNF 中的备选方案通常由竖线分隔；但由于竖线|在 pi-calculus 中具有含义，因此作者不想在 pi-calculus 含义和 BNF 含义中都使用它们。该定义仍应理解为“一个进程要么为 nil，要么为并行组合，要么……”。