In the Backus-Naur Form what does a comma ',' mean while defining a symbol

Question

Hello,

I am as much newbie to Pi-Calculus as I am with Backus Naur Form. Here is one of the core BNF for Pi Calculus ( found in "Applied Pi - A Brief Tutorial" by Peter Sewell)

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

In deed I am focussed on learning Pi Calculus. But I do wonder about the meaning of P,Q ::= in the definition of the BNF.

I would understand P ::= meaning that a process P of Pi calculus is this or this or this. But what P,Q ::= stands for ?

Answer 1

Here, this means that the letters P and Q are both used to denote processes. For example, in P | Q, P is a process and Q is a process. The author could have written

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

but preferred to allow two distinct letters to refer to the same concept in order to make formulas a bit more readable.

By the way, classically the alternatives in BNF are separated by a vertical bar; but since the vertical bar | has a meaning in pi-calculus, the author didn't want to use them both in their pi-calculus meaning and in their BNF meaning. The definition should still be read as “a process is either nil, or a parallel composition, or …”.