Proofs: Pike VM

The Pike VM returns the leftmost-first match full

This proof shows: correctness, termination.

Fix the program $\mathit{prog}$ compiled from $r$ and the text $w = a_1 \cdots a_n$. A configuration is a pair $(p, i)$ of an instruction number and a position $0 \le i \le n$. Its steps are: from char $a$ at $(p, i)$ to $(p + 1, i + 1)$ when $i < n$ and $a_{i+1} = a$; from jmp $x$ to $(x, i)$; from split $x, y$ to $(x, i)$ and then $(y, i)$, in this order of preference; from save $k$ to $(p + 1, i)$, writing $i$ into slot $k$; no step from fail or match. A leaf is a configuration at a char or match instruction. A path from $(0, s)$ determines the slots it has written, so a thread $(p, \mathit{caps})$ created at position $i$ is the end of a path from $(0, s)$ to $(p, i)$ with $s = \mathit{caps}[0]$, the start of the thread.

Lemma 1 (the program). For each subexpression $t$, let $b$ be the first instruction of its code and $e$ the instruction right after it. For all $i \le j$, there is a path from $(b, i)$ to $(e, j)$ that stays inside the code of $t$ before it reaches $e$ if and only if $a_{i+1} \cdots a_j \in L(t)$. Consequently a path from $(0, s)$ to a match configuration $(p, e)$ exists if and only if $a_{s+1} \cdots a_e \in L(r)$, and on such a path slots 0 and 1 hold $s$ and $e$.

Proof. By induction on $t$, following the code shapes. For $\emptyset$ the code is fail, with no step, and $L(\emptyset) = \emptyset$. For $\varepsilon$ the code is empty, so $b = e$ and the only path is the empty one, with $i = j$. For a symbol $a$ the only path is one char step, which needs $j = i + 1$ and $a_{i+1} = a$. For $t_1 t_2$ the code of $t_2$ starts where that of $t_1$ ends, and any path from $b$ to $e$ passes the boundary once, so it splits into a path for $t_1$ and one for $t_2$. For $t_1 \mid t_2$ a path goes from the split into one branch, and the left branch ends with jmp to $e$, so it is a path for $t_1$ or for $t_2$. For a group, the two save instructions do not move. For $t_1^*$ and $t_1^{*?}$, a path from the split to $e$ passes through the body some number $q \ge 0$ of times, each pass from the body's first instruction to the jmp back, so it reads a word of $L(t_1)^q$, and every such word gives such a path. The last statement follows by applying the claim to $r$ inside "save 0; code; save 1; match". $\square$

ADD and the lists. ADD$(L, p, \mathit{caps}, i)$ with an explicit stack visits configurations at position $i$ depth first, the preferred target of a split first, and skips any pc already marked in $L$ (line L14). Call the calls of ADD on a list its entries. The list at position $i + 1$ has as entries the successors of the char leaves of the list at $i$ that read $a_{i+1}$, in the order of that list; the list at $i$ has as last entry the start $(0, i)$ if no match was recorded before (line L3).

Lemma 2 (depth first search with a shared mark set). Let $e_1, e_2, \dots$ be the entries of one list, in order. A pc $x$ is marked during entry $e_t$ for the least $t$ such that some path of steps at position $i$ leads from $e_t$ to $x$.

