Dans la forme de Backus-Naur, que veut dire une virgule ',' en définissant un symbole?

Question

Je suis autant novice à Pi-Calculus que je le suis avec Backus Naur Form. Voici un des BNF base pour Pi calcul (dans « Applied Pi - Un bref tutoriel » par 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 

En acte, je suis concentré sur l'apprentissage Pi Calcul. Mais je m'interroge sur la signification de P, Q :: = dans la définition de la BNF.

Je comprendrais que P :: = ce qui signifie qu'un processus P du calcul de Pi est ceci ou ceci ou ceci. Mais qu'est-ce que P, Q :: =?

Answer 1

Ici, cela signifie que les lettres P et Q sont toutes deux utilisées pour désigner des processus. Par exemple, dans P | Q, P est un processus et Q est un processus. L'auteur aurait pu écrire

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

mais préféré pour permettre à deux lettres distinctes de se référer au même concept pour faire des formules un peu plus lisible. Par ailleurs, classiquement les alternatives dans BNF sont séparées par une barre verticale; mais puisque la barre verticale | a une signification en pi-calcul, l'auteur n'a pas voulu les utiliser à la fois dans leur signification de pi-calcul et dans leur signification BNF. La définition devrait toujours être lue comme "un processus est soit nul, soit une composition parallèle, ou ...".