Proofs: Operator-precedence parsing

OP-PARSE accepts exactly the sentences of an operator precedence grammar and stops after O(n) steps full

This proof shows: correctness.

Statement. Let $G$ be an operator grammar, without the productions that use a nonterminal deriving no terminal string, such that at most one of $\lessdot$, $\doteq$, $\gtrdot$ holds between any two symbols of $\Sigma \cup \{\$\}$, where the end markers are treated as the right side $\$ S \$$. Then for every input $w = a_1 \cdots a_n$, OP-PARSE stops after at most $2n + 2$ iterations of its loop, and it accepts if and only if $w \in L(G)$; when it accepts, it returns a parse tree of $w$.

Proof.

Step 1 (termination). Terminals enter the stack only by the shift at L4, which also advances the input, so there are at most $n$ shifts before the current token is $\$$, and $\$$ is never shifted, because $\$ \doteq \$$ is not a relation and no $\$ \lessdot \$$ or $\$ \gtrdot \$$ can be derived from right sides that do not contain $\$$. Each reduction removes at least one terminal from the stack: L6 pops at least one. So there are at most $n$ reductions, and with the final step at L3 or L9 the loop runs at most $2n + 2$ times. The pop at L6 never removes the bottom $\$$: a terminal $x$ is pushed above the topmost terminal $y$ only if $y \lessdot x$ or $y \doteq x$, and the first terminal above $\$$ was pushed with $\$ \lessdot x$, since $\$ \doteq x$ would need a right side with $\$$ and a terminal $x$ next to it, and $\$ S \$$ has none.

Step 2 (soundness). We claim that every nonterminal entry on the stack is a map from a set $N$ of nonterminals to trees, where the tree for $A \in N$ is a parse tree with root $A$ whose yield is the part of the input covered by the entry, and that the entries and terminals on the stack cover the shifted input from left to right. A shift adds a terminal. A reduction at L8 builds, for a production $A \to X_1 \cdots X_m$ that matches the handle, the node $A$ whose children are the handle's terminals and, for each nonterminal $X_i$, the tree for $X_i$ of the corresponding entry; this is a parse tree with yield the covered input. A unit production $B \to A$ adds the node $B$ above the tree for $A$. If OP-PARSE accepts at L3, the whole input has been shifted, the stack is $\$ \, N$ with $S \in N$, and the tree for $S$ is a parse tree of $w$. So acceptance implies $w \in L(G)$.

Step 3 (contracted trees). Now let $w \in L(G)$ with a parse tree $t$. A unit chain of $t$ is a maximal path of nodes $B_1, B_2, \ldots, B_r$ in which each $B_i$ has the single nonterminal child $B_{i+1}$ for $i < r$, by the production $B_i \to B_{i+1}$; its bottom $B_r$ uses a production that is not a unit production. Contract each unit chain to one node, labeled with the chain. Every node of the contracted tree $\hat t$ uses a production whose right side has a terminal: a right side that is not a unit production and not empty either is one terminal or has length at least 2 with no two adjacent nonterminals.

Process the nodes of $\hat t$ in postorder, the children from left to right. After the first $k$ nodes have been processed, the cut is the string obtained from $w$ by replacing the yield of each maximal processed subtree by its root. Let $h$ be the $(k+1)$-th node. All its children are leaves or processed, so its children are a substring of the cut, of the form $[X_0] \, c_1 [X_1] \cdots c_m [X_m]$ with terminals $c_1, \ldots, c_m$, $m \ge 1$, and optional processed nodes $X_i$. Everything to the right of $h$ in the cut is an unprocessed leaf, a terminal. Write the cut as $\$ \, \pi \, [X_0] c_1 \cdots c_m [X_m] \, \rho \, \$$.

Step 4 (the relations around $h$). Let $\ell$ be the last terminal of $\$ \pi$ and $r$ the first symbol of $\rho \$$, a terminal. Treat the two end markers as children of a virtual root above $S$ with the right side $\$ S \$$.

(a) $c_i \doteq c_{i+1}$, since both are children of $h$ with at most one nonterminal between them.

