Definition:Parsing Sequence

From ProofWiki
Jump to navigation Jump to search


Let $\mathcal F$ be a formal language with alphabet $\mathcal A$.

Let $S$ be a collation in $\mathcal A$.

A parsing sequence for $S$ in $\mathcal F$ is a sequence of collations in $\mathcal F$ formed by application of rules of formation of $\mathcal F$ from previous collations in this sequence, and ending in the collation $S$.

If $S$ has no parsing sequence in $\mathcal F$, then it is not a well-formed formula in $\mathcal F$.

A parsing sequence for a given well-formed formula in any formal language is usually not unique.

Thus, we can determine whether $S$ is a well-formed formula in any formal language by using a sequence of rules of formation of that language.

To parse a collation in a formal language is to find a parsing sequence for that collation, and thereby to determine whether or not it is a well-formed formula.

Also known as

Some sources call a parsing sequence a derivation.

Other sources use the term derivation tree or formation tree.

The latter names arise from the presentation of the parsing sequence as a labeled tree.