Изменения
Нет описания правки
положить <tex>N'=N</tex> и <tex>S'=S</tex>.
(4) Положить <tex> G'=(N',\Sigma, P', S')</tex>. <tex>\Box</tex>
Для доказательства корректности нам понадобиться следующее утверждение:
{{Утверждение
|statement= <tex>A \overset{*}{\underset{G'}{\Rightarrow}}w</tex> <tex>(A \ne S')</tex> тогда и только тогда, когда <tex>A \overset{*}{\underset{G}{\Rightarrow}}w</tex> и <tex>w \ne \varepsilon</tex>
|proof=
<tex>\Rightarrow</tex><br\>
Пусть <tex>A \overset{*}{\underset{G'}{\Rightarrow}}w</tex>. Несомненно, <tex>w \ne \varepsilon</tex>, поскольку <tex>G'</tex> - грамматика без <tex>\varepsilon</tex>-правил и <tex>A \ne S'</tex>.<br/>Докажем индукцией по длине порождения, что <tex>A \overset{*}{\underset{G}{\Rightarrow}}w</tex>.<br/>
Обозначим длину порождения за <tex>p</tex>.
:'''Базис'''. <tex>p = 1</tex><br/>
В этом случае в <tex>G'</tex> есть правило <tex>A \rightarrow w</tex>. Согласно конструкции <tex>G'</tex> в <tex>G</tex> есть правило <tex>A \rightarrow \alpha</tex>, причем <tex>\alpha-</tex> это <tex>w</tex>, символы которой, возможно, перемежаются <tex>\varepsilon-</tex> порождающими переменными. Тогда в <tex>G</tex> есть порождения <tex>A \underset{G}{\Rightarrow} \alpha \overset{*}{\underset{G}{\Rightarrow}}w</tex>, где на шагах после первого, из всех переменных в цепочке <tex>\alpha</tex> выводиться <tex>\varepsilon</tex>.<br/>
:'''Предположение'''. Пусть <tex>[A \overset{*}{\underset{G'}{\Rightarrow}}w</tex> <tex>(A \ne S')]</tex> <tex>\Rightarrow [A \overset{*}{\underset{G}{\Rightarrow}}w</tex> и <tex>w \ne \varepsilon]</tex> верно для <tex>p < n</tex>.<br/>
:'''Переход'''. <tex>p = n</tex><br/>
Пусть в порождении <tex>n</tex> шагов, <tex>n > 1</tex>. Тогда оно имеет вид <tex>A\underset{G'}{\Rightarrow}X_1 X_2...X_k
\overset{*}{\underset{G'}{\Rightarrow}}w</tex>, где <tex>X_i \in N \cup \Sigma </tex>. Первое использованное правило должно быть построено по правилу <tex>A \rightarrow Y_1 Y_2...Y_m</tex>, где цепочка <tex>Y_1 Y_2...Y_m</tex> совпадает с цепочкой <tex>X_1 X_2...X_k</tex>, цепочка <tex>Y_1 Y_2...Y_m</tex>, возможно, перемежаются <tex>\varepsilon-</tex> порождающими переменными.<br/>
Цепочку <tex>w</tex> можно разбить на <tex>w_1 w_2...w_k</tex>, где <tex>X_i \overset{*}{\underset{G'}{\Rightarrow}}w_i</tex>. Если <tex>X_i</tex> есть терминал, то <tex>w = X_i</tex>, a если переменная, то порождение <tex>X_i \overset{*}{\underset{G'}{\Rightarrow}}w_i</tex> содержит менее <tex>n</tex> шагов.<br/> По предположению <tex>X_i \overset{*}{\underset{G}{\Rightarrow}}w_i</tex>.<br/>
Теперь построим соответствующее порождение в <tex>G</tex>.<br/>
:<tex>A \underset {G}{\Rightarrow} Y_1 Y_2...Y_m \overset{*}{\underset{G}{\Rightarrow}} X_1 X_2...X_k \overset{*}{\underset{G}{\Rightarrow}} w_1 w_2...w_k = w</tex><br/>
Ч.т.д.<br/>
<tex>\Leftarrow</tex><br/>
Пусть <tex>A \overset{*}{\underset{G}{\Rightarrow}}w</tex> и <tex>w \ne \varepsilon</tex>.<br/>
Докажем индукцией по длине порождения, что <tex>A \overset{*}{\underset{G'}{\Rightarrow}}w</tex>.<br/>
Обозначим длину порождения за <tex>p</tex>.<br/>
:'''Базис'''. <tex>p = 1</tex><br/>
<tex>A \rightarrow w</tex> является правилом в <tex>G</tex>. Поскольку <tex>w \ne \varepsilon</tex>, эта же правило будет и в <tex>G'</tex>, поэтому <tex>A \overset{*}{\underset{G'}{\Rightarrow}}w</tex>.
:'''Предположение'''. Пусть <tex>[A \overset{*}{\underset{G}{\Rightarrow}}w</tex> и <tex>w \ne \varepsilon] \Rightarrow [A \overset{*}{\underset{G'}{\Rightarrow}}w (A \ne S')]</tex> верно для <tex>p < n</tex>.<br/>
:'''Переход'''. <tex>p = n</tex><br/>
Пусть в порождении <tex>n</tex> шагов, <tex>n > 1</tex>. Тогда оно имеет вид <tex>A\underset{G}{\Rightarrow}Y_1 Y_2...Y_m
\overset{*}{\underset{G}{\Rightarrow}}w</tex>, где <tex>Y_i \in N \cup \Sigma </tex>. Цепочку <tex>w</tex> можно разбить на <tex>w_1 w_2...w_m</tex>, где <tex>Y_i \overset{*}{\underset{G'}{\Rightarrow}}w_i</tex>.<br/>
Пусть <tex>X_1, X_2, ... X_k</tex> будут теми из <tex>Y_j</tex>(в порядке записи), для которых <tex>w_i \ne \varepsilon</tex>. <tex>k \ge 1</tex>, поскольку <tex>w \ne \varepsilon</tex>.<br/> Таким образом <tex>A \rightarrow X_1 X_2 ... X_k</tex> является правилом в <tex>G'</tex> по построению <tex>G'</tex>.
Утверждаем, что <tex> X_1 X_2...X_k \overset{*}{\underset{G}{\Rightarrow}}w</tex>, поскольку только <tex>Y_j</tex>, которых нет среди <tex>X_1, X_2, ... X_k</tex>, использованы для порождения <tex>\varepsilon</tex> и не вносят ничего в порождение <tex>w</tex>.
Так как каждое из порождений <tex>Y_j \overset{*}{\underset{G}{\Rightarrow}}w_j</tex> содержит менее <tex>n</tex> шагов, к ним можно применить предположение индукции и заключить, что если <tex>w_j \ne \varepsilon</tex>, то <tex>Y_j \overset{*}{\underset{G'}{\Rightarrow}}w_j</tex>.<br/>
Таким образом <tex>A \underset{G'}{\rightarrow} X_1 X_2 ... X_k \overset{*}{\underset{G'}{\Rightarrow}} w</tex>.<br/>
Ч.т.д.
}}
Теперь можно доказать корректность:
{{Утверждение
|statement=Алгоритм корректен: <tex>L(G)=L(G')</tex>
|proof=
Подставив <tex>S</tex> вместо <tex>A</tex> в утверждении выше, видим, что <tex>w \in L(G)</tex> для <tex>w \ne \varepsilon</tex> тогда и только тогда, когда <tex>w \in L(G')</tex>.<br/> Очевидно, что <tex>\varepsilon \in L(G)</tex> тогда и только тогда, когда <tex>\varepsilon \in L(G')</tex>.<br/> Таким образом, <tex>L(G)=L(G')</tex>.
}}
== Литература ==
* Ахо Альфред, Джеффри Ульман. Теория Синтаксического Анализа, Перевода и Компиляции. Том 1.
* Джон Хопкрофт, Раджив Мотвани, Джеффри Ульман. Введение в теорию автоматов, языков и вычислений.
