Изменения

Для всех наборов <tex>\tau = \langle \alpha, \beta, \gamma, \delta, A, i , j \rangle</tex> нужно доказать, что, если <tex> S' \Rightarrow^* \gamma A \delta, \gamma \Rightarrow^* a_1...a_{i}, (A \rightarrow \alpha \beta) \in P, \alpha \Rightarrow^* a_{i+1}...a_{j}</tex>, то алгоритм добавит <tex> [A \rightarrow \alpha \cdot \beta, i]</tex> в <tex> I_{j}</tex>. ''Рангом набора'' <tex> \tau </tex> называется <tex> \tau_{S'}(\tau) + 2(j + \tau_{\gamma}(\tau) + \tau_{\alpha}(\tau))</tex>, где <tex>\tau_{S'}(\tau)</tex> — длина кратчайшего вывода <tex>S' \Rightarrow^* \gamma A \delta </tex>, <tex>\tau_{\gamma}(\tau)</tex> — длина кратчайшего вывода <tex>\gamma \Rightarrow^* a_1...a_{i}</tex>, <tex>\tau_{\alpha}(\tau)</tex> — длина кратчайшего вывода <tex>\alpha \Rightarrow^* a_{i+1}...a_{j}</tex>. Докажем утверждение индукцией по рангу набора.<br/>База: если ранг <tex>\tau</tex> равен 0, то <tex>\tau_{S'} = \tau_{\gamma} = \tau_{\alpha} = j = i = 0</tex>. Значит, <tex>A = S'a</tex>, тогда <tex>\alpha = \gamma a = \delta = \varepsilon </tex>, <tex>\beta = S </tex>. При инициализации такая ситуация <tex>[S' \rightarrow \cdot S, 0]</tex> будет добавлена в <tex>I_0</tex>.<br/>Индукционный переход:пусть ранг <tex>\tau</tex> равен <tex>r > 0</tex>, пусть для всех наборов с меньшими рангами утверждение верно. Докажем для набора <tex>\tau</tex>. Для этого рассмотрим три случая: 1. <tex>\alpha</tex> оканчивается терминалом.<br/><tex>\alpha = \alpha' c</tex>. <tex>\alpha \Rightarrow^*a_{i+1}...a_{j}</tex>, значит <tex>c = a_{j}</tex>. Рассмотрим набор <tex>\tau' = \langle \alpha', a_{j} \beta, \gamma, \delta, A, i, j-1 \rangle </tex>. <tex>(A \rightarrow \alpha' a_{j} \beta) \in P</tex>, следовательно ранг <tex>\tau'</tex> равен <tex>r - 2</tex>, так как <tex>\tau_{S'}(\tau) = \tau_{S'}(\tau'), \tau_{\gamma}(\tau) = \tau_{\gamma}(\tau'), \tau_{\alpha}(\tau) = \tau_{\alpha}(\tau')</tex>. Значит, по предположению <tex>[A \rightarrow \alpha' \cdot a_{j} \beta, i] \in I_w_{j-1}</tex>, и <tex>[A \rightarrow \alpha \cdot \beta, i] </tex> будет добавлена в <tex>I_{j}</tex> по правилу <tex>(1)</tex>. 2. <tex>\alpha</tex> оканчивается нетерминалом.<br/> <tex>\alpha = \alpha' B</tex>. <tex>\alpha \Rightarrow^*a_{i+1}w_i...a_{j}</tex>, значит <tex>\mathcal {9} k</tex> такое, что <tex>\alpha' \Rightarrow^*a_{i+1}...a_{k}, B \Rightarrow^* a_{k+1}...a_w_{j-2}</tex>.<br/>Рассмотрим набор <tex>\tau' = \langle \alpha', B \beta, \gamma, \delta, A, i, k \rangle</tex>, его ранг меньше <tex>r</tex>, следовательно По предположению индукции: <tex>[A \rightarrow \alpha' \cdot B a \beta, i] \in I_{k}</tex> по предположению.<br/>Пусть <tex>B \Rightarrow \eta</tex> — первый шаг в кратчайшем выводе <tex>B \Rightarrow^* a_{k+1}...a_D_{j}</tex>. Рассмотрим набор <tex>\tau'' = \langle \eta, \varepsilon, \gamma \alpha', \beta \delta, B, k, j \rangle</tex>. <tex>S \Rightarrow^* \gamma A \delta \Rightarrow \gamma \alpha' B \beta \delta</tex>, следовательно <tex>\tau_{S'}(\tau'') \leqslant \tau_{S'}(\tau) + -1</tex>.<br> Пусть длина кратчайшего вывода <tex>\alpha' \Rightarrow^*a_{i+1}...a_{k}</tex> равна <tex>n_1</tex>, а длина кратчайшего вывода <tex> B \Rightarrow^* a_{k+1}...a_{j}</tex> равна <tex>n_2</tex>. Тогда <tex>\tau_{\alpha}(\tau) = n_1 + n_2</tex>. Так как <tex> B \Rightarrow \eta \Rightarrow^* a_{k+1}...a_{j}</tex>, то <tex>\tau_{\alpha}(\tau'') = n_2 - 1</tex>. Очевидно, что <tex>\tau_{\gamma}(\tau'') = \tau_{\gamma}(\tau) + n_1</tex>. Тогда ранг <tex>\tau''</tex> равен <tex>\tau_{S'}(\tau'') + 2(\tau_{\gamma}(\tau'') + \tau_{\alpha}(\tau'') + j) \leqslant \tau_{S'}(\tau) + 1 + 2(\tau_{\gamma}(\tau) + n_1 + n_2 - 1 + j)</tex> <tex>= \tau_{S'}(\tau) - 1 + 2(\tau_{\gamma}(\tau) + \tau_{\alpha}(\tau) + j) < r</tex>. Значит, отсюда по предположению для <tex>\tau''</tex>, правилу <tex>[B \rightarrow \eta \cdot, k] \in I_mathtt{jscan}</tex>. Из того, что получаем <tex>[A \rightarrow \alpha' a \cdot B \beta, i] \in I_{k}</tex> и <tex>[B \rightarrow \eta \cdot, k] \in I_{j}</tex>, по правилу <tex>(2)</tex> <tex>[A \rightarrow \alpha \cdot \beta, i] </tex> будет добавлена в <tex>I_D_{j}</tex>.