(b) $\ell \lessdot c_1$. The parent $p$ of the leaf $\ell$ is not processed, since $h$ comes before it in postorder ($h$ is not in the subtree of $p$ to the left of $\ell$, and if $h$ were in the subtree of a child of $p$ to the left of $\ell$, its yield would be to the left of $\ell$). If $p = h$, then $\ell$ would be a terminal child of $h$ to the left of $c_1$, which is impossible. So the subtree of $h$ is to the right of $\ell$. Let $Y$ be the child of $p$ right after $\ell$. If $Y$ is a terminal, it is the symbol right after $\ell$ in the cut, which is $X_0$ or $c_1$; $X_0$ is not a terminal, and $Y = c_1$ would make $p = h$. So $Y$ is a nonterminal, and the subtree of $Y$ starts right after $\ell$. If that subtree contains $c_1$, then $Y \Rightarrow^+ [X_0] c_1 \cdots$ with $X_0$ a single nonterminal, so $c_1 \in \mathrm{LEADING}(Y)$ and $\ell \lessdot c_1$, using the unit chains and labels of $t$. Otherwise the subtree of $Y$ is exactly $X_0$, which is processed; then the next child of $p$ after $Y$, if any, is a terminal adjacent to $X_0$ in the cut, that is, $c_1$, which again gives $p = h$; and if $Y$ is the last child of $p$, all children of $p$ are processed or leaves to the left of $h$'s yield, so $p$ comes before $h$ in postorder, a contradiction.

(c) $c_m \gtrdot r$. The parent $q$ of $r$ is not processed, because its leaf $r$ is not. If $q = h$, $r$ would be a child of $h$ after $c_m$, which is impossible. The child $Z$ of $q$ right before $r$ is not the terminal $c_m$ (else $q = h$), and not a terminal at all, since the symbol right before $r$ in the cut is $c_m$ or $X_m$. So $Z$ is a nonterminal whose subtree ends right before $r$ and contains $c_m$, since a subtree that is only $X_m$ would leave $c_m$ before it as a child of $q$, again $q = h$. Thus $Z \Rightarrow^+ \cdots c_m [X_m]$, so $c_m \in \mathrm{TRAILING}(Z)$ and $c_m \gtrdot r$.

(d) For two consecutive terminals $x, y$ of $\$ \pi \, c_1$ ($y$ right after $x$, possibly with one nonterminal between them), $x \lessdot y$ or $x \doteq y$. If $y = c_1$ this is (b). Otherwise the parent $p$ of $x$ is unprocessed, by the argument of (b), and the child $Y$ of $p$ after $x$ is either the terminal $y$, giving $x \doteq y$, or a nonterminal followed in $p$ by $y$, giving $x \doteq y$, or a nonterminal whose subtree contains $y$, giving $y \in \mathrm{LEADING}(Y)$ and $x \lessdot y$. The remaining cases, where $Y$ is processed and is the last child of $p$, or $x$ is the last child of $p$, make $p$ processed before $h$, as in (b).

Since at most one relation holds between any two terminals, (a) to (d) determine the relation of every pair used below, and in particular $c_i \lessdot c_{i+1}$ and $\ell \doteq c_1$ do not hold.

Step 5 (the parser follows $\hat t$). We show by induction on $k$: when the parser has made all moves up to the $k$-th reduction, its stack is $\$ \pi$ with the same terminals, nonterminal entries at the places of the processed nodes, the input pointer is at the first unprocessed leaf, and the entry of each processed node with unit chain $B_1, \ldots, B_r$ contains $B_1$, the label its parent's production uses.

Before the reduction of $h$, the parser is in the configuration where the stack is $\$ \pi$ and the input is $[\ldots] c_1 \cdots$. As long as the topmost stack terminal is $x$ and the next token $y$ is $c_1$ or a terminal of $h$, (b), (a) and (d) give $\lessdot$ or $\doteq$, so L4 shifts. When the stack holds $\ldots \ell [X_0] c_1 [X_1] \cdots c_m [X_m]$ and the next token is $r$, (c) gives $\gtrdot$, so L5 reduces. The pops at L6 remove $c_m, \ldots, c_1$: after popping $c_{i+1}$ the topmost terminal is $c_i$ and $c_i \doteq c_{i+1}$ is not $\lessdot$, and after popping $c_1$ the topmost terminal is $\ell$ with $\ell \lessdot c_1$. So the handle is exactly the children of $h$. The production of the bottom of $h$'s unit chain matches it, because each child entry contains the label used in that production, so it is in $N$, and closing under unit productions adds the whole chain up to its top. This is the claim for $k + 1$.

After the root has been processed, the stack is $\$ \, N$ with the root chain in $N$, whose top is $S$, and the input is at $\$$. L3 accepts. Since the moves before were all shifts and reductions with nonempty $N$, no error was reported earlier. So $w \in L(G)$ implies acceptance. $\blacksquare$