Definition:Formal Grammar
Definition
Let $\LL$ be a formal language whose alphabet is $\AA$.
The formal grammar of $\LL$ comprises of rules of formation, which determine whether collations in $\AA$ belong to $\LL$ or not.
Roughly speaking, there are two types of formal grammar: top-down grammar and bottom-up grammar.
Top-Down Grammar
A top-down grammar for $\LL$ is a formal grammar which allows well-formed formulas to be built from a single metasymbol.
Such a grammar can be made explicit by declaring that:
- A metasymbol may be replaced by a letter of $\AA$.
- A metasymbol may be replaced by certain collations labeled with metasymbols and signs of $\AA$.
From the words thus generated, those not containing any metasymbols are the well-formed formulas.
Bottom-Up Grammar
A bottom-up grammar for $\LL$ is a formal grammar whose rules of formation allow the user to build well-formed formulas from primitive symbols, in the following way:
- Letters are well-formed formulas.
- A collection of specified collations of well-formed formulas, possibly labeled with additional signs, are also well-formed formulas.
In certain use cases, the first clause is adjusted to allow for more complex situations, for example in the bottom-up specification of predicate logic
Extremal Clause
The extremal clause of a bottom-up grammar is the final rule which excludes all collations other than those specified in the formation rules from being well-formed formulas.
Also known as
The formal grammar may also be called syntax; however, a convenient viewpoint is to think of the formal grammar as explicating the syntax for the associated formal language.
Thus the formal grammar is a means to obtain a syntax for $\LL$, and multiple formal grammars may yield the same syntax.
Some sources call this merely a grammar, the term formal being taken for granted by the fact that a formal language is under discussion.
Sources
- 1993: M. Ben-Ari: Mathematical Logic for Computer Science ... (previous) ... (next): Chapter $1$: Introduction: $\S 1.2$: Propositional and predicate calculus