简化对齐/数组组合（BNF 语法）

Question

我经常需要使用 Backus-Naur Form (BNF) 语法写出类型、程序等的语法。我已经习惯用

\begin{alignat*}{2}
  \text{\itshape Types} &\quad&
    A &\begin{array}[t]{@{}r@{}l@{}}
         {} \Coloneqq {} & A_1 \times A_2 \mid 1 \\
                 \mid {} & A_1 + A_2 \mid 0
       \end{array}
  \\
  \text{\itshape Programs} &&
    P &\Coloneqq \dotsb
\end{alignat*}

有没有办法改善这种标记？具体来说：

• {}下面的\Coloneqq和\mid能以某种方式移到array的列规范中吗？我试过了\begin{array}[t]{@{}r@{{}}l@{}}，但没有用。
• 是否可以\Coloneqq将 移到 之外array，同时仍将\mid每个新行开头的 s 与 的右侧对齐\Coloneqq？

Answer 1

为了在列的开头和结尾插入一个空组，您可以使用>{{}}和<{{}}。

不过，我不会使用alignat。

\documentclass{article}
\usepackage{mathtools,array}

\newcommand{\bnflabel}[1]{\textit{#1}}
\newenvironment{bnf}
 {\renewcommand{\arraystretch}{1.2}\begin{array}{@{}r@{\quad}l@{}}}
 {\end{array}}
\newenvironment{bnfalign}
  {\renewcommand{\arraystretch}{1}%
   \begin{array}[t]{@{}>{{}}r<{{}}@{}l@{}}}
  {\end{array}}

\begin{document}

\[
\begin{bnf}
  \bnflabel{Types} &
    \begin{bnfalign}
      A \Coloneqq & A_1 \times A_2 \mid 1 \\
            \mid  & A_1 + A_2 \mid 0
    \end{bnfalign}
  \\
  \bnflabel{Programs} & P \Coloneqq \dotsb
\end{bnf}
\]

\end{document}