Proof. Let $t$ be least with a path from $e_t$ to $x$. No earlier entry reaches $x$, so $x$ is not marked before $e_t$. During $e_t$, a depth first search from $e_t$ reaches every pc that has a path from $e_t$ avoiding the pcs marked before $e_t$. If every path from $e_t$ to $x$ met such a pc $y$, then $y$ was reached from some $e_{t'}$ with $t' < t$, and $x$ would be reachable from $e_{t'}$ through $y$, against the choice of $t$. $\square$

Lemma 3 (sorted by start). In every list, the starts of the threads are nondecreasing in list order, and the starts of the entries are too.

Proof. By induction on the position. The entries of the list at $i + 1$ come from the list at $i$ in order and keep their starts, then possibly the start entry with start $i + 1$, which is larger than every start so far. Each entry appends threads with its own start. $\square$

Theorem 1 (the match exists and starts leftmost). PIKE-VM returns a match if and only if some substring $a_{s+1} \cdots a_e$ is in $L(r)$, and then the match has the least such start $s^*$, and $a_{s^*+1} \cdots a_{e'}$ is in $L(r)$ for its end $e'$.

Proof. Every recorded match is the end of a real path from $(0, s)$, so by Lemma 1 it spells a substring of $L(r)$. If no substring is in $L(r)$, nothing is recorded and the VM returns none.

Suppose some substring is in $L(r)$, let $s^*$ be the least start of one, and fix a path $\pi$ from $(0, s^*)$ to a match configuration $(p_m, e)$. For each $i$ from $s^*$ to $e$ let $x_i$ be the leaf of $\pi$ at position $i$ (the last configuration of $\pi$ at position $i$, which is a char leaf for $i < e$ and the match for $i = e$). Call a thread good if a match is reachable from its configuration. A good thread has start at least $s^*$, since its start reaches a match through it, so by the choice of $s^*$ every good thread has start exactly $s^*$ or more.

First, a match with start $s^*$ is recorded at some point. Suppose not. Then the start entry $(0, s^*)$ is added at position $s^*$: a match recorded before round $s^*$ would end before $s^*$, so its start would be less than $s^*$, which is impossible. We show by induction that $x_i$'s pc is in the list at $i$ for $i = s^*, \dots, e$. The pc is reached from an entry of start at most $s^*$ by Lemma 2 (the entry on $\pi$ reaches it), so its thread has start at most $s^*$ and is good, so its start is $s^*$. It can be dropped only by line L10 for a match ahead of it, which by Lemma 3 has start at most $s^*$, so equal to $s^*$, against the assumption. Then its char step leads into the next list. At $i = e$ the thread for $p_m$ is a match with start $s^*$, which is recorded unless an earlier match in the list is recorded first, with start at most $s^*$, again a contradiction.

Second, once a match with start $s^*$ is recorded, every later recorded match comes from a thread ahead of it in some list, or from a descendant of such a thread, and so has start at most $s^*$ by Lemma 3, hence exactly $s^*$, since recorded matches are good. So the final match has start $s^*$. $\square$

To describe which match from $s^*$ is returned, define the reference search BT: for $s = 0, 1, \dots, n$ in order, run a depth first search from $(0, s)$ that follows the steps of a configuration in order of preference, keeps one global set of visited configurations, and skips a configuration already visited. Let $\mathcal{P}$ be the order in which BT, run to the end without stopping, first visits configurations. The bit-state backtracker returns the first match configuration in $\mathcal{P}$, with the slots of the path that first visited it.

Lemma 4 (same order). Consider the VM with line L10 disabled and line L3 always active. For every position $i$, its list at $i$ holds exactly the leaves at position $i$ in the order of $\mathcal{P}$, each with the slots of the path by which BT first visits it.

Proof. By induction on $i$. Configurations at different positions are different, so the visited set of BT, restricted to position $i$, is a mark set for position $i$ only. BT enters position $i$ either through the char step of a leaf at $i - 1$, which it takes right after first visiting that leaf, or from the start $(0, i)$, after all searches from smaller starts are finished. By the induction hypothesis the char leaves at $i - 1$ are first visited by BT in the order of the VM's list at $i - 1$, so BT makes its entries into position $i$ in the order of the VM's entries, ending with $(0, i)$. After each entry, BT finishes the depth first search below it before the next entry. Inside position $i$ this search follows the same steps in the same order as ADD, with the same marks, and the searches at later positions that it starts do not touch position $i$. So both visit the configurations at $i$ in the same order, through the same paths, and the leaves come out in the same order. $\square$

In $\mathcal{P}$, a char leaf $u$ at position $i$ has one step, to position $i + 1$, and every configuration that BT first visits from $u$ comes right after $u$ and before the next configuration at position $i$ or earlier. Call these the descendants of $u$. A match leaf at position $i$ is never a descendant of a char leaf at position $i$. So for a char leaf $u$ and a match leaf $q$ at the same position: if $u$ comes before $q$ in $\mathcal{P}$, so do all descendants of $u$; if $u$ comes after $q$, so do all its descendants.

Lemma 5 (the cut). For the real VM, let $R_i$ be the match recorded before round $i$ (or none). Then the list at $i$ holds, in the order of $\mathcal{P}$, exactly the leaves at position $i$ that come before every match leaf at a position less than $i$, and $R_i$ is the first match leaf in $\mathcal{P}$ among those at positions less than $i$.

Proof. By induction on $i$. At $i = 0$ nothing is recorded and the list is the closure of $(0, 0)$, as in Lemma 4. Assume the claim at $i$. The round at $i$ processes the list in order and stops at its first match leaf $q$, if any.

The new $R_{i+1}$: if $q$ exists, it comes before every match leaf at positions less than $i$, by the hypothesis, and before every other match leaf at position $i$: those in the list come after it, and those not in the list come after some match leaf at a smaller position, which comes after $q$. So $q$ is the first in $\mathcal{P}$ among match leaves at positions up to $i$, and the VM records it. If $q$ does not exist, every match leaf at position $i$ is outside the list, so it comes after $R_i$, and $R_{i+1} = R_i$ is still first.

The list at $i + 1$: a leaf $v$ at $i + 1$ is a descendant of some char leaf $u$ at $i$, or comes from the start $(0, i + 1)$, which comes after everything at smaller starts. By the remark above, $v$ comes before every match leaf at positions up to $i$ exactly when $u$ does, that is, when $u$ is in the list at $i$ and ahead of $q$. These are exactly the char leaves whose steps the VM follows at line L7. The start $(0, i + 1)$ comes before every match leaf at smaller positions exactly when there is none, which is when line L3 adds it. Since the dropped entries come after the kept ones, the kept entries see the same marks as in Lemma 4, and the leaves come out in the same order, with the same slots. $\square$

Theorem 2 (leftmost-first). PIKE-VM returns the first match configuration of $\mathcal{P}$, with the slots of its path, which is the result of the bit-state backtracker.

Proof. The VM ends after round $n$, or earlier when a list is empty. If it ends after round $n$, then $R_{n+1}$ is the first match leaf in $\mathcal{P}$ by Lemma 5. If the list at $i$ is empty, then by Lemma 5 no leaf at position $i$ comes before $R_i$. A leaf at a later position is a descendant of a leaf at $i$, or comes from a start larger than $i$, which comes after $R_i$ if $R_i$ exists. If $R_i$ does not exist, the start $(0, i)$ was added and gave no leaf, so the closure of $(0, \cdot)$ has no leaf at any position, and there is no leaf after position $i$ at all. In both cases no match leaf at a later position comes before $R_i$ in $\mathcal{P}$, so the VM returns the first one. $\square$

Remark (plain backtracking). If no star of $r$ has a nullable body, there is no cycle of steps at one position: every backward jump closes a star, and going around it at one position means reading the empty word through its body, which by Lemma 1 needs a nullable body. Then the configurations form an acyclic graph, every path is simple, and a configuration that BT skips was fully searched before without finding a match, so skipping it changes nothing. BT then returns the first accepting path in the order of preference, which is what a backtracking matcher without a visited set returns.

Termination. Each round calls ADD on at most $m$ distinct pcs per list, by line L14, and each pc does a bounded amount of work. There are at most $n + 1$ rounds. So the VM stops. $\blacksquare$