We have discussed rules of the form
that could be interpreted as a decomposition scheme describing how a task A
can be solved: Select a suitable rule for A, and solve the subtasks
B1, B2, ... , Bn.
Given the interpretation
this could also be read as: A proof of A can be obtained from proofs
of B1 , B2 , ... , Bn.
A if B1 and B2 and ... and Bn
The same kind of rules can also be used to describe formal languages
by recursive definitions. In the definition of Algol 60
the following notation (known as Backus-Naur-Formalism, BNF)
which states that a member of a syntactic class
< A >
can be composed from members of syntactic classes
< B1 >, < B2 >, ..., < Bn >.
< A > ::=
< B1 > < B2 > ... < Bn >