7
правок
Изменения
Нет описания правки
Предположим детерминированный строгий автомат с единственным состоянием с элементами, представленный тройкой: входной алфавит на ленте <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>F</tex> такая что <tex>(E, u) \rightarrow F</tex>, которая может быть и <tex>\emptyset</tex>.
}}
{{Определение
Равенство задаваемых языков также может быть приблизительным.
{{Определение
|definition=<tex>E \sim_n F, n \geq 0</tex> - конфигурафии <tex>E</tex> и <tex>F</tex> '''<tex>n</tex>-эквивалентны''' если они принимают одни и те же слова, длина которых не больше <tex>n</tex>:
<br>для всех слов <tex>w</tex>, таких что <tex>|w| \leq n, (E \cdot w) = \varepsilon</tex> тогда и только тогда, когда <tex>(F \cdot w) = \varepsilon</tex>
}}
}}
Можно рассматривать дополнения как матрицы. Если <tex>E''</tex> расширяет <tex>E'</tex> с помощью <tex>e</tex> и <tex>E'</tex> расширяет <tex>E</tex> с помощью <tex>f</tex>, то <tex>E''</tex> расширяет <tex>E</tex> с помощью <tex>ef</tex>(в смысле умножения матриц).
Особый случай расширения возникает когда хвосты одинаковы. Если <tex>E = E_1G_1 + ... + E_nG_n</tex> и <tex>F = F_1G_1+...+F_nG_n</tex>, тогда <tex>F</tex> расширяет <tex>E</tex> с помощью <tex>e = ( \varepsilon + \emptyset +... + \emptyset ,..., \emptyset + \emptyset +...+ \varepsilon)</tex>. Расширение <tex>e</tex> сокращается до тождества <tex>\varepsilon</tex> (аналог единичной матрицы).
== Процедура проверки ==
Процедура для проверки <tex>E \sim F</tex> - направленное дерево доказательства из выражений, имеющие графическое представление, со стартовой целью <tex>E \doteq F</tex>. Чтобы проверить конфигурации на эквивалентность мы будем разбивать выражения на подвыражения используя правила вывода. Существует всего три правила вывода:
[[Файл:unf_600.jpg]]
где <tex>C</tex> - это условие:
# Каждая <tex>E_i \neq \varepsilon</tex> и хотя бы одна <tex>H_i \neq \varepsilon</tex>.
# Имеется ровно <tex>max \{ |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 i \leq 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 \sim F</tex> и <tex>a \in \sigma</tex>, то <tex>(E \cdot a) \sim (F \cdot 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> - конфигурация в исходном выражении правила вывода. Если есть успешное представление, корень которого является ложным, то существует ветвь таблицы, внутри которой каждое подвыражение является ложной. Если два исходных выражения принадлежат последующей ветке, то подвыражение сохраняет уровень ложности второй предпосылки. Запишем это более строго:
{{Утверждение
|statement=
Справедливы следующие факты о <tex>BAL</tex>:
# Если <tex>X_1H_1+...+X_kH_k \sim F</tex> и <tex>E_1H_1+...+E_kH_k \sim F'</tex>, тогда <tex>E_1(F \cdot w(X_1))+...+X_k(F \cdot w(X_k)) \sim F'</tex>.
# Если <tex>X_1H_1+...+X_kH_k \sim_{n+m} F</tex> и <tex>E_1H_1+...+E_kH_k \nsim_{n+1} F'</tex> и каждая <tex>E_i \neq \varepsilon</tex> и <tex>m \ge max \{ |w(X_i)| : E_i \neq \emptyset \}</tex>, то <tex>E_1(F \cdot w(X_1))+...+E_k(F \cdot w(X_k)) \nsim_{n+1} F'</tex>.
}}
{{Теорема
|about=о расширении
|statement=Пусть есть два семейства выражений <tex>g(i), h(i), 1 \leq i \leq 2^n</tex>, и каждое выражение <tex>g(i)</tex> имеет форму <tex>E_1G^i_1+...+E_nG^i_n=F_1G^i_1+...+F_nG^i_n</tex> и каждое выражение <tex>h(i)</tex> имеет форму <tex>E_1H^i_1+...+E_nH^i_n=F_1H^i_1+...+F_nH^i_n</tex>.
Пусть расширения <tex>e_1,...,e_n</tex> такие, что для каждого <tex>e_j</tex> и <tex>i \ge 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 i \leq 2^n</tex>, и для каждого выражения <tex>h(j),j: 1 \leq j < 2^n</tex> верно на уровне <tex>m</tex>,
то <tex>h(2^n)</tex> верно на уровне <tex>m</tex>.
}}
{{Определение
|definition=Пусть ветка доказательства состоит из выражений <tex>d(0),...,d(l)</tex>. Выражение <tex>d(l)</tex> '''удовлетворяет''' теореме о расширении если существеют выражения <tex>g(i),h(i),1 \leq i \leq 2^n</tex>, и расширения <tex>e_1,...,e_n</tex> как описано в теормере о расширении, и выражения принадлежат <tex>\{d(0),...,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),...,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),...,g(n),...</tex> где <tex>g(0)</tex> - корневое выражение, существует такое <tex>n</tex>, что <tex>g(n)</tex> - финальное выражение.
}}
Введём несложную '''процедуру проверки <tex>E \sim F</tex>''', и зададим её пошагово.
# '''Шаг <tex>0</tex>:''' начинаем с корневого выражение <tex>g(0)</tex>, <tex>E \doteq F</tex>, что является вершиной ветвления ветки <tex>g(0)</tex>.
# '''Шаг <tex>n+1</tex>:''' Если текущая вершина ветвления <tex>g(n)</tex> ветки <tex>g(0),...,g(n)</tex> - это неуспешное финальное выражение, то прерываемся и возвращаем "некорректное представление";<br>Если каждая вершина ветвления <tex>g(n)</tex> ветки <tex>g(0),...,g(n)</tex> - успешное финальное выражение, тогда возвращаем "корректное представление";<br>Иначе для каждой вершины ветвления <tex>g(n)</tex> ветки <tex>g(0),...,g(n)</tex>, которая не является финальной целью, применяем следующие правило, и подвыражения, получившиеся в результате, - новые вершины ветвления расширенных веток.
{{Теорема
|statement=Справедливы следующие факты:
# Если <tex>E \nsim F</tex>, то процедура проверки вернёт "некорректное представление".
# Если <tex>E \sim F</tex>, то процедура проверки вернёт "корректное представление".
}}
