http://neerc.ifmo.ru/wiki/api.php?action=feedcontributions&user=Oxygen31&feedformat=atomВикиконспекты - Вклад участника [ru]2024-03-28T12:33:04ZВклад участникаMediaWiki 1.30.0http://neerc.ifmo.ru/wiki/index.php?title=%D0%AD%D0%BA%D0%B2%D0%B8%D0%B2%D0%B0%D0%BB%D0%B5%D0%BD%D1%82%D0%BD%D0%BE%D1%81%D1%82%D1%8C_%D0%94%D0%9C%D0%9F-%D0%B0%D0%B2%D1%82%D0%BE%D0%BC%D0%B0%D1%82%D0%BE%D0%B2&diff=59769Эквивалентность ДМП-автоматов2017-01-16T22:20:14Z<p>Oxygen31: </p>
<hr />
<div>[[Нормальная форма ДМП-автомата|Предположим детерминированный строгий автомат с единственным состоянием с элементами, представленный тройкой]]:<br />
* входной алфавит на ленте <tex>\Sigma</tex>,<br />
* стековым алфавит <tex>\Gamma</tex>,<br />
* множеством переходов <tex>\Delta</tex>.<br />
Мы предполагаем наличие полного порядка на <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> {{---}} допустимые конфигурации.<br />
{{Определение<br />
|definition='''Конфигурация <tex>E</tex> после слова <tex>u</tex>''', обозначается <tex>E \cdot u</tex> {{---}} единственная допустимая конфигурация <tex>F</tex> такая что <tex>(E, u) \rightarrow F</tex>, которая может быть и <tex>\emptyset</tex>.<br />
}}<br />
{{Определение<br />
|definition='''Язык, задаваемой конфигурацией <tex>E</tex>''' {{---}} <tex>L(E) = \{ E \mid (E \cdot u) = \varepsilon \}</tex>.<br />
}}<br />
{{Определение<br />
|definition=Две конфигурации <tex>E</tex> и <tex>F</tex> '''эквивалентны''' {{---}} <tex>L(E) = L(F)</tex>, обозначается <tex>E \sim F</tex>.<br />
}}<br />
<br />
Равенство задаваемых языков также может быть приблизительным.<br />
{{Определение<br />
|definition=Конфигурафии <tex>E</tex> и <tex>F</tex> '''<tex>n</tex>-эквивалентны''', обозначается <tex>E \sim_n F, n \geqslant 0</tex> {{---}} они принимают одни и те же слова, длина которых не больше <tex>n</tex>:<br />
<br>для всех слов <tex>w</tex>, таких что <tex>|w| \leqslant n, (E \cdot w) = \varepsilon</tex> тогда и только тогда, когда <tex>(F \cdot w) = \varepsilon</tex>.<br />
}}<br />
<br />
{{Утверждение<br />
|statement=<br />
Справедливы следующие факты:<br />
# <tex>E \sim F</tex> тогда и только тогда, когда для любого <tex> n \geqslant 0</tex> выполняется <tex>E \sim_n F</tex>.<br />
# Если <tex>E \nsim F</tex>, то существует <tex> n \geqslant 0</tex> такой, что <tex>E \sim_n F</tex> и <tex>E \nsim_{n+1} F</tex>.<br />
# Если <tex>E \sim F</tex>, то для любого <tex>u \in \Sigma^*</tex>, <tex>(E \cdot u) \sim (F \cdot u)</tex>.<br />
# <tex>E \sim_{n} F</tex>, тогда и только тогда, когда для любого <tex>u \in \Sigma^*</tex>, где <tex>|u| \leqslant n</tex>, <tex>(E \cdot u) \sim_{n-|u|} (F \cdot u)</tex>.<br />
# Если <tex>E \sim_{n} F</tex> и <tex>0 \leqslant m < n</tex>, то <tex>E \sim_{m} F</tex>.<br />
# Если <tex>E \sim_{n} F</tex> и <tex>F \nsim_{n} G</tex>, то <tex>E \nsim_{n} G</tex>.<br />
}}<br />
<br />
{{Определение<br />
|definition=Для каждого стекового символа <tex>X</tex> '''словом <tex>w(X)</tex>''' называется самое короткое слово в множестве <tex>\{u \mid (X \cdot u) = \varepsilon \}</tex>.<br />
}}<br />
<br />
{{Определение<br />
|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>.<br />
}}<br />
<br />
Приведём некоторые свойства формы голова/хвост. Эквивалентность и <tex>n</tex>-эквивалентность языков согласуются с операцией суммы. Следовательно, форма голова/хвост позволяет подставить эквивалентное выражение в хвост (т.к. допустимость сохраняется).<br />
<br />
{{Утверждение<br />
|statement=<br />
Пусть <tex>E = E_1G_1 + \ldots + E_nG_n</tex>, тогда справедливы следующие факты:<br />
# Если <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>.<br />
# Если <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>.<br />
# Если <tex>H_i \neq \emptyset, 1 \leqslant i \leqslant n</tex>, то <tex>E_1H_1 + \ldots + E_nH_n</tex> в форме голова/хвост.<br />
# Если каждая <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>.<br />
# Если <tex>H_i \sim G_i, 1 \leqslant i \leqslant n</tex>, то <tex>E \sim E_1H_1 + \ldots + E_nH_n</tex>.<br />
}}<br />
<br />
Две конфигурации могут иметь одинаковые головы и разные хвосты, или одинаковые хвосты и различие в головах. Если <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_{1 \leqslant i \leqslant n} \{|E_i|, |F_i| \}</tex>. Если несоответствие равно 0, то конфигурации одинаковы.<br />
<br />
'''Замечание:''' любая пара конфигураций <tex>E</tex> и <tex>F</tex> имеет форму голова/хвост включающую в себя одинаковые хвосты: <tex> E = EG</tex> и <tex>F = FG</tex>, где <tex>G = \varepsilon</tex>.<br />
<br />
{{Определение<br />
|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 \leqslant i \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>.<br />
}}<br />
<br />
Можно рассматривать дополнения как матрицы. Если <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>(в смысле умножения матриц).<br />
<br />
Особый случай расширения возникает когда хвосты одинаковы. Если <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> (аналог единичной матрицы).<br />
<br />
== Процедура проверки ==<br />
Процедура для проверки <tex>E \sim F</tex> {{---}} направленное дерево доказательства из выражений, имеющие графическое представление, со стартовой целью <tex>E \doteq F</tex>. Чтобы проверить конфигурации на эквивалентность мы будем разбивать выражения на подвыражения используя правила вывода. Существует всего три правила вывода:<br />
[[Файл:unf_600.jpg]]<br />
<br />
где <tex>C</tex> {{---}} это условие:<br />
# Каждая <tex>E_i \neq \varepsilon</tex> и хотя бы одна <tex>H_i \neq \varepsilon</tex>.<br />
# Имеется ровно <tex> \max_{1 \leqslant i \leqslant k } \{ |w(X_i)| : E_i \neq \emptyset \}</tex> применений <tex>UNF</tex> между верхним и нижним выражением, и не применяются другие правила.<br />
# Если <tex>u</tex> {{---}} это слово относящиеся к полседовательности операция <tex>UNF</tex>, то <tex>E_i = (X_i \cdot u)</tex> для каждого <tex>i : 1 \leqslant i \leqslant k \</tex>.<br />
<br />
<tex>UNF</tex> {{---}} означает развертывание(англ. ''unfold''), редуцирует выражение <tex>E \doteq F</tex> на подвыражения <tex>(E \cdot a) \doteq (F \cdot a)</tex> для каждого <tex>a</tex> из алфавита. Если исходное выражение истинно, то истинны и его подвыражения. Более строгая версия этого факта зафиксирована в следующих фактах:<br />
# Если <tex>E \sim F</tex> и <tex>a \in \sigma</tex>, то <tex>(E \cdot a) \sim (F \cdot a)</tex>.<br />
# Если <tex>E \nsim_{m+1} F</tex>, то для какого-то <tex>a \in \sigma</tex> выполняется <tex>(E \cdot a) \nsim_m (F \cdot a)</tex>.<br />
<br />
Применение <tex>BAL</tex> использует <tex>F</tex>, если <tex>F</tex> {{---}} конфигурация в исходном выражении правила вывода. Если есть успешное представление, корень которого является ложным, то существует ветвь таблицы, внутри которой каждое подвыражение является ложной. Если два исходных выражения принадлежат последующей ветке, то подвыражение сохраняет уровень ложности второй предпосылки. Запишем это более строго:<br />
<br />
{{Утверждение<br />
|statement=<br />
Справедливы следующие факты о <tex>BAL</tex>:<br />
# Если <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>.<br />
# Если <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 \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>.<br />
}}<br />
<br />
{{Теорема<br />
|about=о расширении<br />
|statement=Пусть есть два семейства выражений <tex>g(i), h(i), 1 \leqslant i \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>.<br />
Пусть расширения <tex>e_1, \ldots ,e_n</tex> такие, что для каждого <tex>e_j</tex> и <tex>i \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>.<br />
<br />
Если для каждое выражение <tex>g(i)</tex> верно на уровне <tex>m, i: 1 \leqslant i \leqslant 2^n</tex>, и для каждого выражения <tex>h(j),j: 1 \leqslant j < 2^n</tex> верно на уровне <tex>m</tex>,<br />
то <tex>h(2^n)</tex> верно на уровне <tex>m</tex>.<br />
}}<br />
{{Определение<br />
|definition=Пусть ветка доказательства состоит из выражений <tex>d(0), \ldots ,d(l)</tex>. Выражение <tex>d(l)</tex> '''удовлетворяет''' теореме о расширении если существеют выражения <tex>g(i),h(i),1 \leqslant i \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>.<br />
}}<br />
{{Определение<br />
|definition=Пусть ветка доказательства состоит из выражений <tex>g(0), \ldots ,g(n)</tex>, где <tex>g(0)</tex> {{---}} корневое выражение. Выражение <tex>g(n)</tex> {{---}} это финальное выражние находящиеся одном из следующих условий:<br />
# Если <tex>g(n)</tex> {{---}} это тождество <tex>E \doteq E</tex>, то <tex>g(n)</tex> {{---}} это '''успешное финальное выражение'''.<br />
# Если <tex>g(n)</tex> удовлетворяет теореме о расширении, то <tex>g(n)</tex> {{---}} это '''успешное финальное выражение'''.<br />
# Если <tex>g(n)</tex> имеет форму <tex>E \doteq \emptyset</tex> или <tex>\emptyset \doteq E</tex> (и <tex>E \neq \emptyset</tex>), тогда <tex>g(n)</tex> {{---}} это '''неуспешное финальное выражение'''.<br />
}}<br />
{{Лемма<br />
|statement=В бесконечной ветке доказательств состоящей из выражений <tex>g(0), \ldots ,g(n), \ldots </tex> где <tex>g(0)</tex> {{---}} корневое выражение, существует такое <tex>n</tex>, что <tex>g(n)</tex> {{---}} финальное выражение.<br />
}}<br />
<br />
Введём несложную '''процедуру проверки <tex>E \sim F</tex>''', и зададим её пошагово.<br />
# '''Шаг <tex>0</tex>:''' начинаем с корневого выражение <tex>g(0)</tex>, <tex>E \doteq F</tex>, что является вершиной ветвления ветки <tex>g(0)</tex>.<br />
# '''Шаг <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>, которая не является финальной целью, применяем следующие правило, и подвыражения, получившиеся в результате, {{---}} новые вершины ветвления расширенных веток.<br />
<br />
{{Теорема<br />
|statement=Справедливы следующие факты:<br />
# Если <tex>E \nsim F</tex>, то процедура проверки вернёт "некорректное представление".<br />
# Если <tex>E \sim F</tex>, то процедура проверки вернёт "корректное представление".<br />
}}<br />
<br />
== См. также ==<br />
* [[Нормальная форма ДМП-автомата]]<br />
* [[Детерминированные автоматы с магазинной памятью, допуск по пустому стеку]]<br />
* [[Детерминированные автоматы с магазинной памятью]]<br />
* [[ДМП-автоматы и неоднозначность]]<br />
<br />
== Источники информации ==<br />
* [http://homepages.inf.ed.ac.uk/cps/india.pdf Colin Stirling "An Introduction to Decidability of DPDA Equivalence"]<br />
<br />
[[Категория: Теория формальных языков]]<br />
[[Категория: Контекстно-свободные грамматики]]<br />
[[Категория: МП-автоматы]]</div>Oxygen31http://neerc.ifmo.ru/wiki/index.php?title=%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D1%84%D0%BE%D1%80%D0%BC%D0%B0%D0%BB%D1%8C%D0%BD%D1%8B%D1%85_%D1%8F%D0%B7%D1%8B%D0%BA%D0%BE%D0%B2&diff=59766Теория формальных языков2017-01-16T21:45:09Z<p>Oxygen31: /* МП-автоматы */</p>
<hr />
<div>[[Категория: Теория формальных языков]]<br />
Символом <tex> \star </tex> помечены дополнительные темы (возможно, сложные), которые не были подробно рассмотрены (или вообще рассмотрены) в рамках курса.<br />
== Автоматы и регулярные языки ==<br />
=== Регулярные языки и ДКА ===<br />
*[[Основные определения: алфавит, слово, язык, конкатенация, свободный моноид слов; операции над языками]]<br />
*[[Регулярные языки: два определения и их эквивалентность | Регулярные языки: два определения и их эквивалентность, регулярные выражения]]<br />
*[[Детерминированные конечные автоматы]]<br />
*[[Прямое произведение ДКА]]<br />
*[[Простой сопоставитель регулярных выражений]] <tex> \star </tex><br />
<br />
=== НКА ===<br />
*[[Недетерминированные конечные автоматы]]<br />
*[[Построение по НКА эквивалентного ДКА, алгоритм Томпсона]]<br />
*[[Автоматы с eps-переходами. Eps-замыкание]]<br />
*[[Теорема Клини (совпадение классов автоматных и регулярных языков)]]<br />
*[[Альтернативное доказательство теоремы Клини (через систему уравнений в регулярных выражениях)]]<br />
=== Минимизация ДКА ===<br />
*[[Эквивалентность состояний ДКА]]<br />
*[[Минимизация ДКА, алгоритм за O(n^2) с построением пар различимых состояний]]<br />
*[[Минимизация ДКА, алгоритм Хопкрофта (сложность O(n log n))]]<br />
*[[Алгоритм Бржозовского]]<tex> ^\star </tex><br />
=== Свойства конечных автоматов ===<br />
*[[Доказательство нерегулярности языков: лемма о разрастании]]<br />
*[[Интерпретация булевых формул с кванторами как игр для двух игроков]]<br />
*[[Решение уравнений в регулярных выражениях]]<br />
*[[Замкнутость регулярных языков относительно различных операций]]<br />
*[[Анализ свойств регулярных языков (пустота, совпадение, включение, конечность, подсчет числа слов)]]<br />
*[[Контексты и синтаксические моноиды]]<br />
=== Другие автоматы ===<br />
*[[Локальные автоматы]]<tex> ^\star </tex><br />
*[[Двусторонний детерминированный конечный автомат]]<tex> ^\star </tex><br />
*[[Квантовые конечные автоматы]]<tex> ^\star </tex><br />
*[[Автоматы Мура и Мили]]<tex> ^\star </tex><br />
*[[Автоматы в современном мире]]<tex> ^\star </tex><br />
<br />
== Контекстно-свободные грамматики ==<br />
=== Базовые понятия о грамматиках ===<br />
*[[Формальные грамматики]]<br />
*[[Иерархия Хомского формальных грамматик]]<br />
*[[Неукорачивающие и контекстно-зависимые грамматики, эквивалентность]]<br />
*[[Правоконтекстные грамматики, эквивалентность автоматам]]<br />
*[[Контекстно-свободные грамматики, вывод, лево- и правосторонний вывод, дерево разбора]]<br />
*[[Замкнутость КС-языков относительно различных операций]]<br />
*[[Регулярная аппроксимация КС-языков]]<tex> ^\star </tex><br />
<br />
=== Нормальные формы КС-грамматик ===<br />
*[[Удаление бесполезных символов из грамматики]]<br />
*[[Удаление длинных правил из грамматики]]<br />
*[[Удаление eps-правил из грамматики]]<br />
*[[Удаление цепных правил из грамматики]]<br />
*[[Нормальная форма Хомского]]<br />
*[[Устранение левой рекурсии]]<br />
*[[Приведение грамматики к ослабленной нормальной форме Грейбах]]<br />
*[[Нормальная форма Куроды]]<tex> ^\star </tex><br />
<br />
=== Алгоритмы разбора ===<br />
*[[Алгоритм Кока-Янгера-Касами разбора грамматики в НФХ]]<br />
*[[Алгоритм Кока-Янгера-Касами, модификация для произвольной грамматики]]<br />
*[[Алгоритм Эрли]]<br />
*[[Алгоритм Эрли, доказательство оценки O(n^2) для однозначной грамматики]]<br />
<br />
=== Опровержение контекстно-свободности языка ===<br />
*[[Лемма о разрастании для КС-грамматик]]<br />
*[[Лемма Огдена]]<br />
*[[Существенно неоднозначные языки]]<br />
*[[Теорема Парика]]<tex> ^\star </tex><br />
<br />
=== МП-автоматы ===<br />
*[[Автоматы с магазинной памятью]]<br />
*[[МП-автоматы, допуск по пустому стеку и по допускающему состоянию, эквивалентность]]<br />
*[[Совпадение множества языков МП-автоматов и контекстно-свободных языков]]<br />
*[[Детерминированные автоматы с магазинной памятью]]<br />
*[[Детерминированные автоматы с магазинной памятью, допуск по пустому стеку]]<br />
*[[Нормальная форма ДМП-автомата]]<tex> ^\star </tex><br />
*[[Эквивалентность ДМП-автоматов]]<tex> ^\star </tex><br />
*[[Несовпадение класса языков, распознаваемых ДМП автоматами и произвольными МП автоматами]]<br />
*[[ДМП-автоматы и неоднозначность]]<br />
<br />
== Теория вычислимости ==<br />
=== Разрешимые и перечислимые языки ===<br />
*[[Разрешимые (рекурсивные) языки]]<br />
*[[Перечислимые языки]]<br />
*[[Замкнутость разрешимых и перечислимых языков относительно теоретико-множественных и алгебраических операций]]<br />
*[[Вычислимые функции]]<br />
*[[Вычислимые числа]]<br />
*[[Универсальная функция|Универсальная функция и главные нумерации]] <br />
*[[Свойства перечислимых языков. Теорема Успенского-Райса]]<br />
*[[Неотделимые множества]]<br />
*[[Иммунные и простые множества]]<br />
*[[Теорема о рекурсии]]<br />
*[[Квайны]]<tex> ^\star </tex><br />
*[[Busy beaver]]<br />
*[[Колмогоровская сложность]]<tex> ^\star </tex><br />
<br />
=== Вычислительные формализмы ===<br />
*[[Машина Тьюринга]]<br />
*[[Лямбда-исчисление]]<tex> ^\star </tex><br />
*[[Рекурсивные функции, представимость в формальной арифметике | Примитивно рекурсивные функции]]<tex> ^\star </tex><br />
*[[Частично рекурсивные функции]]<tex> ^\star </tex><br />
*[[Стековые машины, эквивалентность двухстековой машины МТ]]<br />
*[[Счетчиковые машины, эквивалентность двухсчетчиковой машины МТ]]<br />
*[[Линейный клеточный автомат, эквивалентность МТ]]<br />
*[[Возможность порождения формальной грамматикой произвольного перечислимого языка]]<br />
*[[Линейный ограниченный автомат]]<br />
*[[Сверхтьюринговые вычисления (гипервычисления)]]<tex> ^\star </tex><br />
*[[Тьюринг-полнота]]<tex> ^\star </tex><br />
<br />
=== Примеры неразрешимых задач ===<br />
*[[m-сводимость]]<br />
*[[Примеры неразрешимых задач: проблема соответствий Поста |Проблема соответствий Поста]]<br />
*[[Примеры неразрешимых задач: однозначность грамматики|Однозначность КС-грамматики]]<br />
*[[Неразрешимость задачи об эквивалентности КС-грамматик|Эквивалентность КС-грамматик]]<br />
*[[Неразрешимость задачи о проверке на пустоту пересечения двух КС-грамматик|Пустота пересечения КС-грамматик]]<br />
*[[Примеры неразрешимых задач: задача о замощении|Задача о замощении полимино]]<br />
*[[Примеры неразрешимых задач: задача о выводе в полусистеме Туэ|Задача о выводе в полусистеме Туэ]]<br />
*[[Неразрешимость исчисления предикатов первого порядка]]<br />
*[[Неразрешимость проблемы существования решения диофантова уравнения в целых числах]]<br />
*[[Игра «Жизнь»]]<tex>^\star</tex><br />
*[[Неразрешимость игры Braid]]<tex>^\star</tex><br />
*[[Теорема Райса-Шапиро]]</div>Oxygen31http://neerc.ifmo.ru/wiki/index.php?title=%D0%9D%D0%BE%D1%80%D0%BC%D0%B0%D0%BB%D1%8C%D0%BD%D0%B0%D1%8F_%D1%84%D0%BE%D1%80%D0%BC%D0%B0_%D0%94%D0%9C%D0%9F-%D0%B0%D0%B2%D1%82%D0%BE%D0%BC%D0%B0%D1%82%D0%B0&diff=59763Нормальная форма ДМП-автомата2017-01-16T21:06:04Z<p>Oxygen31: /* Применение */</p>
<hr />
<div>== Определение ==<br />
{{Определение<br />
|definition=ДМП в '''нормальной форме''' (англ. ''Normal Form'') называется такой [[Детерминированные автоматы с магазинной памятью, допуск по пустому стеку|детерминированный автомат с магазинной памятью]] <tex>M</tex>, представленный конечным набором состояний <tex>Q</tex>, входным алфавитом на ленте <tex>\Sigma</tex>, стековым алфавитом <tex>\Gamma</tex> и множеством переходов <tex>\Delta</tex>, который удовлетворяет следующим условиям:<br />
# Если <tex>(p, a, S) \rightarrow (q, \alpha) \in \Delta</tex>, то <tex>|\alpha| \leqslant 2</tex>, где <tex>\alpha \in \Gamma^*</tex> {{---}} последовательность стековых символов, <tex>S \in \Gamma</tex>.<br />
# Если <tex>(p, \varepsilon, S) \rightarrow (q, \alpha) \in \Delta</tex>, то <tex>\alpha = \varepsilon</tex>.<br />
# <tex>\Delta</tex> не содержит бесполезных переходов (переход <tex>(p, a, S) \rightarrow (q, \alpha)</tex> считается бесполезным, если <tex>L(q, \alpha) = \emptyset</tex>, то есть из конфигурации <tex>(q, \alpha)</tex> нельзя ничего вывести).<br />
}}<br />
<br />
{{Определение<br />
|definition=Множество слов выводимых из конфигурации <tex>L(p, \sigma) = \{ \omega \in \Sigma^* : \exists q \in Q (p, \omega, \sigma) \rightarrow (q, \varepsilon) \}</tex>.<br />
}}<br />
<br />
'''Замечание:''' здесь и далее речь идёт о [[Детерминированные автоматы с магазинной памятью, допуск по пустому стеку|ДМП с допуском по пустому стеку]].<br />
<br />
==Пример==<br />
Пусть<br />
: <tex>Q = \{p, r\}</tex><br />
: <tex>\Sigma = \{a, b, c\}</tex><br />
: <tex>\Gamma = \{X, Y\}</tex><br />
: <tex>(p, X)</tex> {{---}} стартовая конфигурация<br />
и переходы имеют следующий вид:<br />
: <tex>(p, a, X) \rightarrow (p, X)</tex><br />
: <tex>(p, b, X) \rightarrow (p, \varepsilon)</tex><br />
: <tex>(p, c, X) \rightarrow (p, X)</tex><br />
: <tex>(r, \varepsilon, X) \rightarrow (p, \varepsilon)</tex><br />
: <tex>(p, a, Y) \rightarrow (p, \varepsilon)</tex><br />
: <tex>(p, b, Y) \rightarrow (r, \varepsilon)</tex><br />
: <tex>(p, c, Y) \rightarrow (p, YY)</tex><br />
: <tex>(r, \varepsilon, Y) \rightarrow (r, \varepsilon)</tex><br />
Данный автомат будет являться [[Детерминированные автоматы с магазинной памятью, допуск по пустому стеку|ДМП автоматом с допуском по пустому стеку]] в нормальной форме.<br />
<br />
== Автомат с единственным состоянием ==<br />
{{Определение<br />
|definition='''Автомат с единственным состоянием ''' (англ. ''Single State Push Down Automata'', ''SDA'') называется такой автомат <tex>M</tex>, представленный тройкой: входной алфавит на ленте <tex>\Sigma</tex>, стековым алфавит <tex>\Gamma</tex> и множеством переходов <tex>\Delta</tex>.<br />
Переходы в таком автомате имеют вид:<br />
: <tex>(S, a) \rightarrow \alpha</tex>, где <tex>a \in \Sigma</tex>, <tex>S \in \Gamma</tex>, <tex>\alpha \in \Gamma^*</tex><br />
}}<br />
<br />
{{Определение<br />
|definition=Множество слов выводимых из конфигурации <tex>L(\alpha) = \{ \omega \in \Sigma^* : (\alpha, \omega) \rightarrow \varepsilon \}</tex>.<br />
}}<br />
<br />
{{Определение<br />
|definition=Автомат с единственным состоянием находится в '''нормальной форме''', если все его переходы удовлетворяют условию:<br />
: если <tex>(S, a) \rightarrow \alpha \in \Delta</tex>, тогда <tex>|\alpha| \leqslant 2</tex> и <tex>L(\alpha) \neq \emptyset</tex>.<br />
}}<br />
<br />
Автомат с единственным состоянием можно сделать детерминированным, наложив следующее требование на переходы:<br />
: если <tex>(S, a) \rightarrow \alpha \in \Delta</tex> и <tex>(S, a) \rightarrow \beta \in \Delta</tex>, тогда <tex>\alpha = \beta</tex>.<br />
Детерминированный автомат с единственным состоянием соответствует по мощности "простым грамматикам".<br />
<br />
{{Определение<br />
|definition='''Простая грамматика''' (англ. ''Simple Grammar'') {{---}} такая грамматика, где все продукции имеют вид:<br />
: <tex>A \rightarrow \alpha B_1 B_2 \ldots B_n</tex>,<br />
где <tex>\alpha</tex> {{---}} терминал, а все <tex>B_i, i = 1 \ldots n</tex> {{---}} нетерминалы, и существует только одна продукция с парой <tex>\langle A, \alpha \rangle</tex>.<br />
}}<br />
<br />
Однако, множество языков допускаемых детерминированным автоматом с единственным состоянием является строгим подмножеством языков [[Детерминированные автоматы с магазинной памятью|ДМП автоматов]], поэтому больший интерес представляют ''строгие'' автоматы с единственным состоянием.<br />
<br />
Для этого вводится отношение эквивалентности <tex>\equiv</tex> на множестве <tex>\Gamma</tex>, заданное разбиением <tex>\Gamma</tex> на непересекающиеся подмножества.<br />
<br />
'''Пример 1'''<br />
: <tex>\Sigma = \{a, b\}</tex><br />
: <tex>\Gamma = \{A, C, X, Y\}</tex><br />
: <tex>A, X</tex> {{---}} стартовые конфигурации<br />
Переходы:<br />
: <tex>(X, a) \rightarrow YX</tex><br />
: <tex>(X, b) \rightarrow \varepsilon</tex><br />
: <tex>(Y, b) \rightarrow X</tex><br />
: <tex>(A, a) \rightarrow C</tex><br />
: <tex>(A, b) \rightarrow \varepsilon</tex><br />
: <tex>(C, b) \rightarrow AA</tex><br />
Разбиение <tex>\Gamma</tex> имеет вид <tex>\{\{A\}, \{C\}, \{X\}, \{Y\}\}</tex>.<br />
Такой автомат будет детерминированным.<br />
<br />
'''Пример 2'''<br />
: <tex>\Sigma = \{a, b, c\}</tex><br />
: <tex>\Gamma = \{X, Y, Z\}</tex><br />
: <tex>X, Z</tex> {{---}} стартовые конфигурации<br />
Переходы:<br />
: <tex>(X, a) \rightarrow X</tex><br />
: <tex>(X, b) \rightarrow \varepsilon</tex><br />
: <tex>(X, c) \rightarrow X</tex><br />
: <tex>(Y, a) \rightarrow \varepsilon</tex><br />
: <tex>(Y, c) \rightarrow YY</tex><br />
: <tex>(Z, b) \rightarrow \varepsilon</tex><br />
: <tex>(Z, c) \rightarrow Z</tex><br />
: <tex>(Z, c) \rightarrow YZ</tex><br />
Разбиение <tex>\Gamma</tex> имеет вид <tex>\{\{X\}, \{Y, Z\}\}</tex>, что означает, что <tex>Y \equiv Z</tex>.<br />
<br />
Отношение <tex>\equiv</tex> можно расширить на последовательность стековых символов:<br />
<br />
<tex>\alpha \equiv \beta</tex> если:<br />
: либо <tex>\alpha = \beta</tex>,<br />
: либо <tex>\alpha = \delta X \alpha'</tex>, <tex>\beta = \delta Y \beta'</tex>, <tex>X \equiv Y</tex> и <tex>X \neq Y</tex>.<br />
<br />
'''Свойства''' <tex>\equiv</tex>:<br />
# <tex>\alpha\beta \equiv \alpha \Leftrightarrow \beta = \varepsilon</tex>.<br />
# <tex>\alpha \equiv \beta \Leftrightarrow \delta\alpha \equiv \delta\beta</tex>.<br />
# Если <tex>\alpha \equiv \beta</tex> и <tex>\gamma \equiv \delta</tex>, тогда <tex>\alpha\gamma \equiv \beta\delta</tex>.<br />
# Если <tex>\alpha \equiv \beta</tex> и <tex>\alpha \neq \beta</tex>, тогда <tex>\alpha\gamma \equiv \beta\delta</tex>.<br />
# Если <tex>\alpha\gamma \equiv \beta\delta</tex> и <tex>|\alpha| = |\beta|</tex>, тогда <tex>\alpha \equiv \beta</tex>.<br />
<br />
{{Определение<br />
|definition=Отношение <tex>\equiv</tex> на множестве <tex>\Gamma</tex> является '''строгим''' (англ. ''strict''), если выполняются следующие условия:<br />
# Если <tex>X \equiv Y</tex>, <tex>(X, a) \rightarrow \alpha</tex> и <tex>(Y, a) \rightarrow \beta</tex>, тогда <tex>\alpha \equiv \beta</tex>.<br />
# Если <tex>X \equiv Y</tex>, <tex>(X, a) \rightarrow \alpha</tex> и <tex>(Y, a) \rightarrow \alpha</tex>, тогда <tex>X = Y</tex>.<br />
}}<br />
<br />
{{Определение<br />
|definition=Автомат с единственным состоянием с заданным разбиением <tex>\Gamma</tex> является '''строгим''' (англ. ''strict''), если отношение <tex>\equiv</tex> строгое на множестве <tex>\Gamma</tex>.<br />
}}<br />
<br />
<br />
Определение конфигураций автомата с единственным состоянием расширяется на наборы из последовательностей символов стека <tex>\{ \alpha_1, \ldots , \alpha_n \}</tex>, которые записываются в виде суммы <tex>\alpha_1 + \ldots + \alpha_n</tex>.<br />
<br />
Две суммы конфигураций считаются эквивалентными (записывается через <tex>=</tex>), если они представляют собой один и тот же набор.<br />
<br />
Язык суммы конфигураций определяется {{---}} <tex>L(\alpha_1 + \ldots + \alpha_n) = \bigcup\limits_{i = 1}^{n}L(\alpha_i)</tex><br />
<br />
{{Определение<br />
|definition=Сумма конфигураций <tex>\beta_1 + \ldots + \beta_n</tex> называется '''допустимой''' (англ. ''admissible''), если <tex>\beta_i \equiv \beta_j</tex> для всех элементов суммы, и <tex>\beta_i \neq \beta_j</tex> при <tex>i \neq j</tex>.<br />
}}<br />
Таким образом <tex>\emptyset</tex> {{---}} тоже допустимо.<br />
Некоторые суммы из второго примера: <tex>XX</tex>, <tex>ZZZ + ZZY</tex>, <tex>YX + Z</tex>, <tex>Z + YZ</tex> и <tex>Z + YZ + YYZ</tex> {{---}} все эти суммы допустимые, в то время как <tex>X + Y</tex> будет недопустима, так как <tex>X \not\equiv Y</tex>.<br />
<br />
Строгий автомат с единственным состоянием можно сделать детерминированным, заменив множество переходов <tex>\Delta</tex> на <tex>\Delta'</tex>:<br />
для каждого символа <tex>X \in \Gamma</tex> и <tex>a \in \Sigma</tex> переходы вида<br />
<tex>(X, a) \rightarrow \alpha_1, \ldots , (X, a) \rightarrow \alpha_n</tex> из <tex>\Delta</tex><br />
заменяются на один переход <tex>(X, a) \rightarrow \alpha_1 + \ldots + \alpha_n</tex>.<br />
Таким образом для каждого <tex>X \in \Gamma</tex> и <tex>a \in \Sigma</tex> будет уникальный переход <tex>(X, a) \rightarrow \sum{\alpha_i}</tex> из <tex>\Delta'</tex>.<br />
<br />
== Связь ДМП автомата в нормальной форме и автомата с единственным состоянием ==<br />
{{Утверждение<br />
|statement=Допустимые конфигурации строгого автомата с единственным состоянием генерируют те же языки, что и конфигурации [[Детерминированные автоматы с магазинной памятью, допуск по пустому стеку|ДМП с допуском по пустому стеку]].<br />
|proof=<br />
Пусть задан ДМП автомат в нормальной форме в виде четырех множеств <tex>Q, \Sigma, \Gamma, \Delta</tex>.<br />
# Для двух состояний <tex>p, q \in Q</tex> и <tex>X \in \Gamma</tex> заведём новый символ стека <tex>[pXq]</tex>.<br />
# Для переходов для данного <tex>a \in \Sigma</tex>:<br />
#* если <tex>(p, a, X) \rightarrow (q, \varepsilon) \in \Delta</tex>, тогда <tex>([pXq], a) \rightarrow \varepsilon</tex>;<br />
#* если <tex>(p, a, X) \rightarrow (q, Y) \in \Delta</tex>, тогда <tex>([pXr], a) \rightarrow [qYr]</tex> для всех <tex>r \in Q</tex>;<br />
#* если <tex>(p, a, X) \rightarrow (q, YZ) \in \Delta</tex>, тогда <tex>([pXr], a) \rightarrow [qYp'][p'Zr]</tex> для всех <tex>r,p' \in Q</tex>.<br />
# [pSq] считается <tex>\varepsilon</tex>-символом, если <tex>(p, \varepsilon, X) \rightarrow (q, \varepsilon) \in \Delta</tex>. Все <tex>\varepsilon</tex>-символы удаляются из правой части переходов, полученных в предыдущем пункте.<br />
Полученный автомат с единственным состоянием также находится в нормальной форме. Детерминируем новый автомат, чтобы сохранить детерминированность.<br />
Таким образом каждая конфигурация вида <tex>pX_1X_2 \ldots X_n</tex> из исходного автомата была трансформирована в <tex>sum(p\alpha) = \sum\limits_{p_i \in Q}{[p X_1 p_1][p_1 X_2 p_2] \ldots [p_{n-1}X_n p_n]}</tex> и <tex>L(p\alpha) = L(sum(p\alpha))</tex>.<br />
}}<br />
<br />
Применим алгоритм к самому первому примеру и получим следующее:<br />
: <tex>(X, a) \rightarrow X</tex><br />
: <tex>(Y, a) \rightarrow \varepsilon</tex><br />
: <tex>(Z, a) \rightarrow \emptyset</tex><br />
: <tex>(X, b) \rightarrow \varepsilon</tex><br />
: <tex>(Y, b) \rightarrow \emptyset</tex><br />
: <tex>(Z, b) \rightarrow \varepsilon</tex><br />
: <tex>(X, c) \rightarrow X</tex><br />
: <tex>(Y, c) \rightarrow YY</tex><br />
: <tex>(Z, c) \rightarrow YZ + Z</tex>, где<br />
<br />
: <tex>X = [pXp]</tex><br />
: <tex>Y = [pYp]</tex><br />
: <tex>Z = [pYr]</tex><br />
<br />
== Применение ==<br />
Нормализация [[Детерминированные автоматы с магазинной памятью|ДМП автоматов]] используется в задаче проверки их на [[Эквивалентность ДМП автоматов|эквивалентность]].<br />
Для этого автоматы переводятся в нормальную форму, а затем в автоматы с единственным состоянием, для которых эта задача разрешима, следовательно разрешима и изначальная задача.<br />
<br />
== См. также ==<br />
* [[Детерминированные автоматы с магазинной памятью, допуск по пустому стеку]]<br />
* [[Детерминированные автоматы с магазинной памятью]]<br />
* [[ДМП-автоматы и неоднозначность]]<br />
<br />
== Источники информации ==<br />
* [http://homepages.inf.ed.ac.uk/cps/india.pdf Colin Stirling "An Introduction to Decidability of DPDA Equivalence"]<br />
<br />
[[Категория: Теория формальных языков]]<br />
[[Категория: Контекстно-свободные грамматики]]<br />
[[Категория: МП-автоматы]]</div>Oxygen31http://neerc.ifmo.ru/wiki/index.php?title=%D0%AD%D0%BA%D0%B2%D0%B8%D0%B2%D0%B0%D0%BB%D0%B5%D0%BD%D1%82%D0%BD%D0%BE%D1%81%D1%82%D1%8C_%D0%94%D0%9C%D0%9F-%D0%B0%D0%B2%D1%82%D0%BE%D0%BC%D0%B0%D1%82%D0%BE%D0%B2&diff=59762Эквивалентность ДМП-автоматов2017-01-16T21:03:47Z<p>Oxygen31: </p>
<hr />
<div>[[Нормальная форма ДМП-автомата|Предположим детерминированный строгий автомат с единственным состоянием с элементами, представленный тройкой]]: входной алфавит на ленте <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> - допустимые конфигурации.<br />
{{Определение<br />
|definition=<tex>E \cdot u</tex> - конфигурация '''<tex>E</tex> после слова <tex>u</tex>''', единственная допустимая конфигурация <tex>F</tex> такая что <tex>(E, u) \rightarrow F</tex>, которая может быть и <tex>\emptyset</tex>.<br />
}}<br />
{{Определение<br />
|definition=Язык, задаваемой конфигурацией <tex>E</tex>, <tex>L(E) = \{ E : (E \cdot u) = \varepsilon \}</tex>.<br />
}}<br />
{{Определение<br />
|definition=<tex>E \sim F</tex> - две конфигурации <tex>E</tex> и <tex>F</tex> '''эквивалентны''' если <tex>L(E) = L(F)</tex>.<br />
}}<br />
<br />
Равенство задаваемых языков также может быть приблизительным.<br />
{{Определение<br />
|definition=<tex>E \sim_n F, n \geq 0</tex> - конфигурафии <tex>E</tex> и <tex>F</tex> '''<tex>n</tex>-эквивалентны''' если они принимают одни и те же слова, длина которых не больше <tex>n</tex>:<br />
<br>для всех слов <tex>w</tex>, таких что <tex>|w| \leq n, (E \cdot w) = \varepsilon</tex> тогда и только тогда, когда <tex>(F \cdot w) = \varepsilon</tex><br />
}}<br />
<br />
{{Утверждение<br />
|statement=<br />
Справедливы следующие факты:<br />
# <tex>E \sim F</tex> тогда и только тогда, когда для любого <tex> n \geq 0</tex> выполняется <tex>E \sim_n F</tex><br />
# Если <tex>E \nsim F</tex>, то существует <tex> n \geq 0</tex> такой, что <tex>E \sim_n F</tex> и <tex>E \nsim_{n+1} F</tex><br />
# Если <tex>E \sim F</tex>, то для любого <tex>u \in \Sigma^*</tex>, <tex>(E \cdot u) \sim (F \cdot u)</tex>.<br />
# <tex>E \sim_{n} F</tex>, тогда и только тогда, когда для любого <tex>u \in \Sigma^*</tex>, где <tex>|u| \leq n</tex>, <tex>(E \cdot u) \sim_{n-|u|} (F \cdot u)</tex>.<br />
# Если <tex>E \sim_{n} F</tex> и <tex>0 \leq m < n</tex>, то <tex>E \sim_{m} F</tex>.<br />
# Если <tex>E \sim_{n} F</tex> и <tex>F \nsim_{n} G</tex>, то <tex>E \nsim_{n} G</tex>.<br />
}}<br />
<br />
{{Определение<br />
|definition=Для каждого стекового символа <tex>X</tex> словом <tex>w(X)</tex> называется самое короткое слово в множестве <tex>\{u : (X \cdot u) = \varepsilon \}</tex><br />
}}<br />
<br />
{{Определение<br />
|definition=<tex>E = E_1G_1 + ... + E_nG_n</tex> находится в форме голова/хвост, если голова <tex>E_1 + ...+E_n</tex> допустима и хотя бы один <tex>E_i= \emptyset</tex>, и каждый хвост <tex>G_i = \emptyset</tex>.<br />
}}<br />
<br />
Приведём некоторые свойства формы голова/хвост. Эквивалентность и n-эквивалентность языков согласуются с операциями <tex>+</tex> и суммы. Следовательно, форма голова/хвост позволяет подставить эквивалентное выражение в хвост (т.к. допустимость сохраняется).<br />
<br />
{{Утверждение<br />
|statement=<br />
Пусть <tex>E = E_1G_1 + ... + E_nG_n</tex>, тогда справедливы следующие факты:<br />
# Если <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><br />
# Если <tex>(E_i \cdot u) = \emptyset</tex>, то <tex>(E \cdot u) = (E_1 \cdot u)G_1 + ... + (E_n \cdot u)G_n</tex>.<br />
# Если <tex>H_i \neq \emptyset, 1 \leq i \leq n</tex>, то <tex>E_1H_1 + ... + E_nH_n</tex> в форме голова/хвост.<br />
# Если каждая <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 + ... + E_nH_n</tex>.<br />
# Если <tex>H_i \sim G_i, 1 \leq i \leq n</tex>, то <tex>E \sim E_1H_1 + ... + E_nH_n</tex>.<br />
}}<br />
<br />
Две конфигурации могут иметь одинаковые головы и разные хвосты, или одинаковые хвосты и различие в головах. Если <tex>E</tex> представлена в форме голова/хвост<tex>E_1G_1 + ... + E_nG_n</tex> и <tex>F</tex> имеет схожую форму голова/хвост <tex>F_1G_1 + ... + E_nF_n</tex>, имеющая тот же самый хвост. Несоответствие между <tex>E</tex> и <tex>F</tex>, соответственное этому представлению - это <tex>max\{|E_i|, |F_i| : 1 \leq i \leq n\}</tex>. Если несоответствие равно 0, то конфигурации одинаковы.<br />
<br />
'''Замечание:''' любая пара конфигураций <tex>E</tex> и <tex>F</tex> имеет форму голова/хвост включающую в себя одинаковые хвосты: <tex> E = EG</tex> и <tex>F = FG</tex>, где <tex>G = \varepsilon</tex>.<br />
<br />
{{Определение<br />
|definition= Если <tex>E = E_1G_1 + ... + E_nG_n</tex> и <tex>F = F_1F_1 + ... + F_nF_n</tex>, тогда <tex>F</tex> в его форме голова/хвост - '''хвостовое дополнение <tex>E</tex>''' в его форме голова/хвост обеспечивается <tex>H_i = K^i_1G_1 + ... + K^i_nG_n, 1 \leq i \leq m</tex>. Когда <tex>F</tex> - хвостовое дополнение <tex>E</tex>, относящиеся к нему дополнение <tex>e</tex> - кортеж из m элементов <tex>(K^1_1+...+K_n^1,...,K_1^m +...+K_n^m)</tex> без <tex>G_is</tex>, и говорится, что <tex>F</tex> дополняет <tex>E</tex> с помощью <tex>e</tex>.<br />
}}<br />
<br />
Можно рассматривать дополнения как матрицы. Если <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>(в смысле умножения матриц).<br />
<br />
Особый случай расширения возникает когда хвосты одинаковы. Если <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> (аналог единичной матрицы).<br />
<br />
== Процедура проверки ==<br />
Процедура для проверки <tex>E \sim F</tex> - направленное дерево доказательства из выражений, имеющие графическое представление, со стартовой целью <tex>E \doteq F</tex>. Чтобы проверить конфигурации на эквивалентность мы будем разбивать выражения на подвыражения используя правила вывода. Существует всего три правила вывода:<br />
[[Файл:unf_600.jpg]]<br />
<br />
где <tex>C</tex> - это условие:<br />
# Каждая <tex>E_i \neq \varepsilon</tex> и хотя бы одна <tex>H_i \neq \varepsilon</tex>.<br />
# Имеется ровно <tex>max \{ |w(X_i)| : E_i \neq \emptyset , 1 \leq i \leq k \}</tex> применений <tex>UNF</tex> между верхним и нижним выражением, и не применяются другие правила.<br />
# Если <tex>u</tex> - это слово относящиеся к полседовательности операция <tex>UNF</tex>, то <tex>E_i = (X_i \cdot u)</tex> для каждого <tex>i : 1 \leq i \leq k \</tex>.<br />
<br />
<tex>UNF</tex> - означает развертывание(англ. ''unfold''), редуцирует выражение <tex>E \doteq F</tex> на подвыражения <tex>(E \cdot a) \doteq (F \cdot a)</tex> для каждого <tex>a</tex> из алфавита. Если исходное выражение истинно, то истинны и его подвыражения. Более строгая версия этого факта зафиксирована в следующих фактах:<br />
# Если <tex>E \sim F</tex> и <tex>a \in \sigma</tex>, то <tex>(E \cdot a) \sim (F \cdot a)</tex>.<br />
# Если <tex>E \nsim_{m+1} F</tex>, то для какого-то <tex>a \in \sigma</tex> выполняется <tex>(E \cdot a) \nsim_m (F \cdot a)</tex><br />
<br />
Применение <tex>BAL</tex> использует <tex>F</tex>, если <tex>F</tex> - конфигурация в исходном выражении правила вывода. Если есть успешное представление, корень которого является ложным, то существует ветвь таблицы, внутри которой каждое подвыражение является ложной. Если два исходных выражения принадлежат последующей ветке, то подвыражение сохраняет уровень ложности второй предпосылки. Запишем это более строго:<br />
<br />
{{Утверждение<br />
|statement=<br />
Справедливы следующие факты о <tex>BAL</tex>:<br />
# Если <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>.<br />
# Если <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>.<br />
}}<br />
<br />
{{Теорема<br />
|about=о расширении<br />
|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>. <br />
Пусть расширения <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>. <br />
<br />
Если для каждое выражение <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>,<br />
то <tex>h(2^n)</tex> верно на уровне <tex>m</tex>.<br />
}}<br />
{{Определение<br />
|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>.<br />
}}<br />
{{Определение<br />
|definition=Пусть ветка доказательства состоит из выражений <tex>g(0),...,g(n)</tex>, где <tex>g(0)</tex> - корневое выражение. Выражение <tex>g(n)</tex> - это финальное выражние находящиеся одном из следующих условий:<br />
# Если <tex>g(n)</tex> - это тождество <tex>E \doteq E</tex>, то <tex>g(n)</tex> - это успешное финальное выражение.<br />
# Если <tex>g(n)</tex> удовлетворяет теореме о расширении, то <tex>g(n)</tex> - это успешное финальное выражение.<br />
# Если <tex>g(n)</tex> имеет форму <tex>E \doteq \emptyset</tex> или <tex>\emptyset \doteq E</tex> (и <tex>E \neq \emptyset</tex>), тогда <tex>g(n)</tex> - это неуспешное финальное выражение.<br />
}}<br />
{{Лемма<br />
|statement=В бесконечной ветке доказательств состоящей из выражений <tex>g(0),...,g(n),...</tex> где <tex>g(0)</tex> - корневое выражение, существует такое <tex>n</tex>, что <tex>g(n)</tex> - финальное выражение.<br />
}}<br />
<br />
Введём несложную '''процедуру проверки <tex>E \sim F</tex>''', и зададим её пошагово.<br />
# '''Шаг <tex>0</tex>:''' начинаем с корневого выражение <tex>g(0)</tex>, <tex>E \doteq F</tex>, что является вершиной ветвления ветки <tex>g(0)</tex>.<br />
# '''Шаг <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>, которая не является финальной целью, применяем следующие правило, и подвыражения, получившиеся в результате, - новые вершины ветвления расширенных веток.<br />
<br />
{{Теорема<br />
|statement=Справедливы следующие факты:<br />
# Если <tex>E \nsim F</tex>, то процедура проверки вернёт "некорректное представление".<br />
# Если <tex>E \sim F</tex>, то процедура проверки вернёт "корректное представление".<br />
}}</div>Oxygen31http://neerc.ifmo.ru/wiki/index.php?title=%D0%AD%D0%BA%D0%B2%D0%B8%D0%B2%D0%B0%D0%BB%D0%B5%D0%BD%D1%82%D0%BD%D0%BE%D1%81%D1%82%D1%8C_%D0%94%D0%9C%D0%9F-%D0%B0%D0%B2%D1%82%D0%BE%D0%BC%D0%B0%D1%82%D0%BE%D0%B2&diff=59761Эквивалентность ДМП-автоматов2017-01-16T21:02:09Z<p>Oxygen31: </p>
<hr />
<div>Предположим детерминированный строгий автомат с единственным состоянием с элементами, представленный тройкой: входной алфавит на ленте <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> - допустимые конфигурации.<br />
{{Определение<br />
|definition=<tex>E \cdot u</tex> - конфигурация '''<tex>E</tex> после слова <tex>u</tex>''', единственная допустимая конфигурация <tex>F</tex> такая что <tex>(E, u) \rightarrow F</tex>, которая может быть и <tex>\emptyset</tex>.<br />
}}<br />
{{Определение<br />
|definition=Язык, задаваемой конфигурацией <tex>E</tex>, <tex>L(E) = \{ E : (E \cdot u) = \varepsilon \}</tex>.<br />
}}<br />
{{Определение<br />
|definition=<tex>E \sim F</tex> - две конфигурации <tex>E</tex> и <tex>F</tex> '''эквивалентны''' если <tex>L(E) = L(F)</tex>.<br />
}}<br />
<br />
Равенство задаваемых языков также может быть приблизительным.<br />
{{Определение<br />
|definition=<tex>E \sim_n F, n \geq 0</tex> - конфигурафии <tex>E</tex> и <tex>F</tex> '''<tex>n</tex>-эквивалентны''' если они принимают одни и те же слова, длина которых не больше <tex>n</tex>:<br />
<br>для всех слов <tex>w</tex>, таких что <tex>|w| \leq n, (E \cdot w) = \varepsilon</tex> тогда и только тогда, когда <tex>(F \cdot w) = \varepsilon</tex><br />
}}<br />
<br />
{{Утверждение<br />
|statement=<br />
Справедливы следующие факты:<br />
# <tex>E \sim F</tex> тогда и только тогда, когда для любого <tex> n \geq 0</tex> выполняется <tex>E \sim_n F</tex><br />
# Если <tex>E \nsim F</tex>, то существует <tex> n \geq 0</tex> такой, что <tex>E \sim_n F</tex> и <tex>E \nsim_{n+1} F</tex><br />
# Если <tex>E \sim F</tex>, то для любого <tex>u \in \Sigma^*</tex>, <tex>(E \cdot u) \sim (F \cdot u)</tex>.<br />
# <tex>E \sim_{n} F</tex>, тогда и только тогда, когда для любого <tex>u \in \Sigma^*</tex>, где <tex>|u| \leq n</tex>, <tex>(E \cdot u) \sim_{n-|u|} (F \cdot u)</tex>.<br />
# Если <tex>E \sim_{n} F</tex> и <tex>0 \leq m < n</tex>, то <tex>E \sim_{m} F</tex>.<br />
# Если <tex>E \sim_{n} F</tex> и <tex>F \nsim_{n} G</tex>, то <tex>E \nsim_{n} G</tex>.<br />
}}<br />
<br />
{{Определение<br />
|definition=Для каждого стекового символа <tex>X</tex> словом <tex>w(X)</tex> называется самое короткое слово в множестве <tex>\{u : (X \cdot u) = \varepsilon \}</tex><br />
}}<br />
<br />
{{Определение<br />
|definition=<tex>E = E_1G_1 + ... + E_nG_n</tex> находится в форме голова/хвост, если голова <tex>E_1 + ...+E_n</tex> допустима и хотя бы один <tex>E_i= \emptyset</tex>, и каждый хвост <tex>G_i = \emptyset</tex>.<br />
}}<br />
<br />
Приведём некоторые свойства формы голова/хвост. Эквивалентность и n-эквивалентность языков согласуются с операциями <tex>+</tex> и суммы. Следовательно, форма голова/хвост позволяет подставить эквивалентное выражение в хвост (т.к. допустимость сохраняется).<br />
<br />
{{Утверждение<br />
|statement=<br />
Пусть <tex>E = E_1G_1 + ... + E_nG_n</tex>, тогда справедливы следующие факты:<br />
# Если <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><br />
# Если <tex>(E_i \cdot u) = \emptyset</tex>, то <tex>(E \cdot u) = (E_1 \cdot u)G_1 + ... + (E_n \cdot u)G_n</tex>.<br />
# Если <tex>H_i \neq \emptyset, 1 \leq i \leq n</tex>, то <tex>E_1H_1 + ... + E_nH_n</tex> в форме голова/хвост.<br />
# Если каждая <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 + ... + E_nH_n</tex>.<br />
# Если <tex>H_i \sim G_i, 1 \leq i \leq n</tex>, то <tex>E \sim E_1H_1 + ... + E_nH_n</tex>.<br />
}}<br />
<br />
Две конфигурации могут иметь одинаковые головы и разные хвосты, или одинаковые хвосты и различие в головах. Если <tex>E</tex> представлена в форме голова/хвост<tex>E_1G_1 + ... + E_nG_n</tex> и <tex>F</tex> имеет схожую форму голова/хвост <tex>F_1G_1 + ... + E_nF_n</tex>, имеющая тот же самый хвост. Несоответствие между <tex>E</tex> и <tex>F</tex>, соответственное этому представлению - это <tex>max\{|E_i|, |F_i| : 1 \leq i \leq n\}</tex>. Если несоответствие равно 0, то конфигурации одинаковы.<br />
<br />
'''Замечание:''' любая пара конфигураций <tex>E</tex> и <tex>F</tex> имеет форму голова/хвост включающую в себя одинаковые хвосты: <tex> E = EG</tex> и <tex>F = FG</tex>, где <tex>G = \varepsilon</tex>.<br />
<br />
{{Определение<br />
|definition= Если <tex>E = E_1G_1 + ... + E_nG_n</tex> и <tex>F = F_1F_1 + ... + F_nF_n</tex>, тогда <tex>F</tex> в его форме голова/хвост - '''хвостовое дополнение <tex>E</tex>''' в его форме голова/хвост обеспечивается <tex>H_i = K^i_1G_1 + ... + K^i_nG_n, 1 \leq i \leq m</tex>. Когда <tex>F</tex> - хвостовое дополнение <tex>E</tex>, относящиеся к нему дополнение <tex>e</tex> - кортеж из m элементов <tex>(K^1_1+...+K_n^1,...,K_1^m +...+K_n^m)</tex> без <tex>G_is</tex>, и говорится, что <tex>F</tex> дополняет <tex>E</tex> с помощью <tex>e</tex>.<br />
}}<br />
<br />
Можно рассматривать дополнения как матрицы. Если <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>(в смысле умножения матриц).<br />
<br />
Особый случай расширения возникает когда хвосты одинаковы. Если <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> (аналог единичной матрицы).<br />
<br />
== Процедура проверки ==<br />
Процедура для проверки <tex>E \sim F</tex> - направленное дерево доказательства из выражений, имеющие графическое представление, со стартовой целью <tex>E \doteq F</tex>. Чтобы проверить конфигурации на эквивалентность мы будем разбивать выражения на подвыражения используя правила вывода. Существует всего три правила вывода:<br />
[[Файл:unf_600.jpg]]<br />
<br />
где <tex>C</tex> - это условие:<br />
# Каждая <tex>E_i \neq \varepsilon</tex> и хотя бы одна <tex>H_i \neq \varepsilon</tex>.<br />
# Имеется ровно <tex>max \{ |w(X_i)| : E_i \neq \emptyset , 1 \leq i \leq k \}</tex> применений <tex>UNF</tex> между верхним и нижним выражением, и не применяются другие правила.<br />
# Если <tex>u</tex> - это слово относящиеся к полседовательности операция <tex>UNF</tex>, то <tex>E_i = (X_i \cdot u)</tex> для каждого <tex>i : 1 \leq i \leq k \</tex>.<br />
<br />
<tex>UNF</tex> - означает развертывание(англ. ''unfold''), редуцирует выражение <tex>E \doteq F</tex> на подвыражения <tex>(E \cdot a) \doteq (F \cdot a)</tex> для каждого <tex>a</tex> из алфавита. Если исходное выражение истинно, то истинны и его подвыражения. Более строгая версия этого факта зафиксирована в следующих фактах:<br />
# Если <tex>E \sim F</tex> и <tex>a \in \sigma</tex>, то <tex>(E \cdot a) \sim (F \cdot a)</tex>.<br />
# Если <tex>E \nsim_{m+1} F</tex>, то для какого-то <tex>a \in \sigma</tex> выполняется <tex>(E \cdot a) \nsim_m (F \cdot a)</tex><br />
<br />
Применение <tex>BAL</tex> использует <tex>F</tex>, если <tex>F</tex> - конфигурация в исходном выражении правила вывода. Если есть успешное представление, корень которого является ложным, то существует ветвь таблицы, внутри которой каждое подвыражение является ложной. Если два исходных выражения принадлежат последующей ветке, то подвыражение сохраняет уровень ложности второй предпосылки. Запишем это более строго:<br />
<br />
{{Утверждение<br />
|statement=<br />
Справедливы следующие факты о <tex>BAL</tex>:<br />
# Если <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>.<br />
# Если <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>.<br />
}}<br />
<br />
{{Теорема<br />
|about=о расширении<br />
|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>. <br />
Пусть расширения <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>. <br />
<br />
Если для каждое выражение <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>,<br />
то <tex>h(2^n)</tex> верно на уровне <tex>m</tex>.<br />
}}<br />
{{Определение<br />
|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>.<br />
}}<br />
{{Определение<br />
|definition=Пусть ветка доказательства состоит из выражений <tex>g(0),...,g(n)</tex>, где <tex>g(0)</tex> - корневое выражение. Выражение <tex>g(n)</tex> - это финальное выражние находящиеся одном из следующих условий:<br />
# Если <tex>g(n)</tex> - это тождество <tex>E \doteq E</tex>, то <tex>g(n)</tex> - это успешное финальное выражение.<br />
# Если <tex>g(n)</tex> удовлетворяет теореме о расширении, то <tex>g(n)</tex> - это успешное финальное выражение.<br />
# Если <tex>g(n)</tex> имеет форму <tex>E \doteq \emptyset</tex> или <tex>\emptyset \doteq E</tex> (и <tex>E \neq \emptyset</tex>), тогда <tex>g(n)</tex> - это неуспешное финальное выражение.<br />
}}<br />
{{Лемма<br />
|statement=В бесконечной ветке доказательств состоящей из выражений <tex>g(0),...,g(n),...</tex> где <tex>g(0)</tex> - корневое выражение, существует такое <tex>n</tex>, что <tex>g(n)</tex> - финальное выражение.<br />
}}<br />
<br />
Введём несложную '''процедуру проверки <tex>E \sim F</tex>''', и зададим её пошагово.<br />
# '''Шаг <tex>0</tex>:''' начинаем с корневого выражение <tex>g(0)</tex>, <tex>E \doteq F</tex>, что является вершиной ветвления ветки <tex>g(0)</tex>.<br />
# '''Шаг <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>, которая не является финальной целью, применяем следующие правило, и подвыражения, получившиеся в результате, - новые вершины ветвления расширенных веток.<br />
<br />
{{Теорема<br />
|statement=Справедливы следующие факты:<br />
# Если <tex>E \nsim F</tex>, то процедура проверки вернёт "некорректное представление".<br />
# Если <tex>E \sim F</tex>, то процедура проверки вернёт "корректное представление".<br />
}}</div>Oxygen31http://neerc.ifmo.ru/wiki/index.php?title=%D0%A4%D0%B0%D0%B9%D0%BB:Unf_600.jpg&diff=59757Файл:Unf 600.jpg2017-01-16T18:40:52Z<p>Oxygen31: </p>
<hr />
<div></div>Oxygen31http://neerc.ifmo.ru/wiki/index.php?title=%D0%A4%D0%B0%D0%B9%D0%BB:Unf_balr_ball.png&diff=59756Файл:Unf balr ball.png2017-01-16T18:35:01Z<p>Oxygen31: </p>
<hr />
<div></div>Oxygen31