Backus-Naur記法
[math] \newcommand{\mathsetextension}[1]{% \left\{ #1 \right\}% } \newcommand{\mathderiv}{\mathrel{\mathop{\Rightarrow}}^{*}} \newcommand{\mathgen}{\rightsquigarrow} \newcommand{\emptyword}{\varepsilon} \newcommand{\kleenecl}[1]{{#1}^{*}} \newcommand{\interpret}[1]{[\![#1]\!]} \newcommand{\mathautomaton}[1]{\mathcal{#1}} \newcommand{\mathnat}{\mathbb{N}} \newcommand{\qed}{\blacksquare} [/math]
Backus-Naur記法(Backus-Naur form) とは文脈自由言語の文法を定義するのに用いられる標準的な記法である。 BN記法、BNF記法や単に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\] という記号列全体を表現できている．
BNF記法の具体例
命題論理の論理式の表現
数理論理学の基礎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$ の関数記号である。
関連項目
| 文法のタイプ | 言語のクラス | 計算モデル |
|---|---|---|
| タイプ0 | 句構造言語 | Turingマシン |
| タイプ1 | 文脈依存言語 | 線形有界オートマトン |
| タイプ2 | 文脈自由言語 | プッシュダウン・オートマトン |
| タイプ3 | 正規言語 | 有限オートマトン |
