Бюрократы, editor, Администраторы
422
правки
Изменения
Быстрофикс по результатам обдумывания во сне
Для простоты добавим новый стартовый вспомогательный нетерминал <tex>S'</tex> и правило <tex>S' \rightarrow S</tex>.
<tex>I_0</tex> ∪= <tex>[S' \rightarrow \cdot S, 0]</tex># Правило (0) — инициализация
useful_loop(0)
function useful_loop(j):
do for <tex>[B \rightarrow \eta \cdot , i] \in I_j</tex> for <tex>[A \rightarrow \alpha \cdot B \beta, k] \in I_{i}</tex> <tex>I_j</tex> ∪= <tex>[A \rightarrow \alpha B \cdot \beta, k]</tex> # Правило (2)
==Корректность алгоритма==
{{Теорема
|statement = Приведенный алгоритм включает в правильно строит все списки нужные ситуации и только ихситуаций.
|proof =
=====Алгоритм не добавит в список ситуацию, которая ему не принадлежит:=====
Докажем индукцией по индукцииисполнению алгоритма.<br/>База: (инициализация) : <tex>\alpha = \varepsilon \Rightarrow^* \varepsilon </tex> и <tex>S' \Rightarrow^* \gamma S \delta </tex> при <tex>\gamma = \delta = \varepsilon </tex>.<br/>Индукционный переход: пусть верно для всех ситуаций из списков в <tex> I_{i0}, i \leqslant ...,I_{j } </tex>нет лишних ситуаций. Пусть включаем <tex>[A \rightarrow \alpha \cdot \beta, i] </tex> в <tex>I_{j}</tex>. Рассмотрим три случая:
1. Пусть включаем Включаем по правилу 1.<br/>
Тогда <tex>\alpha = \alpha' a_{j} , [A \rightarrow \alpha' \cdot a_{j} \beta, i] \in I_{j-1}</tex>. По предположению, <tex>\alpha' \Rightarrow^* a_{i+1}...a_{j-1} </tex> и существуют <tex>\gamma'</tex> и <tex>\delta' </tex> такие, что <tex>S' \Rightarrow^* \gamma' A \delta', \gamma' \Rightarrow^* a_1...a_{i} </tex>. Значит, <tex> \alpha = \alpha' a_{j} \Rightarrow^* a_{i+1}...a_{j} </tex> и при <tex>\gamma = \gamma', \delta = \delta'</tex> <tex>[A \rightarrow \alpha \cdot \beta, i] \in I_j</tex>.
2. Пусть включаем Включаем по правилу 2.<br/>
Тогда <tex>\alpha = \alpha' B , [A \rightarrow \alpha' \cdot B \beta, k] \in I_{i}</tex> и <tex> [B \rightarrow \eta \cdot, i] \in I_{j} </tex>. По предположению, <tex>\alpha' \Rightarrow^* a_{k+1}...a_{i}, \eta \Rightarrow^* a_{i+1}...a_{j} </tex>, откуда <tex>\alpha = \alpha' B \Rightarrow^*a_{k+1}...a_{j} </tex>. Кроме того, существуют <tex>\gamma'</tex> и <tex>\delta' </tex> такие, что <tex>S' \Rightarrow^* \gamma' A \delta', \gamma' = a_1...a_{k} </tex>. Значит, при <tex>\gamma = \gamma', \delta = \delta'</tex> <tex>[A \rightarrow \alpha \cdot \beta, i] \in I_j</tex>.
3. Пусть включаем Включаем по правилу 3.<br/>
Тогда <tex>\alpha = \varepsilon, i = j, [B \rightarrow \alpha' \cdot A \eta, k] \in I_{j}, A \Rightarrow \beta</tex>. По предположению <tex>\alpha' \Rightarrow^* a_{k+1}...a_{i}</tex> и существуют <tex>\gamma'</tex> и <tex>\delta' </tex> такие, что <tex>S' \Rightarrow^* \gamma' B \delta', \gamma' \Rightarrow^* a_1...a_{k} </tex>. Значит, при <tex>\gamma = \gamma' \alpha', \delta = \eta \delta' </tex> выполнено <tex> S' \Rightarrow^* \gamma A \delta</tex>, следовательно <tex>[A \rightarrow \alpha \cdot \beta, i] \in I_j</tex>.
