在巴科斯-诺尔范式中，逗号 ',' 的作用是什么？定义符号时的意思

Question

我对 Pi 微积分和巴科斯诺尔范数都是新手。 这是 Pi 微积分的核心 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 演算中具有含义，因此作者不想同时使用它们的 pi 演算含义和 BNF 含义。该定义仍应解读为“进程要么为零，要么并行组合，要么……”。