Backus-Naur form

From CS2800 wiki

Backus-Naur form (or BNF) is a convenient syntax for writing down inductively defined sets.

BNF definitions give the name of the set being defined, and the list of rules defining the set in a compact form, separated by a vertical bar ([math]\href{/cs2800/wiki/index.php/%5Cmid}{\mid} [/math]).

A BNF definition looks like this:

[math]\begin{align*} var_1 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} Set_1 &\href{/cs2800/wiki/index.php/BNF}{::=} \text{rule 1} \href{/cs2800/wiki/index.php/%5Cmid}{\mid} \text{rule 2} \href{/cs2800/wiki/index.php/%5Cmid}{\mid} \cdots \\ var_2 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} Set_2 &\href{/cs2800/wiki/index.php/BNF}{::=} \text{rule 1} \href{/cs2800/wiki/index.php/%5Cmid}{\mid} \text{rule 2} \href{/cs2800/wiki/index.php/%5Cmid}{\mid} \cdots \\ & \vdots \end{align*} [/math]

The rules define the various ways of constructing objects in the set. Any uses of the variables on the left hand-side of any of the equations, should be replaced by already-constructed elements of the corresponding set.

The [math]\href{/cs2800/wiki/index.php/BNF}{::=} [/math] symbol is simply used to indicate that the definition is a BNF definition.

For example, the rules defining the natural numbers say that [math]\href{/cs2800/wiki/index.php/Z}{Z} \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] and [math]\href{/cs2800/wiki/index.php/S}{S}~n \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] for any [math]n \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math]. These would be written in BNF as follows:

Definition: natural number
The set of natural numbers is given inductively by [math]n \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/BNF}{::=} \href{/cs2800/wiki/index.php/Z}{Z} \href{/cs2800/wiki/index.php/%5Cmid}{\mid} \href{/cs2800/wiki/index.php/S}{S}~n [/math]

The second rule says that you can form a new natural number by prepending an S onto an existing natural number.