Proofs: Incremental parsing

Incremental Earley reparsing returns the Earley chart of the edited string full

This proof shows: correctness.

Notation. $G = (V, \Sigma, P, S)$ is any context-free grammar, $w = a_1 \cdots a_n$ is the old string and $E[0], \ldots, E[n]$ is its Earley chart. The edit replaces $a_{p+1} \cdots a_q$ by $v$, with $0 \le p \le q \le n$ and $t = |v|$. The new string is $w' = a_1 \cdots a_p\, v\, a_{q+1} \cdots a_n = a'_1 \cdots a'_{n'}$, with $n' = n + \delta$, $\delta = t - (q - p)$ and $q' = p + t$. So $a'_k = a_k$ for $k \le p$ and $a'_{k + \delta} = a_k$ for $k > q$. $E'[0], \ldots, E'[n']$ is the true Earley chart of $w'$; we show that REPARSE returns it. The shift of an old position $i$ is $\sigma(i) = i$ if $i < q$ and $\sigma(i) = i + \delta$ if $i \ge q$. For an item, $\sigma[A \to \alpha \bullet \beta, i] = [A \to \alpha \bullet \beta, \sigma(i)]$, and $\sigma(X) = \{\sigma(I) : I \in X\}$ for a set $X$. Note that $\sigma(i) \le \sigma(i_2)$ when $i \le p$ and $q \le i_2$, and $\sigma(K) = K + \delta$ for $K \ge q$.

Fact 1 (Earley sets as least sets). For a string $u = u_1 \cdots u_m$, write $\mathrm{Scan}(X, a)$ for the set of items $[A \to \alpha a \bullet \beta, i]$ with $[A \to \alpha \bullet a \beta, i] \in X$. Given the sets $E_u[0], \ldots, E_u[j - 1]$ and a seed $X$, let $\mathrm{Cl}_j(X)$ be the least set $Y \supseteq X$ such that (P) if $[A \to \alpha \bullet B \beta, i] \in Y$ with $B \in V$, then $[B \to \bullet \eta, j] \in Y$ for every $B \to \eta \in P$; and (C) if $[B \to \gamma \bullet, i] \in Y$ and $[A \to \alpha \bullet B \beta, o]$ is in $E_u[i]$ (for $i < j$) or in $Y$ (for $i = j$), then $[A \to \alpha B \bullet \beta, o] \in Y$. Then $E_u[0] = \mathrm{Cl}_0(\{[S \to \bullet \alpha, 0] : S \to \alpha \in P\})$ and $E_u[j] = \mathrm{Cl}_j(\mathrm{Scan}(E_u[j - 1], u_j))$ for $j \ge 1$. This is the set that Earley's algorithm computes for position $j$, with the nullable rule making one pass enough (see the Earley parser), and it is the set computed by EARLEY-SET at line L4. In particular $E_u[j]$ depends only on $u_1 \cdots u_j$, and every origin in $E_u[j]$ is at most $j$.

Definition (good positions). An old position $i$ is good when either (a) $i < q$ and $i \le p$, or (b) $i \ge q$, $E'[i + \delta] = \sigma(E[i])$, and every origin $o < i$ of an item of $E[i]$ is good. This is well founded, since $o < i$. For a good position of kind (a), $E'[i] = E[i]$ by Fact 1, because $w$ and $w'$ agree on their first $p \ge i$ symbols. Every origin $o$ of $E[i]$ has $o \le i$, so $o < q$ and $\sigma(o) = o$; hence $E'[\sigma(i)] = \sigma(E[i])$ for every good $i$, of either kind, and every origin of an item of $E[i]$ is good or equal to $i$.

Lemma 1 (the test). When line L7 sets $\mathrm{ANCH}[k]$ for $k \ge q'$, the set new$[k]$ equals $E'[k]$, and $\mathrm{ANCH}[k]$ is true exactly when $K = k - \delta$ is good.

Proof. By induction on $k$. Line L2 copies $E[0], \ldots, E[p]$, which equal $E'[0], \ldots, E'[p]$ by Fact 1. Each set computed at line L4 is $\mathrm{Cl}_k(\mathrm{Scan}(E'[k - 1], a'_k))$ from correct earlier sets, so it is $E'[k]$ by Fact 1. Now $k \ge q'$ gives $K \ge q$. Line L6 accepts an origin $i$ of $E[K]$ when $i < q$ and $i \le p$, which is kind (a); when $i = K$; or when $q \le i < K$ and $\mathrm{ANCH}[i + \delta]$ is true. In the last case $q' \le i + \delta < k$, so $\mathrm{ANCH}[i + \delta]$ was set earlier, and by induction it is true exactly when $i$ is good. Line L6 rejects every origin $i$ with $p < i < q$, and such an $i$ is not good. Line L7 adds the test $E'[k] = \sigma(E[K])$. Together, these are the conditions of kind (b) for $K$. $\square$

Lemma 2 (good positions propagate). If $K \ge q$ is good and $K < n$, then $K + 1$ is good.

Proof. Let $j = K + 1$ and $j' = j + \delta = \sigma(j)$, and let $\Gamma$ be the set of good positions at most $K$, together with $j$. Since $j > q$, $a'_{j'} = a_j$.

Claim A: every origin of an item of $E[j]$ is in $\Gamma$. The items of $E[j]$ with an origin in $\Gamma$ form a set that contains $\mathrm{Scan}(E[K], a_j)$, since the origins of $E[K]$ are good or equal to $K$, and $K$ is good. It is closed under (P), which adds origin $j$. It is closed under (C): for $[B \to \gamma \bullet, i]$ with $i \in \Gamma$, either $i = j$ and the new item takes its origin from an item of the set, or $i \le K$ is good and the new item takes its origin from an item of $E[i]$, which is good or equal to $i$. By Fact 1, $E[j]$ is the least such set, so all its items are in this set.

Claim B: $\sigma(E[j]) \subseteq E'[j']$. Let $Z$ be the set of items $I \in E[j]$ with $\sigma(I) \in E'[j']$. $Z$ contains the seed: an item of $\mathrm{Scan}(E[K], a_j)$ comes from $J \in E[K]$, and $\sigma(J) \in \sigma(E[K]) = E'[K + \delta]$ scans $a'_{j'} = a_j$ into $E'[j']$. $Z$ is closed under (P), because the predicted item $[B \to \bullet \eta, j]$ maps to $[B \to \bullet \eta, j']$, which (P) puts in $E'[j']$. $Z$ is closed under (C). Take $[B \to \gamma \bullet, i] \in Z$, so $i \in \Gamma$ by Claim A. If $i = j$ and the waiting item $J$ is also in $Z$, then (C) in $E'[j']$ with origin $j'$ applies to $\sigma(J)$ and gives the image of the new item. If $i \le K$ and $J \in E[i]$, then $\sigma(i) \le \sigma(K) < j'$, and (C) in $E'[j']$ reads $E'[\sigma(i)] = \sigma(E[i])$, which contains $\sigma(J)$, so it gives the image of the new item. By the leastness in Fact 1, $Z = E[j]$.

