# Backus-Naur form

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 ().

A BNF definition looks like this:

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 symbol is simply used to indicate that the definition is a BNF definition.

For example, the rules defining the natural numbers say that and for any . These would be written in BNF as follows:

Definition: natural number

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