Proofs: One-pass regex matching

The one-pass matcher is correct, and its compile test is exact full

This proof shows: correctness, termination.

Let $r$ have positions $1, \dots, k$ and marked expression $r'$. Write $\pi$ for the map that replaces each position $p$ by $\mathrm{sym}(p)$, extended to sequences. A direct induction on $r$ shows $L(r) = \pi(L(r'))$, since marking and $\pi$ commute with union, concatenation and star. The sets Nullable, First, Last and Follow are computed by the usual rules: for $s \mid t$ they are unions; for $st$, $\mathrm{First} = \mathrm{First}(s) \cup (\mathrm{First}(t)$ if $s$ is nullable$)$, $\mathrm{Last} = \mathrm{Last}(t) \cup (\mathrm{Last}(s)$ if $t$ is nullable$)$, and each $p \in \mathrm{Last}(s)$ gets $\mathrm{First}(t)$ added to its Follow set; for $s^*$, each $p \in \mathrm{Last}(s)$ gets $\mathrm{First}(s)$ added. A sequence $p_1 \cdots p_n$ with $n \ge 1$ is a chain of $r$ when $p_1 \in \mathrm{First}(r)$, $p_n \in \mathrm{Last}(r)$ and $p_{i+1} \in \mathrm{Follow}_r(p_i)$ for each $i < n$.

Lemma 1 (Glushkov). $\varepsilon \in L(r')$ if and only if $r$ is nullable, and a nonempty sequence is in $L(r')$ if and only if it is a chain of $r$.

Proof. By induction on $r$. The nullable part is the usual induction, so we treat nonempty sequences. For $\emptyset$ and $\varepsilon$ there are no positions and no nonempty sequences in $L(r')$, and First is empty, so there are no chains. For a single position $p$, $L(r') = \{p\}$, and since $\mathrm{First} = \mathrm{Last} = \{p\}$ and $\mathrm{Follow}(p) = \emptyset$, the only chain is $p$.

For $s \mid t$, the positions of $s$ and of $t$ are disjoint, and Follow never links them. So a chain of $s \mid t$ lies in $s$ or in $t$ and is then a chain of that part, and conversely. The claim follows from the induction hypothesis.

