# Definition:Parsing Sequence

## Definition

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.

## Sources

- 1993: M. Ben-Ari:
*Mathematical Logic for Computer Science*(1st ed.) ... (previous) ... (next): $\S 2.2$: Propositional formulas - 1996: H. Jerome Keisler and Joel Robbin:
*Mathematical Logic and Computability*... (previous) ... (next): $\S 1.2$: Syntax of Propositional Logic - 2000: Michael R.A. Huth and Mark D. Ryan:
*Logic in Computer Science: Modelling and reasoning about systems*... (previous) ... (next): $\S 1.3$: Propositional logic as a formal language - 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous) ... (next): $\S 2.1.6$