What bar should be used for definition of (formal) languages?

Question

I wanted to know which standard symbol should be used as a delimiter when recursively defining a (formal) language, such as this fragment of arithmetic expressions :

X ::= 0 | 1 | X+X | X*X |

I use |, but I have to put by hand the spaces between the bar and the left and right symbols. Moreover, in other documents or papers, the bar looks like bigger than the standard one, so I wondered if there was a particular symbol or a best practice.

Edit : Here a short version of the kind of code I'm using right now :

\documentclass[11pt,letterpaper]{report}

\usepackage{amssymb,amsmath,amsfonts,amsxtra,amsthm}
% etc...

\begin{document}

% ...

\[ A ::= 0 | 1 | A+A | A \times A \]

%...

\end{document}

While I'm looking for spacing more like the definition at page 4, around the end of 1.1 in http://perso.ens-lyon.fr/olivier.laurent/folgames.pdf for example. I think its called Backus-Naur Form or something like that.

Answer 1

Those bars look like relation symbols, so \mid should be the choice.

However, defining an own command for it can surely be considered best practice: you can easily change the appearance of the symbol by just changing its definition. Here's an example, where the \renewcommand serves for the purpose of showing how you can modify the symbol without changing the document code.

\documentclass[11pt,letterpaper]{report}
\usepackage{amsmath,amssymb,amsthm}

\usepackage{bm} % for the second version

\newcommand{\bnfor}{\mid}

\begin{document}

\[ A ::= 0 \bnfor 1 \bnfor A+A \bnfor A \times A \]

\renewcommand{\bnfor}{\mathrel{\big\bracevert}}

\[ A ::= 0 \bnfor 1 \bnfor A+A \bnfor A \times A \]

\end{document}