Изменения

Пусть <tex>G = \langle N, \Sigma, P, S \rangle</tex> {{---}} [[Контекстно-свободные грамматики, вывод, лево- и правосторонний вывод, дерево разбора|контекстно-свободная]] грамматика и <tex>w = w_0 w_1 ... \ldots w_{n-1}</tex> {{---}} входная цепочка из <tex>\Sigma^*</tex>.

Ситуации хранятся в множествах <tex>D_0,...\ldots ,D_{n-1}</tex>, называемых '''списками ситуаций'''. Причем наличие ситуации <tex>[A \rightarrow \alpha \cdot \beta , i]</tex> в <tex>j</tex>-м списке ситуаций <tex>D_j</tex> равносильно тому, что <tex>\exists \delta \in \Sigma \cup N : ((S' \Rightarrow^* w_0...\ldots w_{i-1} A \delta) \wedge A \Rightarrow^* w_i...\ldots w_{j-1})</tex>.

Последовательность списков ситуаций <tex>D_0, D_1, ..\ldots, D_{n-1}\ </tex> называется <b>списком разбора</b> для входной цепочки <tex>w</tex>.

# Если <tex>[B \rightarrow \eta \ \cdot, i] \in D_j</tex> и <tex>[A \rightarrow \alpha \cdot B \beta, k] \in D_i</tex>, то <tex>[A \rightarrow \alpha B \cdot \beta, k] \in D_j</tex>.# Если <tex>[A \rightarrow \alpha \ \cdot B \beta, i] \in D_{j} </tex> и <tex>(B \rightarrow \eta) \in P </tex>, то <tex>[B \rightarrow \cdot \ \eta, j] \in D_{j}</tex>.

<tex> D_{0} = \lbrace [S' \rightarrow \cdot \ S, 0] \rbrace </tex> '''for''' <tex>i = 1</tex> '''to''' <tex>len(w) - 1</tex>

'''for''' <tex>j = 0</tex> '''to''' <tex>len(w) - 1</tex>

'''if''' <tex>[S' \rightarrow S \ \cdot, 0] \in D_{len(w)} </tex>

<tex>D_{j}</tex> <tex> \cup</tex>= <tex>[A \rightarrow \alpha a \cdot a \beta, i]</tex> <font color=green>// Второе правило </font>

'''for''' <tex>[B \rightarrow \eta \ \cdot, i] \in D_{j} </tex> '''for''' <tex>[A \rightarrow \alpha \cdot B \beta, kj] \in D_{i} </tex> <tex>D_{j}</tex> <tex> \cup</tex>= <tex>[A \rightarrow \alpha B \cdot \beta, kj]</tex>

<tex>D_{j}</tex> <tex>\cup</tex>= <tex>[B \rightarrow \cdot \ \eta, j]</tex>

То есть алгоритм поддерживает инвариант <tex> [A \rightarrow \alpha \cdot \beta, i] \in D_{j} \Longleftrightarrow \exists \delta \in \Sigma \cup N : ((S' \Rightarrow^* w_0...\ldots w_{i-1} A \delta) \wedge A \Rightarrow^* w_i...\ldots w_{j-1})</tex>

<tex>[S' \rightarrow \cdot S, 0] \in D_0\ </tex>.<br/>

1. Включаем по правилу <tex> \mathtt{scan}\ </tex>.<br/>

По предположению индукции <tex>S' \Rightarrow^* w_0...\ldots w_{i-1} A \delta</tex> и <tex>\alpha' \Rightarrow^* w_i...\ldots w_{j-2}</tex>,<br/> тогда в силу <tex>a = w_{j-1}</tex> получаем <tex>\alpha = \alpha ' a \Rightarrow^* w_i...\ldots w_{j-2}w_{j-1} = w_i...\ldots w_{j-1}\ </tex>.<br/>Таким образом условия: <tex>S' \Rightarrow^* w_0...\ldots w_{i-1} A \delta</tex> и <tex>\alpha \Rightarrow^* w_i...\ldots w_{j-1}</tex> выполняются.

2. Включаем по правилу <tex> \mathtt{predict}\ </tex>.<br/>

Кроме того <tex>\exists i' \le i</tex> и ситуация <tex>[A' \rightarrow \alpha ' \cdot A \delta ', i'] \in D_i</tex>, из чего по предположению индукции следует <tex>S' \Rightarrow^* w_0...\ldots w_{i'-1} A' \delta ''</tex> и <tex> \alpha ' \Rightarrow^* w_{i'}...\ldots w_{i-1}</tex>.<br/>Получаем, что <tex>S' \Rightarrow^* w_0...\ldots w_{i'-1} A' \delta ''</tex>, значит <tex>S \Rightarrow^* w_0...\ldots w_{i'-1} \alpha' A \delta' \delta '' </tex>, следовательно <tex> S' \Rightarrow^* w_0...\ldots w_{i'-1} w_{i'}...\ldots w_{i-1} A \delta' \delta ''</tex>, в итоге <tex> S' \Rightarrow^* w_0...\ldots w_{i-1} A \delta</tex>, что нам и требовалось.

3. Включаем по правилу <tex> \mathtt{complete}\ </tex>.<br/>

Cледовательно <tex>\alpha = \alpha ' A' \Rightarrow^* w_i...\ldots w_{i'-1} w_{i'}...\ldots w_{j} = w_i...\ldots w_{j-1}</tex>, что дает нам второй пункт утверждения, а так как первый пункт следует из индукционного предположения, все хорошо.

В обратную сторону будем доказывать индукцией по суммарной длине вывода <tex>w_0...\ldots w_{i-1} A \delta\ </tex> из <tex>S'</tex> и <tex>w_i...\ldots w_{j-1}</tex> из <tex>\alpha</tex>. После чего примениминдукцию по длине вывода <tex>w_i...\ldots w_{j-1}</tex> из <tex>\alpha</tex>.<br/>

1. <tex>\alpha = \alpha ' a</tex>, тогда <tex>a = w_{j-1}</tex> и <tex>\alpha ' \Rightarrow^* w_i...\ldots w_{j-2}</tex>.<br/>

2. <tex>\alpha = \alpha ' B</tex>, тогда <tex>\exists i' : \alpha ' \Rightarrow^* w_i...\ldots w_{i'-1} \wedge B ' \Rightarrow^* w_{i'}...\ldots w_{j-1}</tex>.<br/>Тогда имеем <tex>[A \rightarrow \alpha ' a \cdot \beta, i] \in D_{j}</tex>. Также можно записать <tex>S' \Rightarrow^* w_0...\ldots w_{i-1} A \delta</tex>, как <tex>S' \Rightarrow^* w_0...\ldots w_{i-1} w_i...\ldots w_{i'-1}B \beta \delta</tex>,а также <tex>B \rightarrow \eta \wedge \eta \rightarrow w_{i'}...\ldots w_{j-1}</tex>.<br/>Применяя индукцию по второму параметру получим <tex>[B \rightarrow \eta \cdot, i'] \in D_j\ </tex>, откуда по правилу <tex> \mathtt{complete}</tex> получаем <tex>[A \rightarrow \alpha ' B \cdot \beta, i] \in D_{j}</tex>.

либо вывод можно записать в виде <tex>S' \Rightarrow^* w_0...\ldots w{i'-1}w_{i'}...\ldots w{i-1} A \delta ' \delta '' = w_0...\ldots w_{i-1} A \delta\ </tex> для некоторого правила <tex>(A' \rightarrow w_{i'}...\ldots w_{i-1} A \delta ') \in P</tex>. <br/>Отсюда по предположению индукции <tex>[A' \rightarrow \cdot w_{i'}...\ldots w_{i-1} A \delta ', i'] \in D_{i'}\ </tex>, что после нескольких применений правила <tex> \mathtt{scan}</tex> приводит к <tex>[A' \rightarrow w_{i'}...\ldots w_{i-1} \cdot A \delta ', i'] \in D_{i}\ </tex>,после чего по правилу <tex> \mathtt{predict}\ </tex> получим <tex>[A \rightarrow \cdot \beta, i] \in D_{j}\ </tex>, что и требовалось.