Изменения

[[Нормальная форма ДМП-автомата|Предположим детерминированный строгий автомат с единственным состоянием с элементами, представленный тройкой]]: * входной алфавит на ленте <tex>\Sigma</tex>, * стековым алфавит <tex>\Gamma</tex> и ,* множеством переходов <tex>\Delta</tex>. Мы предполагаем наличие полного порядка на <tex>\Sigma</tex>,и говорим, что слово <tex>u</tex> короче слова <tex>v</tex> если <tex>|u| < |v|</tex> или <tex>|u| = |v|</tex> и <tex>u</tex> лексикографически меньше <tex>v</tex>. Пусть <tex>E, F, G,\dotsc</tex> {{--- }} допустимые конфигурации.

|definition=<tex>E \cdot u</tex> - конфигурация '''Конфигурация <tex>E</tex> после слова <tex>u</tex>''', обозначается <tex>E \cdot u</tex> {{---}} единственная допустимая конфигурация <tex>F</tex> такая что <tex>(E, u) \rightarrow F</tex>, которая может быть и <tex>\emptyset</tex>.

|definition='''Язык, задаваемой конфигурацией <tex>E</tex>, ''' {{---}} <tex>L(E) = \{ E : \mid (E \cdot u) = \varepsilon \}</tex>.

|definition=<tex>E \sim F</tex> - две Две конфигурации <tex>E</tex> и <tex>F</tex> '''эквивалентны''' если {{---}} <tex>L(E) = L(F)</tex>, обозначается <tex>E \sim F</tex>.

