Эквивалентность ДМП-автоматов — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 1: Строка 1:
[[Нормальная форма ДМП-автомата|Предположим детерминированный строгий автомат с единственным состоянием с элементами, представленный тройкой]]: входной алфавит на ленте <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> - допустимые конфигурации.
+
[[Нормальная форма ДМП-автомата|Предположим детерминированный строгий автомат с единственным состоянием с элементами, представленный тройкой]]:
 +
* входной алфавит на ленте <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</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 : (E \cdot u) = \varepsilon \}</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>.
+
|definition=Две конфигурации <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>E</tex> и <tex>F</tex> '''<tex>n</tex>-эквивалентны'''  если они принимают одни и те же слова, длина которых не больше <tex>n</tex>:
+
|definition=Конфигурафии <tex>E</tex> и <tex>F</tex> '''<tex>n</tex>-эквивалентны''', обозначается <tex>E \sim_n F,  n \geqslant 0</tex> {{---}} они принимают одни и те же слова, длина которых не больше <tex>n</tex>:
<br>для всех слов <tex>w</tex>, таких что <tex>|w| \leq n, (E \cdot w) = \varepsilon</tex> тогда и только тогда, когда <tex>(F \cdot w) = \varepsilon</tex>
+
<br>для всех слов <tex>w</tex>, таких что <tex>|w| \leqslant n, (E \cdot w) = \varepsilon</tex> тогда и только тогда, когда <tex>(F \cdot w) = \varepsilon</tex>.
 
}}
 
}}
  
Строка 19: Строка 23:
 
|statement=
 
|statement=
 
Справедливы следующие факты:
 
Справедливы следующие факты:
# <tex>E \sim F</tex> тогда и только тогда, когда для любого <tex> n \geq 0</tex> выполняется <tex>E \sim_n F</tex>
+
# <tex>E \sim F</tex> тогда и только тогда, когда для любого <tex> n \geqslant 0</tex> выполняется <tex>E \sim_n F</tex>.
# Если <tex>E \nsim F</tex>, то существует <tex> n \geq 0</tex> такой, что <tex>E \sim_n F</tex> и <tex>E \nsim_{n+1} F</tex>
+
# Если <tex>E \nsim F</tex>, то существует <tex> n \geqslant 0</tex> такой, что <tex>E \sim_n F</tex> и <tex>E \nsim_{n+1} F</tex>.
 
# Если <tex>E \sim F</tex>, то для любого <tex>u \in \Sigma^*</tex>, <tex>(E \cdot u) \sim (F \cdot u)</tex>.
 
# Если <tex>E \sim F</tex>, то для любого <tex>u \in \Sigma^*</tex>, <tex>(E \cdot u) \sim (F \cdot u)</tex>.
# <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>.
+
# <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>.
# Если <tex>E \sim_{n} F</tex> и <tex>0 \leq m < n</tex>, то <tex>E \sim_{m} F</tex>.
+
# Если <tex>E \sim_{n} F</tex> и <tex>0 \leqslant m < n</tex>, то <tex>E \sim_{m} F</tex>.
 
# Если <tex>E \sim_{n} F</tex> и <tex>F \nsim_{n} G</tex>, то <tex>E \nsim_{n} G</tex>.
 
