Definition:Parsing Sequence

From ProofWiki
Jump to navigation Jump to search

Definition

Let $\FF$ be a formal language with alphabet $\AA$.

Let $S$ be a collation in $\AA$.


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

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


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.


Sources