Proofs: Packrat parsing

PACKRAT-PARSE computes the PEG semantics, stops exactly when it is undefined, and runs in time O(|G| (n + 1)) full

This proof shows: correctness.

Statement. Let $G$ be a PEG with $g$ subexpressions and start expression $e_S$, and let $w = a_1 \cdots a_n$. Then PACKRAT-PARSE:

1. makes at most $g \, (n + 1)$ evaluations at lines L7 to L14, and stops after $O(g \, (n + 1))$ steps;
2. stops at L6 or L12 if and only if $\mathrm{m}(e_S, 0)$ is undefined;
3. otherwise computes $j = \mathrm{m}(e_S, 0)$, accepts exactly when $j = n$, and then returns the parse tree of the match.

Setup. The semantics $\mathrm{m}(e, i)$ is defined by the clauses of the parsing expression grammar page. For a repetition we use the clause $\mathrm{m}(e_1^*, i) = i$ if $\mathrm{m}(e_1, i) = \mathsf{fail}$ and $\mathrm{m}(e_1^*, i) = \mathrm{m}(e_1^*, j)$ if $\mathrm{m}(e_1, i) = j$. A value $\mathrm{m}(e, i)$ is defined when it has a finite derivation by these clauses. Each clause is deterministic: given $(e, i)$, it names the first pair $(e', i')$ whose value it needs, and the value of each needed pair determines the next pair needed or the result. Call these pairs the calls of $(e, i)$. So a defined value has exactly one derivation, a finite tree whose root is $(e, i)$ and whose children are the calls of $(e, i)$, each with its own derivation.

Step 1: the stored values are correct. Claim: whenever the parser stores $r$ in $\mathit{memo}[e, i]$, $\mathrm{m}(e, i)$ is defined and equals $r$. Induction on the order of the stores. A terminal or the empty expression is stored at once by its clause. A composite pair $(e, i)$ is opened at L7 and asks for its calls one after the other; each answer comes from the table at L5, or from a pair opened and stored later but finished earlier, so by the induction hypothesis each answer is the defined value of the call. Lines L9 to L13 then compute the next call, or the result, exactly as the clause does: L10 passes the end of each part as the start of the next and stops at the first $\mathsf{fail}$; L11 returns the first alternative that does not fail; L12 returns $i$ when $e_1$ fails and otherwise the value at the end of $e_1$; L13 turns $\mathsf{fail}$ into $i$ and a success into $\mathsf{fail}$ for $!$, and the reverse for $\&$. So the stored value is the result of the clause applied to defined values, and $\mathrm{m}(e, i)$ is defined with this value.

Step 2: each pair is evaluated at most once. A pair is evaluated when it is requested, is not in the table and is not open. From then until it is stored it is open, and a request for it during that time stops the run at L6; after it is stored, requests are answered at L5. So there are at most $g \, (n + 1)$ evaluations, one for each pair with $0 \le i \le n$; positions never exceed $n$, since a terminal succeeds only when $i < n$.

Step 3: the number of steps. An evaluation of $e$ requests at most $k + 1$ calls, where $k$ is the number of children of $e$ (the $+1$ is the recursive request of a repetition). Each request costs a constant number of steps besides the evaluation it may start. The sum of $k + 1$ over all subexpressions is at most $2g$, so the requests number at most $2g \, (n + 1)$ and EVAL takes $O(g \, (n + 1))$ steps. Together with Step 2 this proves the first half of part 1.

Step 4: an early stop means no result. The open pairs at any moment form a chain $(e_0, i_0), (e_1, i_1), \ldots, (e_t, i_t)$ in which $(e_0, i_0) = (e_S, 0)$ and each pair is a call of the previous one, made after the values of its earlier calls were obtained, which by Step 1 are the defined values. Suppose the run stops at L6: the top pair requests $(e_s, i_s)$ for some $s \le t$. Then the derivation of $\mathrm{m}(e_s, i_s)$, if it existed, would contain, along the chain $e_s, \ldots, e_t$, a derivation of $\mathrm{m}(e_s, i_s)$ as a proper subtree, which is impossible for a finite tree. Suppose it stops at L12: the repetition $e_1^*$ at $i$ found $\mathrm{m}(e_1, i) = i$, so its clause calls $(e_1^*, i)$ itself, and again the derivation would contain itself. In both cases the value of the pair at the stop is undefined, and so are the values of all pairs below it in the chain, since each needs the next. In particular $\mathrm{m}(e_S, 0)$ is undefined.

Step 5: no early stop when there is a result. Suppose $\mathrm{m}(e_S, 0)$ is defined, with the derivation $D$. By Step 1 and the determinism of the clauses, every pair that the parser opens is a node of $D$, and the open chain is a path of $D$ from the root. A stop at L6 would give two nodes on one path of $D$ with the same pair, and the subtree of the lower one would be a derivation of the same value inside its own derivation, contradicting uniqueness and finiteness; precisely, the derivation of the upper node strictly contains a copy of itself, so its height exceeds itself. A stop at L12 would give a node $(e_1^*, i)$ of $D$ whose call is $(e_1^*, i)$, the same contradiction. So the parser does not stop early, and by Steps 2 and 3 it finishes the evaluation of $(e_S, 0)$; by Step 1 it obtains $j = \mathrm{m}(e_S, 0)$. Line L3 accepts exactly when $j = n$. With Step 4 this proves part 2 and the first half of part 3.

Step 6: the tree. Define the output of a successful pair $(e, i)$ with $\mathrm{m}(e, i) = j$: for a terminal, the token $a_{i+1}$; for $\varepsilon$ and the predicates, nothing; for a nonterminal $A$, one node $A$ whose children are the output of $(e_A, i)$; for a sequence, the outputs of its parts at the successive positions; for a choice, the output of the first alternative that succeeds; for $e_1^*$ with $\mathrm{m}(e_1, i) = i' \ne \mathsf{fail}$, the output of $(e_1, i)$ followed by that of $(e_1^*, i')$, and nothing when $e_1$ fails. The parse tree is the node $S$ with the output of $(e_S, 0)$. Each part referred to here is a call of the pair, so by Step 1 its position and success are those stored in the table, and the alternative of a choice is the one recorded at L11. TREE (lines L15 to L18) computes this output by induction on the derivation: it emits the token at L15, builds the node at L16, and at L17 visits the parts at the stored positions. In the implementation each pair is pushed on a work stack with the list it writes into, and the parts of a sequence are pushed in reverse order, so all output of one part is written before the next part is popped; the lists therefore receive their items from left to right.

A node for $A$ at $i$ is built once and shared. This does not change the value of the tree, since the output of a pair depends only on the pair.

Step 7: the cost of TREE. A pair $(e, i)$ that consumes at least one token occurs at most once in the written-out tree: two occurrences would both contain the leaf $a_{i+1}$, so one would lie inside the other, and both would start at $i$ with the same expression, which makes $D$ contain a derivation of the pair inside itself, excluded as in Step 5. TREE expands each node $(A, i)$ once. Inside one expansion it visits each subexpression of $e_A$ at most once, except for the iterations of repetitions, and each iteration is a pair that consumes a token, visited once in the whole run. So TREE takes at most $\sum_A |e_A| \, (n + 1) + g \, (n + 1) = O(g \, (n + 1))$ steps, which completes part 1, and it returns the parse tree, which completes part 3. $\blacksquare$