Backus–Naur記法
概要
Backus–Naur記法について説明する。
Backus–Naur記法 (Backus-Naur form) とは文脈自由言語の文法を定義するのに用いられる標準的な記法である。 BN記法、BNF記法や単にBNFとも呼ばれる。 通常、形式言語理論においては、記号集合を有限にするが、 この項目においては記号集合が無限であることがある。
以下ではBNF記法と書く。
概要
BNF記法にはさまざまなバリエーションがあるが共通して
$$\text{定義したい記号列を表すメタ記号}::=\text{記号列の並びを指定するメタ記号の列}\mathrel{|}\cdots\mathrel{|}\text{記号列の並びを指定するメタ記号の列}$$
という表現が用いられる。
たとえば、BNF記法を用いて自然数の二進表現$B$を表現すると次のようになる。
\begin{align*}
{B} &::= {b\mathrel{|}1B'} \\
{B'} &::= {b\mathrel{|}bB'} \\
{b} &::= {0\mathrel{|}1}
\end{align*}
この記法によって、$B$は
$$0, 1, 10, 11, 100, 101, 110, 111, 1000,\ldots$$
という記号列全体を表現できている。
例
命題論理の論理式の表現
数理論理学の基礎1の記事に書いてある命題論理の論理式$\varphi$の定義は次のように表現できる。
\begin{align*}
{p} &\in {\mathrm{PropVar}} \\
{\varphi} &::= {p \mathrel{|} \top \mathrel{|} \bot \mathrel{|} (\lnot\varphi) \mathrel{|} (\varphi\land\varphi) \mathrel{|} (\varphi\lor\varphi) \mathrel{|} (\varphi\to\varphi)}
\end{align*}
等式論理の項、論理式の表現
数理論理学の基礎1の記事に書いてある等式論理の$\mathscr{L}$-項$t$と$\mathscr{L}$-論理式$\varphi$ の定義は次のように表現できる。
\begin{align*}
{t} &::= {v\mathrel{|}f(\overbrace{t,\ldots,t}^{n\text{個}})} \\
{\varphi} &::= {t=t}
\end{align*}
ただし、$v$は変数記号を表し、$f$は項数$n$の関数記号である。
