Примеры неразрешимых задач: задача о выводе в полусистеме Туэ — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 6: Строка 6:
  
 
Подстановка <tex>\alpha_i\rightarrow \beta_i</tex> интерпретируется как правило вывода <tex>R_i</tex> следующим образом:
 
Подстановка <tex>\alpha_i\rightarrow \beta_i</tex> интерпретируется как правило вывода <tex>R_i</tex> следующим образом:
<tex>\gamma \vDash \delta</tex> по <tex>R_i</tex> , если слово <tex>\delta</tex> получается путем подстановки какого-нибудь <tex>\beta_i</tex> вместо какого-то вхождения <tex>\alpha_i</tex> в <tex>\gamma</tex>.
+
<tex>\gamma \vDash \delta</tex> по <tex>R_i</tex> , если слово <tex>\delta</tex> получается путем подстановки <tex>\beta_i</tex> вместо какого-то вхождения <tex>\alpha_i</tex> в <tex>\gamma</tex>.
  
 
Вывод <tex>\beta</tex> из <tex>\alpha</tex> - цепочка <tex>\alpha\vDash\epsilon_1\vDash\epsilon_2\vDash .. \vdash\beta</tex>, где каждое <tex>\epsilon_j</tex> получается из <tex>\epsilon_{j-1}</tex> некоторой подстановкой.
 
Вывод <tex>\beta</tex> из <tex>\alpha</tex> - цепочка <tex>\alpha\vDash\epsilon_1\vDash\epsilon_2\vDash .. \vdash\beta</tex>, где каждое <tex>\epsilon_j</tex> получается из <tex>\epsilon_{j-1}</tex> некоторой подстановкой.

Версия 14:23, 14 января 2014

Определение:
Полусистема Туэ (semi-Thue system) - это формальная система, определяемая алфавитом [math]A[/math] и конечным множеством подстановок вида [math]\alpha_i\rightarrow \beta_i[/math], где [math]\alpha_i, \beta_i[/math] - слова из [math]A[/math].


Подстановка [math]\alpha_i\rightarrow \beta_i[/math] интерпретируется как правило вывода [math]R_i[/math] следующим образом: [math]\gamma \vDash \delta[/math] по [math]R_i[/math] , если слово [math]\delta[/math] получается путем подстановки [math]\beta_i[/math] вместо какого-то вхождения [math]\alpha_i[/math] в [math]\gamma[/math].

Вывод [math]\beta[/math] из [math]\alpha[/math] - цепочка [math]\alpha\vDash\epsilon_1\vDash\epsilon_2\vDash .. \vdash\beta[/math], где каждое [math]\epsilon_j[/math] получается из [math]\epsilon_{j-1}[/math] некоторой подстановкой.


Определение:
Проблема останова (halting problem) - это задача, в которой требуется по заданной программе проверить завершиться ли она на определенных входных данных.


Теорема:
Проблема останова неразрешима.
Доказательство:
[math]\triangleright[/math]
Доказательство теоремы приведено в примере использования теоремы о рекурсии.
[math]\triangleleft[/math]
Теорема:
В заданной полусистеме Туэ задача вывода из слова [math]\alpha [/math] слово [math] \beta[/math] (word problem for semi-Thue systems) неразрешима.
Доказательство:
[math]\triangleright[/math]

Сведем (прим. m-сводимость) неразрешимую задачу проблемы останова к нашей. Для этого построим по структуре данной из проблемы останова МТ (прим. Машина Тьюринга) полусистему Туэ. Пусть [math] q_1 [/math] — стартовое состояние, [math] q_n [/math] — допускающее состояние МТ. Для построение искомой полусистемы будем описывать текущее состояние МТ с помощью строки [math] |xqy| [/math] , где [math] q [/math] — текущее состояние автомата, [math] xy [/math] — строка, записанная на ленте. Пусть [math] s [/math] — последний символ строки [math] x [/math], а [math] t [/math] — первый символ строки [math] y [/math]. При этом головка указывает на символ [math] t [/math]. Тогда текущий шаг МТ можно описать с помощью следующих преобразований строк:

[math] sqt \rightarrow \begin{cases} q'st' & \text{if } \leftarrow \\ sq't' & \text{if } \downarrow \\ st'q' & \text{if } \rightarrow \end{cases} [/math]

В силу конечности множеств состояний автомата ([math] Q [/math]) и алфавита ([math] T [/math]) добавим все подобные правила (представленные выше) в нашу полусистему. Заметим, что в МТ лента у нас бесконечна. Поэтому добавим в нашу систему следующие правила, которые будут эмулировать расширение слова на ленте за счет сдвига маркера [math] | [/math]:

[math]q| \rightarrow q0| [/math] и [math]|q \rightarrow |0q [/math] для [math] \forall q \in Q \setminus \{q_n\}[/math]

И наконец добавим в наш набор те правила, которые позволят нам из конфигурации, в которой присутствует допускающее состояние [math] q_n [/math], получить уникальное слово. Это необходимо, чтобы мы смогли построить критерий в терминах полуситсемы Туэ того, что из стартовой конфигураций наша программа корректно завершается. Имеем следующие правила:

[math]q_nt \rightarrow q_n [/math]

[math]q_n| \rightarrow w| [/math]

[math] tw \rightarrow w [/math] для [math] \forall t \in T[/math].

Имея этот набор правил можем составить упомянутый выше критерий: программа корректно завершиться на данном на ленте входном слове [math] u [/math], если в построенной полусистеме [math] |q_1u| \vDash ^*|w| [/math]. Таким образом из разрешимости этой задачи следовала бы разрешимость задачи останова. Соответсвенно задача о выводе в полусистеме Туэ алгоритмически неразрешима.
[math]\triangleleft[/math]

Источники