Backus-Naur記法

Backus-Naur記法(Backus-Naur form) とは文脈自由言語の文法を定義するのに用いられる標準的な記法である。 BN記法、BNF記法や単にBNFとも呼ばれる。 通常,形式言語理論においては,記号集合を有限にするが, この項目においては記号集合が無限であることがある

以下ではBNF記法と書く。

BNF記法の概要

形式的に厳密な定義については文脈自由言語#BNFを 参照のこと.

BNF記法にはさまざまなバリエーションがあるが共通して $$\text{定義したい記号列を表すメタ記号}::=\text{記号列の並びを指定するメタ記号の列}\mathrel{|}\cdots\mathrel{|}\text{記号列の並びを指定するメタ記号の列}$$ という表現が用いられる。

たとえば、BNF記法を用いて自然数の二進表現 $B$ を表現すると次のようになる。 $$B\mathrel{::=}b\mathrel{|}1B'$$ $$B'\mathrel{::=}b\mathrel{|}bB'$$ $$b\mathrel{::=}0\mathrel{|}1$$ この記法によって、$B$は $$0, 1, 10, 11, 100, 101, 110, 111, 1000,\ldots$$ という記号列全体を表現できている.

BNF記法の具体例

命題論理の論理式の表現

数理論理学の基礎1の記事に書いてある命題論理の論理式 $\varphi$ の定義は次のように表現できる。

$$\begin{aligned}p &\in \mathrm{PropVar} \\ \varphi &\mathrel{::=} p \mathrel{|} \top \mathrel{|} \bot \mathrel{|} (\lnot\varphi) \mathrel{|} (\varphi\land\varphi) \mathrel{|} (\varphi\lor\varphi) \mathrel{|} (\varphi\to\varphi)\end{aligned}$$

等式論理の項、論理式の表現

数理論理学の基礎1の記事に書いてある等式論理の$\mathscr{L}$-項 $t$ と$\mathscr{L}$-論理式 $\varphi$ の定義は次のように表現できる。

$$\begin{aligned}t&\mathrel{::=}v\mathrel{|}f(\overbrace{t,\ldots,t}^{n\text{個}}) \\ \varphi &\mathrel{::=} t=t \end{aligned}$$ ただし、$v$は変数記号を表し、$f$は項数$n$の関数記号である。

関連項目

Chomsky 階層

文法のタイプ言語のクラス計算モデル
タイプ0句構造言語Turingマシン?
タイプ1文脈依存言語線形有界オートマトン?
タイプ2文脈自由言語プッシュダウン・オートマトン?
タイプ3正規言語有限オートマトン


トップ   編集 凍結 差分 バックアップ 添付 複製 名前変更 リロード   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS
Last-modified: 2020-11-06 (金) 00:42:24 (161d)