Claim C: $E'[j'] \subseteq \sigma(E[j])$. Let $W = \sigma(E[j])$. $W$ contains the new seed $\mathrm{Scan}(E'[K + \delta], a_j) = \mathrm{Scan}(\sigma(E[K]), a_j) = \sigma(\mathrm{Scan}(E[K], a_j))$. $W$ is closed under (P) at $j'$, since a prediction from $\sigma(J)$ is the image of the prediction from $J$. $W$ is closed under (C) at $j'$. Take $\sigma[B \to \gamma \bullet, i] \in W$ with $[B \to \gamma \bullet, i] \in E[j]$, so $i \in \Gamma$. If $\sigma(i) = j'$, then $i = j$, because $\sigma(i) \le \sigma(K) < j'$ for the other elements of $\Gamma$; the waiting items of $W$ are images of waiting items of $E[j]$, and (C) in $E[j]$ gives the preimage of the new item. If $\sigma(i) < j'$, then $i \le K$ is good, and (C) reads $E'[\sigma(i)] = \sigma(E[i])$; its waiting items are images of waiting items of $E[i]$, and (C) in $E[j]$ again gives the preimage. By the leastness in Fact 1, $E'[j'] \subseteq W$.

So $E'[j + \delta] = \sigma(E[j])$, $j \ge q$, and every origin $o < j$ of $E[j]$ is in $\Gamma \setminus \{j\}$, so it is good. Hence $j$ is good. $\square$

Theorem. REPARSE$(G, w, E, p, q, v)$ terminates and returns $w'$ and the Earley chart $E'[0], \ldots, E'[n']$ of $w'$. Hence line L12 returns true if and only if $S \Rightarrow^* w'$.

Proof. The loop of line L3 runs at most $n' - p + 1$ times, and each step ends, so the call terminates. Line L1 builds $w'$. By Lemma 1, the sets that lines L2 and L4 build are $E'[0], \ldots, E'[k]$ when the loop reaches $k$. If line L8 never finds an anchored set, the loop computes every set at line L4, and line L11 returns $E'$. Otherwise line L8 stops at some $k \ge q'$ with $\mathrm{ANCH}[k]$ true, so $K = k - \delta$ is good by Lemma 1. By Lemma 2 and induction, every position $j$ with $K \le j \le n$ is good, so $E'[j + \delta] = \sigma(E[j])$. These are the sets that line L9 adds for the positions $k + 1, \ldots, n'$, and line L10 returns $E'$. The last claim follows from the correctness of Earley's algorithm: $S \Rightarrow^* w'$ if and only if some $[S \to \alpha \bullet, 0]$ is in $E'[n']$. $\blacksquare$