For $st$, Follow adds only edges from $\mathrm{Last}(s)$ to $\mathrm{First}(t)$, and no edge leads from a position of $t$ to one of $s$. Take a sequence $uv$ with $u \in L(s')$ and $v \in L(t')$, not both empty. If both are nonempty, $u$ and $v$ are chains of $s$ and $t$, the last element of $u$ is in $\mathrm{Last}(s)$ and the first of $v$ in $\mathrm{First}(t)$, so $uv$ is a chain of $st$. If $u = \varepsilon$, then $s$ is nullable, so $\mathrm{First}(t) \subseteq \mathrm{First}(st)$ and the chain $v$ of $t$ is a chain of $st$. The case $v = \varepsilon$ is symmetric. Conversely, take a chain $x$ of $st$ and cut it before its first position of $t$, as $x = uv$. Every step inside $u$ is in $\mathrm{Follow}_s$ and every step inside $v$ is in $\mathrm{Follow}_t$. If $u$ is empty, then $x$ starts in $\mathrm{First}(st)$ at a position of $t$, which needs $s$ nullable, so $\varepsilon \in L(s')$, and $v$ is a chain of $t$. If $v$ is empty, then $x$ ends in $\mathrm{Last}(st)$ at a position of $s$, which needs $t$ nullable, and $u$ is a chain of $s$. If both are nonempty, the step from $u$ to $v$ is an added edge, so $u$ ends in $\mathrm{Last}(s)$ and $v$ starts in $\mathrm{First}(t)$, and both are chains. In each case $x \in L(s')L(t')$.

For $s^*$, First and Last are those of $s$, and Follow adds edges from $\mathrm{Last}(s)$ to $\mathrm{First}(s)$. A nonempty sequence of $L(s'^*)$ is $u_1 \cdots u_j$ with each $u_i$ a nonempty sequence of $L(s')$, so a chain of $s$, and joining them with added edges gives a chain of $s^*$. Conversely, cut a chain of $s^*$ at each step $p \to q$ with $q \notin \mathrm{Follow}_s(p)$. Such a step is an added edge, so $p \in \mathrm{Last}(s)$ and $q \in \mathrm{First}(s)$. Each piece starts in $\mathrm{First}(s)$, ends in $\mathrm{Last}(s)$ and steps inside $\mathrm{Follow}_s$, so it is a chain of $s$ and is in $L(s')$. $\square$

Let $G$ be the graph on $\{0, 1, \dots, k\}$ with an edge $p \to q$ for each $q \in \mathrm{Follow}(p)$, where $\mathrm{Follow}(0) = \mathrm{First}$, and let $F$ be the set of line L2. By Lemma 1, the sequences of $L(r')$ are exactly the sequences $p_1 \cdots p_n$ such that $0 \to p_1 \to \cdots \to p_n$ is a path of $G$ ending in $F$ (for $n = 0$, the path is $0$ alone and $0 \in F$ exactly when $r$ is nullable). Call such a path accepting. The set $U$ of line L3 is the set of nodes that lie on some accepting path, apart from $0$, which may or may not be in $U$.

Lemma 2 (the table). If ONE-PASS-COMPILE returns $(T, F)$, then for each $p \in U \cup \{0\}$ and symbol $a$, $T[p][a]$ is defined exactly when some $q \in \mathrm{Follow}(p) \cap U$ has $\mathrm{sym}(q) = a$, and then $T[p][a]$ is that $q$, which is unique.

Proof. Lines L5 to L8 insert each $q \in \mathrm{Follow}(p) \cap U$ under the key $\mathrm{sym}(q)$, and line L7 returns before a second $q$ with the same symbol is inserted. So, when the compile ends at line L9, each key has exactly one such $q$, and every such $q$ is a key. $\square$

Lemma 3 (one-pass runs follow accepting paths). Suppose the compile returns $(T, F)$. Let $w = a_1 \cdots a_n$ and let $0 \to p_1 \to \cdots \to p_n$ be an accepting path with $\mathrm{sym}(p_i) = a_i$. Then the matcher, on $w$, takes $p = p_i$ after reading $a_i$ for each $i$, and accepts with $P = p_1 \cdots p_n$.

Proof. Every $p_i$ lies on an accepting path, so $p_i \in U$. By induction on $i$, with $p_0 = 0$: before round $i$ the matcher has $p = p_{i-1}$. Since $p_i \in \mathrm{Follow}(p_{i-1}) \cap U$ and $\mathrm{sym}(p_i) = a_i$, Lemma 2 gives $T[p_{i-1}][a_i] = p_i$, so line L12 does not reject and line L13 sets $p = p_i$ and appends it to $P$. After the loop $p = p_n \in F$ (or $p = 0 \in F$ when $n = 0$), so line L14 accepts with $P = p_1 \cdots p_n$. $\square$

Theorem 1 (the matcher). If the compile returns $(T, F)$, then ONE-PASS-MATCH$(T, F, w)$ accepts if and only if $w \in L(r)$. When it accepts, its list $P$ is in $L(r')$ with $\pi(P) = w$, and it is the only such sequence.

Proof. If $w \in L(r)$, then $w = \pi(x)$ for some $x \in L(r')$, and $x$ gives an accepting path with the symbols of $w$, so the matcher accepts by Lemma 3. Conversely, if the matcher accepts with $P = p_1 \cdots p_n$, then each $p_i = T[p_{i-1}][a_i]$, so by Lemma 2 $p_i \in \mathrm{Follow}(p_{i-1})$ and $\mathrm{sym}(p_i) = a_i$, and line L14 gives $p_n \in F$. So $0 \to p_1 \to \cdots \to p_n$ is an accepting path, $P \in L(r')$, and $w = \pi(P) \in L(r)$. For uniqueness, any $x \in L(r')$ with $\pi(x) = w$ gives an accepting path, and by Lemma 3 the matcher's list equals $x$, so $x = P$. $\square$

Theorem 2 (the test is exact). The compile returns NOT-ONE-PASS if and only if $r$ is not one-unambiguous, that is, if and only if there are $upv$ and $uqv'$ in $L(r')$ with $p \ne q$ and $\mathrm{sym}(p) = \mathrm{sym}(q)$.

Proof. Suppose line L7 fires at a node $p_0 \in U \cup \{0\}$ for two positions $q \ne q'$ in $\mathrm{Follow}(p_0) \cap U$ with the same symbol. Because $q$ and $q'$ are in $U$, they are reachable from $0$, and so $p_0$, which has an edge to them, is reachable from $0$ too (if $p_0 \ne 0$, it is in $U$). Take a path from $0$ to $p_0$ with the sequence of positions $u$. Since $q$ is in $U$, there is a path from $q$ to a node of $F$ with sequence $q v$, and in the same way a path from $q'$ to $F$ with sequence $q' v'$. Then $0 \to u \to q \to v$ and $0 \to u \to q' \to v'$ are accepting paths, so $uqv$ and $uq'v'$ are in $L(r')$, which breaks one-unambiguity.

Conversely, suppose $upv$ and $uqv'$ are in $L(r')$ with $p \ne q$ and $\mathrm{sym}(p) = \mathrm{sym}(q)$. Their accepting paths share the prefix for $u$, which ends at a node $p_0$ (the last element of $u$, or $0$ if $u$ is empty). All nodes of both paths after $0$ lie on accepting paths, so they are in $U$; in particular $p_0 \in U \cup \{0\}$ and $p, q \in \mathrm{Follow}(p_0) \cap U$. When the loop of line L4 reaches $p_0$, if it reaches it, line L6 meets both $p$ and $q$ with the same symbol, and line L7 returns NOT-ONE-PASS. If the loop never reaches $p_0$, it has already returned NOT-ONE-PASS at an earlier node. Either way the compile reports NOT-ONE-PASS. $\square$

Termination. The Glushkov sets are computed by one walk over the $m$ nodes of $r$. Line L3 runs two graph searches over the finite graph $G$, each adding a node at most once. The loop at lines L4 to L8 runs over at most $k + 1$ nodes and their finite Follow sets. The matcher loop runs once for each of the $n$ symbols of $w$, with one table lookup each. So both procedures stop.

Conclusion. By Theorem 2, the compile succeeds exactly on one-unambiguous expressions, and by Theorem 1 the matcher then decides $w \in L(r)$ and returns the unique sequence of positions that spells $w$. $\blacksquare$