# Если <tex>E \sim_{n} F</tex> и <tex>F \nsim_{n} G</tex>, то <tex>E \nsim_{n} G</tex>.
 
}}
 
}}
  
 
{{Определение
 
{{Определение
|definition=Для каждого стекового символа <tex>X</tex> словом <tex>w(X)</tex> называется самое короткое слово в множестве <tex>\{u : (X \cdot u) = \varepsilon \}</tex>
+
|definition=Для каждого стекового символа <tex>X</tex> '''словом <tex>w(X)</tex>''' называется самое короткое слово в множестве <tex>\{u \mid (X \cdot u) = \varepsilon \}</tex>.
 
}}
 
}}
  
 
{{Определение
 
{{Определение
|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>.
+
|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>+</tex> и суммы. Следовательно, форма голова/хвост позволяет подставить эквивалентное выражение в хвост (т.к. допустимость сохраняется).
+
Приведём некоторые свойства формы голова/хвост. Эквивалентность и <tex>n</tex>-эквивалентность языков согласуются с операцией суммы. Следовательно, форма голова/хвост позволяет подставить эквивалентное выражение в хвост (т.к. допустимость сохраняется).
  
 
{{Утверждение
 
{{Утверждение
 
|statement=
 
|statement=
Пусть <tex>E = E_1G_1 + ... + E_nG_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) = \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 + ... + (E_n \cdot u)G_n</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 i \leq n</tex>, то <tex>E_1H_1 + ... + E_nH_n</tex> в форме голова/хвост.
+
# Если <tex>H_i  \neq \emptyset, 1 \leqslant i \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 + ... + 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 i \leq n</tex>, то <tex>E  \sim E_1H_1 + ... + E_nH_n</tex>.
+
# Если <tex>H_i  \sim G_i, 1 \leqslant i \leqslant n</tex>, то <tex>E  \sim E_1H_1 + \ldots  + E_nH_n</tex>.
 
}}
 
}}
  
Две конфигурации могут иметь одинаковые головы и разные хвосты, или одинаковые хвосты и различие в головах. Если <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, то конфигурации одинаковы.
+
Две конфигурации могут иметь одинаковые головы и разные хвосты, или одинаковые хвосты и различие в головах. Если <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, то конфигурации одинаковы.
  
 
'''Замечание:''' любая пара конфигураций <tex>E</tex> и <tex>F</tex> имеет форму голова/хвост включающую в себя одинаковые хвосты: <tex> E = EG</tex> и <tex>F = FG</tex>, где <tex>G = \varepsilon</tex>.
 
'''Замечание:''' любая пара конфигураций <tex>E</tex> и <tex>F</tex> имеет форму голова/хвост включающую в себя одинаковые хвосты: <tex> E = EG</tex> и <tex>F = FG</tex>, где <tex>G = \varepsilon</tex>.
  
 
{{Определение
 
{{Определение
|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>.
+
|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>.
 
}}
 
}}
  
 
Можно рассматривать дополнения как матрицы. Если <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''</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 = 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>E \sim F</tex> {{---}} направленное дерево доказательства из выражений, имеющие графическое представление, со стартовой целью <tex>E \doteq F</tex>. Чтобы проверить конфигурации на эквивалентность мы будем разбивать выражения на подвыражения используя правила вывода. Существует всего три правила вывода:
 
[[Файл:unf_600.jpg]]
 
[[Файл:unf_600.jpg]]
  
где <tex>C</tex> - это условие:
+
где <tex>C</tex> {{---}} это условие:
 
# Каждая <tex>E_i \neq \varepsilon</tex> и хотя бы одна <tex>H_i \neq \varepsilon</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> \max_{1 \leqslant i \leqslant k } \{ |w(X_i)| : E_i \neq \emptyset \}</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>u</tex> {{---}} это слово относящиеся к полседовательности операция <tex>UNF</tex>, то <tex>E_i = (X_i \cdot u)</tex> для каждого <tex>i : 1 \leqslant i \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>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 \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>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>BAL</tex> использует <tex>F</tex>, если <tex>F</tex> {{---}} конфигурация в исходном выражении правила вывода. Если есть успешное представление, корень которого является ложным, то существует ветвь таблицы, внутри которой каждое подвыражение является ложной. Если два исходных выражения принадлежат последующей ветке, то подвыражение сохраняет уровень ложности второй предпосылки. Запишем это более строго:
  
 
{{Утверждение
 
{{Утверждение
 
|statement=
 
|statement=
 
Справедливы следующие факты о <tex>BAL</tex>:
 
Справедливы следующие факты о <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+ \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+...+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>.
+
# Если <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>.
 
}}
 
}}
  
 
{{Теорема
 
{{Теорема
 
|about=о расширении
 
|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>.  
+
|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>.
Пусть расширения <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>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>.
  
Если для каждое выражение <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>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>,
 
то <tex>h(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>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>.
 
}}
 
}}
 
{{Определение
 
{{Определение
|definition=Пусть ветка доказательства состоит из выражений <tex>g(0),...,g(n)</tex>, где <tex>g(0)</tex> - корневое выражение. Выражение <tex>g(n)</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>E \doteq E</tex>, то <tex>g(n)</tex> {{---}} это '''успешное финальное выражение'''.
# Если <tex>g(n)</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> - это неуспешное финальное выражение.
+
# Если <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> - финальное выражение.
+
|statement=В бесконечной ветке доказательств состоящей из выражений <tex>g(0), \ldots ,g(n), \ldots </tex> где <tex>g(0)</tex> {{---}} корневое выражение, существует такое <tex>n</tex>, что <tex>g(n)</tex> {{---}} финальное выражение.
 
}}
 
}}
  
 
Введём несложную '''процедуру проверки <tex>E \sim F</tex>''', и зададим её пошагово.
 
Введём несложную '''процедуру проверки <tex>E \sim F</tex>''', и зададим её пошагово.
 
# '''Шаг <tex>0</tex>:''' начинаем с корневого выражение <tex>g(0)</tex>, <tex>E \doteq F</tex>, что является вершиной ветвления ветки <tex>g(0)</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>, которая не является финальной целью, применяем следующие правило, и подвыражения, получившиеся в результате, - новые вершины ветвления расширенных веток.
+
# '''Шаг <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>, которая не является финальной целью, применяем следующие правило, и подвыражения, получившиеся в результате, {{---}} новые вершины ветвления расширенных веток.
  
 
{{Теорема
 
{{Теорема
Строка 111: Строка 115:
 
# Если <tex>E \sim F</tex>, то процедура проверки вернёт "корректное представление".
 
# Если <tex>E \sim F</tex>, то процедура проверки вернёт "корректное представление".
 
}}
 
}}
 +
 +
== См. также ==
 +
* [[Нормальная форма ДМП-автомата]]
 +
* [[Детерминированные автоматы с магазинной памятью, допуск по пустому стеку]]
 +
* [[Детерминированные автоматы с магазинной памятью]]
 +
* [[ДМП-автоматы и неоднозначность]]
 +
 +
== Источники информации ==
 +
* [http://homepages.inf.ed.ac.uk/cps/india.pdf Colin Stirling "An Introduction to Decidability of DPDA Equivalence"]
 +
 +
[[Категория: Теория формальных языков]]
 +
[[Категория: Контекстно-свободные грамматики]]
 +
[[Категория: МП-автоматы]]

Версия 01:20, 17 января 2017

Предположим детерминированный строгий автомат с единственным состоянием с элементами, представленный тройкой:

  • входной алфавит на ленте [math]\Sigma[/math],
  • стековым алфавит [math]\Gamma[/math],
  • множеством переходов [math]\Delta[/math].

Мы предполагаем наличие полного порядка на [math]\Sigma[/math],и говорим, что слово [math]u[/math] короче слова [math]v[/math] если [math]|u| \lt |v|[/math] или [math]|u| = |v|[/math] и [math]u[/math] лексикографически меньше [math]v[/math]. Пусть [math]E, F, G,\dotsc[/math] — допустимые конфигурации.

Определение:
Конфигурация [math]E[/math] после слова [math]u[/math], обозначается [math]E \cdot u[/math] — единственная допустимая конфигурация [math]F[/math] такая что [math](E, u) \rightarrow F[/math], которая может быть и [math]\emptyset[/math].


Определение:
Язык, задаваемой конфигурацией [math]E[/math][math]L(E) = \{ E \mid (E \cdot u) = \varepsilon \}[/math].


Определение:
Две конфигурации [math]E[/math] и [math]F[/math] эквивалентны[math]L(E) = L(F)[/math], обозначается [math]E \sim F[/math].


Равенство задаваемых языков также может быть приблизительным.

Определение:
Конфигурафии [math]E[/math] и [math]F[/math] [math]n[/math]-эквивалентны, обозначается [math]E \sim_n F, n \geqslant 0[/math] — они принимают одни и те же слова, длина которых не больше [math]n[/math]:
для всех слов [math]w[/math], таких что [math]|w| \leqslant n, (E \cdot w) = \varepsilon[/math] тогда и только тогда, когда [math](F \cdot w) = \varepsilon[/math].


Утверждение:
Справедливы следующие факты:
  1. [math]E \sim F[/math] тогда и только тогда, когда для любого [math] n \geqslant 0[/math] выполняется [math]E \sim_n F[/math].
  2. Если [math]E \nsim F[/math], то существует [math] n \geqslant 0[/math] такой, что [math]E \sim_n F[/math] и [math]E \nsim_{n+1} F[/math].
  3. Если [math]E \sim F[/math], то для любого [math]u \in \Sigma^*[/math], [math](E \cdot u) \sim (F \cdot u)[/math].
  4. [math]E \sim_{n} F[/math], тогда и только тогда, когда для любого [math]u \in \Sigma^*[/math], где [math]|u| \leqslant n[/math], [math](E \cdot u) \sim_{n-|u|} (F \cdot u)[/math].
  5. Если [math]E \sim_{n} F[/math] и [math]0 \leqslant m \lt n[/math], то [math]E \sim_{m} F[/math].
  6. Если [math]E \sim_{n} F[/math] и [math]F \nsim_{n} G[/math], то [math]E \nsim_{n} G[/math].


Определение:
Для каждого стекового символа [math]X[/math] словом [math]w(X)[/math] называется самое короткое слово в множестве [math]\{u \mid (X \cdot u) = \varepsilon \}[/math].


Определение:
[math]E = E_1G_1 + \ldots + E_nG_n[/math] находится в форме голова/хвост, если голова [math]E_1 + \ldots +E_n[/math] допустима и хотя бы один [math]E_i= \emptyset[/math], и каждый хвост [math]G_i = \emptyset[/math].


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

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

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

Замечание: любая пара конфигураций [math]E[/math] и [math]F[/math] имеет форму голова/хвост включающую в себя одинаковые хвосты: [math] E = EG[/math] и [math]F = FG[/math], где [math]G = \varepsilon[/math].


Определение:
Если [math]E = E_1G_1 + \ldots + E_nG_n[/math] и [math]F = F_1F_1 + \ldots + F_nF_n[/math], тогда [math]F[/math] в его форме голова/хвост — хвостовое дополнение [math]E[/math] в его форме голова/хвост обеспечивается [math]H_i = K^i_1G_1 + \ldots + K^i_nG_n, 1 \leqslant i \leqslant m[/math]. Когда [math]F[/math] — хвостовое дополнение [math]E[/math], относящиеся к нему дополнение [math]e[/math] — кортеж из m элементов [math](K^1_1+ \ldots +K_n^1, \ldots ,K_1^m + \ldots +K_n^m)[/math] без [math]G_is[/math], и говорится, что [math]F[/math] дополняет [math]E[/math] с помощью [math]e[/math].


Можно рассматривать дополнения как матрицы. Если [math]E''[/math] расширяет [math]E'[/math] с помощью [math]e[/math] и [math]E'[/math] расширяет [math]E[/math] с помощью [math]f[/math], то [math]E''[/math] расширяет [math]E[/math] с помощью [math]ef[/math](в смысле умножения матриц).

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

Процедура проверки

Процедура для проверки [math]E \sim F[/math] — направленное дерево доказательства из выражений, имеющие графическое представление, со стартовой целью [math]E \doteq F[/math]. Чтобы проверить конфигурации на эквивалентность мы будем разбивать выражения на подвыражения используя правила вывода. Существует всего три правила вывода: Unf 600.jpg

где [math]C[/math] — это условие:

  1. Каждая [math]E_i \neq \varepsilon[/math] и хотя бы одна [math]H_i \neq \varepsilon[/math].
  2. Имеется ровно [math] \max_{1 \leqslant i \leqslant k } \{ |w(X_i)| : E_i \neq \emptyset \}[/math] применений [math]UNF[/math] между верхним и нижним выражением, и не применяются другие правила.
  3. Если [math]u[/math] — это слово относящиеся к полседовательности операция [math]UNF[/math], то [math]E_i = (X_i \cdot u)[/math] для каждого [math]i : 1 \leqslant i \leqslant k \[/math].

[math]UNF[/math] — означает развертывание(англ. unfold), редуцирует выражение [math]E \doteq F[/math] на подвыражения [math](E \cdot a) \doteq (F \cdot a)[/math] для каждого [math]a[/math] из алфавита. Если исходное выражение истинно, то истинны и его подвыражения. Более строгая версия этого факта зафиксирована в следующих фактах:

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

Применение [math]BAL[/math] использует [math]F[/math], если [math]F[/math] — конфигурация в исходном выражении правила вывода. Если есть успешное представление, корень которого является ложным, то существует ветвь таблицы, внутри которой каждое подвыражение является ложной. Если два исходных выражения принадлежат последующей ветке, то подвыражение сохраняет уровень ложности второй предпосылки. Запишем это более строго:

Утверждение:
Справедливы следующие факты о [math]BAL[/math]:
  1. Если [math]X_1H_1+ \ldots +X_kH_k \sim F[/math] и [math]E_1H_1+ \ldots +E_kH_k \sim F'[/math], тогда [math]E_1(F \cdot w(X_1))+ \ldots +X_k(F \cdot w(X_k)) \sim F'[/math].
  2. Если [math]X_1H_1+ \ldots +X_kH_k \sim_{n+m} F[/math] и [math]E_1H_1+ \ldots +E_kH_k \nsim_{n+1} F'[/math] и каждая [math]E_i \neq \varepsilon[/math] и [math]m \geqslant \max \{ |w(X_i)| \mid E_i \neq \emptyset \}[/math], то [math]E_1(F \cdot w(X_1))+ \ldots +E_k(F \cdot w(X_k)) \nsim_{n+1} F'[/math].
Теорема (о расширении):
Пусть есть два семейства выражений [math]g(i), h(i), 1 \leqslant i \leqslant 2^n[/math], и каждое выражение [math]g(i)[/math] имеет форму [math]E_1G^i_1+ \ldots +E_nG^i_n=F_1G^i_1+ \ldots +F_nG^i_n[/math] и каждое выражение [math]h(i)[/math] имеет форму [math]E_1H^i_1+ \ldots +E_nH^i_n=F_1H^i_1+ \ldots +F_nH^i_n[/math].

Пусть расширения [math]e_1, \ldots ,e_n[/math] такие, что для каждого [math]e_j[/math] и [math]i \geqslant 0, g(2^j i + 2^{j-1} + 1)[/math] расширяет [math]g(2^j i + 2^{j-1})[/math] с помощью [math]e_j[/math] и [math]h(2^j i + 2^{j-1} + 1)[/math] расширяет [math]h(2^j i + 2^{j-1})[/math] с помощью [math]e_j[/math].

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

то [math]h(2^n)[/math] верно на уровне [math]m[/math].
Определение:
Пусть ветка доказательства состоит из выражений [math]d(0), \ldots ,d(l)[/math]. Выражение [math]d(l)[/math] удовлетворяет теореме о расширении если существеют выражения [math]g(i),h(i),1 \leqslant i \leqslant 2^n[/math], и расширения [math]e_1, \ldots ,e_n[/math] как описано в теормере о расширении, и выражения принадлежат [math]\{d(0), \ldots ,d(l)\}[/math], и [math]h(2^n)[/math] — это [math]d(l)[/math] и есть хотя бы одно применение [math]UNF[/math] между выражением [math]h(2^n-1)[/math] и [math]d(l)[/math].


Определение:
Пусть ветка доказательства состоит из выражений [math]g(0), \ldots ,g(n)[/math], где [math]g(0)[/math] — корневое выражение. Выражение [math]g(n)[/math] — это финальное выражние находящиеся одном из следующих условий:
  1. Если [math]g(n)[/math] — это тождество [math]E \doteq E[/math], то [math]g(n)[/math] — это успешное финальное выражение.
  2. Если [math]g(n)[/math] удовлетворяет теореме о расширении, то [math]g(n)[/math] — это успешное финальное выражение.
  3. Если [math]g(n)[/math] имеет форму [math]E \doteq \emptyset[/math] или [math]\emptyset \doteq E[/math][math]E \neq \emptyset[/math]), тогда [math]g(n)[/math] — это неуспешное финальное выражение.
Лемма:
В бесконечной ветке доказательств состоящей из выражений [math]g(0), \ldots ,g(n), \ldots [/math] где [math]g(0)[/math] — корневое выражение, существует такое [math]n[/math], что [math]g(n)[/math] — финальное выражение.

Введём несложную процедуру проверки [math]E \sim F[/math], и зададим её пошагово.

  1. Шаг [math]0[/math]: начинаем с корневого выражение [math]g(0)[/math], [math]E \doteq F[/math], что является вершиной ветвления ветки [math]g(0)[/math].
  2. Шаг [math]n+1[/math]: Если текущая вершина ветвления [math]g(n)[/math] ветки [math]g(0), \ldots ,g(n)[/math] — это неуспешное финальное выражение, то прерываемся и возвращаем "некорректное представление";
    Если каждая вершина ветвления [math]g(n)[/math] ветки [math]g(0), \ldots ,g(n)[/math] — успешное финальное выражение, тогда возвращаем "корректное представление";
    Иначе для каждой вершины ветвления [math]g(n)[/math] ветки [math]g(0), \ldots ,g(n)[/math], которая не является финальной целью, применяем следующие правило, и подвыражения, получившиеся в результате, — новые вершины ветвления расширенных веток.
Теорема:
Справедливы следующие факты:
  1. Если [math]E \nsim F[/math], то процедура проверки вернёт "некорректное представление".
  2. Если [math]E \sim F[/math], то процедура проверки вернёт "корректное представление".

См. также

Источники информации