|definition=Конфигурафии <tex>E \sim_n F, n \geq 0</tex> - конфигурафии и <tex>EF</tex> и '''<tex>Fn</tex> -эквивалентны''', обозначается <tex>E \sim_n F, n\geqslant 0</tex>{{-эквивалентны''' если --}} они принимают одни и те же слова, длина которых не больше <tex>n</tex>:<br>для всех слов <tex>w</tex>, таких что <tex>|w| \leq leqslant n, (E \cdot w) = \varepsilon</tex> тогда и только тогда, когда <tex>(F \cdot w) = \varepsilon</tex>.

# <tex>E \sim F</tex> тогда и только тогда, когда для любого <tex> n \geq geqslant 0</tex> выполняется <tex>E \sim_n F</tex>.# Если <tex>E \nsim F</tex>, то существует <tex> n \geq geqslant 0</tex> такой, что <tex>E \sim_n F</tex> и <tex>E \nsim_{n+1} F</tex>.

# <tex>E \sim_{n} F</tex>, тогда и только тогда, когда для любого <tex>u \in \Sigma^*</tex>, где <tex>|u| \leq leqslant n</tex>, <tex>(E \cdot u) \sim_{n-|u|} (F \cdot u)</tex>.# Если <tex>E \sim_{n} F</tex> и <tex>0 \leq leqslant m < n</tex>, то <tex>E \sim_{m} F</tex>.

|definition=Для каждого стекового символа <tex>X</tex> '''словом <tex>w(X)</tex> ''' называется самое короткое слово в множестве <tex>\{u : \mid (X \cdot u) = \varepsilon \}</tex>.

|definition=<tex>E = E_1G_1 + ... \ldots + E_nG_n</tex> находится в '''форме голова/хвост''', если голова <tex>E_1 + ... \ldots +E_n</tex> допустима и хотя бы один <tex>E_i= \emptyset</tex>, и каждый хвост <tex>G_i = \emptyset</tex>.

Приведём некоторые свойства формы голова/хвост. Эквивалентность и n-эквивалентность языков согласуются с операциями <tex>+n</tex> и -эквивалентность языков согласуются с операцией суммы. Следовательно, форма голова/хвост позволяет подставить эквивалентное выражение в хвост (т.к. допустимость сохраняется).

Пусть <tex>E = E_1G_1 + ... \ldots + E_nG_n</tex>, тогда справедливы следующие факты:# Если <tex>(E_i \cdot u) = \varepsilon</tex>, то для всех <tex>j \neq i</tex> выполняется <tex>(E_j \cdot u) = \emptyset</tex> и <tex>(E \cdot u) = G_i</tex>.# Если <tex>(E_i \cdot u) = \emptyset</tex>, то <tex>(E \cdot u) = (E_1 \cdot u)G_1 + ... \ldots + (E_n \cdot u)G_n</tex>.# Если <tex>H_i \neq \emptyset, 1 \leq leqslant i \leq leqslant n</tex>, то <tex>E_1H_1 + ... \ldots + E_nH_n</tex> в форме голова/хвост.# Если каждая <tex>H_i \neq \emptyset</tex> и каждая <tex>E_i \neq \varepsilon</tex> и для каждого <tex>j</tex> такого, что <tex>E_j \neq \emptyset</tex> выполняется <tex>H_j \sim_m G_j</tex>, то <tex>E \sim{m+1} E_1H_1 + ... \ldots + E_nH_n</tex>.# Если <tex>H_i \sim G_i, 1 \leq leqslant i \leq leqslant n</tex>, то <tex>E \sim E_1H_1 + ... \ldots + E_nH_n</tex>.

Две конфигурации могут иметь одинаковые головы и разные хвосты, или одинаковые хвосты и различие в головах. Если <tex>E</tex> представлена в форме голова/хвост<tex>E_1G_1 + ... \ldots + E_nG_n</tex> и <tex>F</tex> имеет схожую форму голова/хвост <tex>F_1G_1 + ... \ldots + E_nF_n</tex>, имеющая тот же самый хвост. Несоответствие между <tex>E</tex> и <tex>F</tex>, соответственное этому представлению {{--- }} это <tex>max\max_{1 \leqslant i \leqslant n} \{|E_i|, |F_i| : 1 \leq i \leq n\}</tex>. Если несоответствие равно 0, то конфигурации одинаковы.

|definition= Если <tex>E = E_1G_1 + ... \ldots + E_nG_n</tex> и <tex>F = F_1F_1 + ... \ldots + F_nF_n</tex>, тогда <tex>F</tex> в его форме голова/хвост {{- --}} '''хвостовое дополнение <tex>E</tex>''' в его форме голова/хвост обеспечивается <tex>H_i = K^i_1G_1 + ... \ldots + K^i_nG_n, 1 \leq leqslant i \leq leqslant m</tex>. Когда <tex>F</tex> {{--- }} хвостовое дополнение <tex>E</tex>, относящиеся к нему дополнение <tex>e</tex> {{--- }} кортеж из m элементов <tex>(K^1_1+...\ldots +K_n^1,...\ldots ,K_1^m +...\ldots +K_n^m)</tex> без <tex>G_is</tex>, и говорится, что <tex>F</tex> дополняет <tex>E</tex> с помощью <tex>e</tex>.

Особый случай расширения возникает когда хвосты одинаковы. Если <tex>E = E_1G_1 + ... \ldots + E_nG_n</tex> и <tex>F = F_1G_1+...\ldots +F_nG_n</tex>, тогда <tex>F</tex> расширяет <tex>E</tex> с помощью <tex>e = ( \varepsilon + \emptyset +... \ldots + \emptyset ,...\ldots , \emptyset + \emptyset +...\ldots + \varepsilon)</tex>. Расширение <tex>e</tex> сокращается до тождества <tex>\varepsilon</tex> (аналог единичной матрицы).

Процедура для проверки <tex>E \sim F</tex> {{- --}} направленное дерево доказательства из выражений, имеющие графическое представление, со стартовой целью <tex>E \doteq F</tex>. Чтобы проверить конфигурации на эквивалентность мы будем разбивать выражения на подвыражения используя правила вывода. Существует всего три правила вывода:

где <tex>C</tex> {{- --}} это условие:

# Имеется ровно <tex>max \max_{1 \leqslant i \leqslant k } \{ |w(X_i)| : E_i \neq \emptyset , 1 \leq i \leq k \}</tex> применений <tex>UNF</tex> между верхним и нижним выражением, и не применяются другие правила.# Если <tex>u</tex> {{- --}} это слово относящиеся к полседовательности операция <tex>UNF</tex>, то <tex>E_i = (X_i \cdot u)</tex> для каждого <tex>i : 1 \leq leqslant i \leq leqslant k \</tex>.

<tex>UNF</tex> {{- --}} означает развертывание(англ. ''unfold''), редуцирует выражение <tex>E \doteq F</tex> на подвыражения <tex>(E \cdot a) \doteq (F \cdot a)</tex> для каждого <tex>a</tex> из алфавита. Если исходное выражение истинно, то истинны и его подвыражения. Более строгая версия этого факта зафиксирована в следующих фактах:

# Если <tex>E \nsim_{m+1} F</tex>, то для какого-то <tex>a \in \sigma</tex> выполняется <tex>(E \cdot a) \nsim_m (F \cdot a)</tex>.

Применение <tex>BAL</tex> использует <tex>F</tex>, если <tex>F</tex> {{- --}} конфигурация в исходном выражении правила вывода. Если есть успешное представление, корень которого является ложным, то существует ветвь таблицы, внутри которой каждое подвыражение является ложной. Если два исходных выражения принадлежат последующей ветке, то подвыражение сохраняет уровень ложности второй предпосылки. Запишем это более строго:

# Если <tex>X_1H_1+...\ldots +X_kH_k \sim F</tex> и <tex>E_1H_1+...\ldots +E_kH_k \sim F'</tex>, тогда <tex>E_1(F \cdot w(X_1))+...\ldots +X_k(F \cdot w(X_k)) \sim F'</tex>.# Если <tex>X_1H_1+...\ldots +X_kH_k \sim_{n+m} F</tex> и <tex>E_1H_1+...\ldots +E_kH_k \nsim_{n+1} F'</tex> и каждая <tex>E_i \neq \varepsilon</tex> и <tex>m \ge geqslant \max \{ |w(X_i)| : \mid E_i \neq \emptyset \}</tex>, то <tex>E_1(F \cdot w(X_1))+...\ldots +E_k(F \cdot w(X_k)) \nsim_{n+1} F'</tex>.

|statement=Пусть есть два семейства выражений <tex>g(i), h(i), 1 \leq leqslant i \leq leqslant 2^n</tex>, и каждое выражение <tex>g(i)</tex> имеет форму <tex>E_1G^i_1+...\ldots +E_nG^i_n=F_1G^i_1+...\ldots +F_nG^i_n</tex> и каждое выражение <tex>h(i)</tex> имеет форму <tex>E_1H^i_1+...\ldots +E_nH^i_n=F_1H^i_1+...\ldots +F_nH^i_n</tex>. Пусть расширения <tex>e_1,...\ldots ,e_n</tex> такие, что для каждого <tex>e_j</tex> и <tex>i \ge geqslant 0, g(2^j i + 2^{j-1} + 1)</tex> расширяет <tex>g(2^j i + 2^{j-1})</tex> с помощью <tex>e_j</tex> и <tex>h(2^j i + 2^{j-1} + 1)</tex> расширяет <tex>h(2^j i + 2^{j-1})</tex> с помощью <tex>e_j</tex>.

Если для каждое выражение <tex>g(i)</tex> верно на уровне <tex>m, i: 1 \leq leqslant i \leq leqslant 2^n</tex>, и для каждого выражения <tex>h(j),j: 1 \leq leqslant j < 2^n</tex> верно на уровне <tex>m</tex>,

|definition=Пусть ветка доказательства состоит из выражений <tex>d(0),...\ldots ,d(l)</tex>. Выражение <tex>d(l)</tex> '''удовлетворяет''' теореме о расширении если существеют выражения <tex>g(i),h(i),1 \leq leqslant i \leq leqslant 2^n</tex>, и расширения <tex>e_1,...\ldots ,e_n</tex> как описано в теормере о расширении, и выражения принадлежат <tex>\{d(0),...\ldots ,d(l)\}</tex>, и <tex>h(2^n)</tex> {{- --}} это <tex>d(l)</tex> и есть хотя бы одно применение <tex>UNF</tex> между выражением <tex>h(2^n-1)</tex> и <tex>d(l)</tex>.

|definition=Пусть ветка доказательства состоит из выражений <tex>g(0),...\ldots ,g(n)</tex>, где <tex>g(0)</tex> {{--- }} корневое выражение. Выражение <tex>g(n)</tex> {{--- }} это финальное выражние находящиеся одном из следующих условий:# Если <tex>g(n)</tex> {{--- }} это тождество <tex>E \doteq E</tex>, то <tex>g(n)</tex> {{--- }} это '''успешное финальное выражение'''.# Если <tex>g(n)</tex> удовлетворяет теореме о расширении, то <tex>g(n)</tex> {{--- }} это '''успешное финальное выражение'''.# Если <tex>g(n)</tex> имеет форму <tex>E \doteq \emptyset</tex> или <tex>\emptyset \doteq E</tex> (и <tex>E \neq \emptyset</tex>), тогда <tex>g(n)</tex> {{--- }} это '''неуспешное финальное выражение'''.

|statement=В бесконечной ветке доказательств состоящей из выражений <tex>g(0),...\ldots ,g(n),...\ldots </tex> где <tex>g(0)</tex> {{- --}} корневое выражение, существует такое <tex>n</tex>, что <tex>g(n)</tex> {{--- }} финальное выражение.

# '''Шаг <tex>n+1</tex>:''' Если текущая вершина ветвления <tex>g(n)</tex> ветки <tex>g(0),...\ldots ,g(n)</tex> {{- --}} это неуспешное финальное выражение, то прерываемся и возвращаем "некорректное представление";<br>Если каждая вершина ветвления <tex>g(n)</tex> ветки <tex>g(0),...\ldots ,g(n)</tex> {{--- }} успешное финальное выражение, тогда возвращаем "корректное представление";<br>Иначе для каждой вершины ветвления <tex>g(n)</tex> ветки <tex>g(0),...\ldots ,g(n)</tex>, которая не является финальной целью, применяем следующие правило, и подвыражения, получившиеся в результате, {{--- }} новые вершины ветвления расширенных веток.