69
правок
Изменения
Нет описания правки
{{Теорема
|statement = Приведенный алгоритм правильно строит все списки ситуаций.
То есть алгоритм поддерживает инвариант <tex> [A \rightarrow \alpha \cdot \beta, i] \in D_{j} \Longleftrightarrow \exists \delta \in \Sigma \cup N : ((S ' \Rightarrow^* w_0...w_{i-1} A \delta) \wedge A \Rightarrow^* w_i...w_{j-1})</tex>
|proof =
1. Включаем по правилу <tex> \mathtt{scan}</tex>.<br/>
Это произошло, если <tex> \alpha = \alpha ' a</tex>, <tex>a = w_{j-1}</tex> и <tex> [A \rightarrow \alpha ' \cdot a \beta, i] \in D_{j-1}</tex>.<br/>
По предположению индукции <tex>S ' \Rightarrow^* w_0...w_{i-1} A \delta</tex> и <tex>\alpha' \Rightarrow^* w_i...w_{j-2}</tex>,<br/>
тогда в силу <tex>a = w_{j-1}</tex> получаем <tex>\alpha = \alpha ' a \Rightarrow^* w_i...w_{j-2}w_{j-1} = w_i...w_{j-1}</tex>.<br/>
Таким образом условия: <tex>S ' \Rightarrow^* w_0...w_{i-1} A \delta</tex> и <tex>\alpha \Rightarrow^* w_i...w_{j-1}</tex> выполняются.
2. Включаем по правилу <tex> \mathtt{predict}</tex>.<br/>
По построению: <tex> \alpha = \varepsilon </tex> и <tex>i=j</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...w_{i'-1} A' \delta ''</tex>
и <tex> \alpha ' \Rightarrow^* w_{i'}...w_{i-1}</tex>.<br/>
Получаем, что <tex>S ' \Rightarrow^* w_0...w_{i'-1} A' \delta ''</tex>, значит <tex>S \Rightarrow^* w_0...w_{i'-1} \alpha' A \delta' \delta '' </tex>, следовательно <tex> S ' \Rightarrow^* w_0...w_{i'-1} w_{i'}...w_{i-1} A \delta' \delta ''</tex>, в итоге <tex> S ' \Rightarrow^* w_0...w_{i-1} A \delta</tex>, что нам и требовалось.
3. Включаем по правилу <tex> \mathtt{complete}</tex>.<br/>
=====<tex>\Longleftarrow</tex>=====
В обратную сторону будем доказывать индукцией по суммарной длине вывода <tex>w_0...w_{i-1} A \delta</tex> из <tex>S'</tex> и <tex>w_i...w_{j-1}</tex> из <tex>\alpha</tex>. После чего примениминдукцию по длине вывода <tex>w_i...w_{j-1}</tex> из <tex>\alpha</tex>.<br/>
Рассмотрим три случая последнего символа <tex>\alpha</tex>:
1. <tex>\alpha = \alpha ' a</tex>, тогда <tex>a = w_{j-1}</tex> и <tex>\alpha ' \Rightarrow^* w_i...w_{j-2}</tex>.<br/>
По предположению индукции: <tex>[A \rightarrow \alpha ' \cdot a \beta, i] \in D_{j-1}</tex>, а отсюда по правилу <tex> \mathtt{scan}</tex> получаем <tex>[A \rightarrow \alpha ' a \cdot \beta, i] \in D_{j}</tex>.
2. <tex>\alpha = \alpha ' B</tex>, тогда <tex>\exists i' : \alpha ' \Rightarrow^* w_i...w_{i'-1} \wedge B ' \Rightarrow^* w_{i'}...w_{j-1}</tex>.<br/>
Тогда имеем <tex>[A \rightarrow \alpha ' a \cdot \beta, i] \in D_{j}</tex>. Также можно записать <tex>S' \Rightarrow^* w_0...w_{i-1} A \delta</tex>, как <tex>S' \Rightarrow^* w_0...w_{i-1} w_i...w_{i'-1}B \beta \delta</tex>,
а также <tex>B \rightarrow \eta \wedge \eta \rightarrow w_{i'}...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>.
3. <tex>\alpha = \varepsilon </tex>, тогда <tex>i=j</tex>.<br/>
Тогда либо <tex>i = 0 \wedge A = S \wedge \delta = \varepsilon</tex>, что доказывает базу индукции,<br/>
либо вывод можно записать в виде <tex>S' \Rightarrow^* w_0...w{i'-1}w_{i'}...w{i-1} A \delta ' \delta '' = w_0...w_{i-1} A \delta</tex> для некоторого правила <tex>(A' \rightarrow w_{i'}...w_{i-1} A \delta ') \in P</tex>. <br/>
Отсюда по предположению индукции <tex>[A' \rightarrow \cdot w_{i'}...w_{i-1} A \delta ', i'] \in D_{i'}</tex>,
что после нескольких применений правила <tex> \mathtt{scan}</tex> приводит к <tex>[A' \rightarrow w_{i'}...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>, что и требовалось.
}}
