Изменения

Перейти к: навигация, поиск
м
Нет описания правки
|statement=<tex>TQBF \in \mathrm{PSH}</tex>.
|proof=Рассмотрим язык <tex>L \in \mathrm{PS}</tex>.
Построим такую функцию <tex>f</tex>, что <tex>x \in L \Leftrightarrow f(x) \in TQBF</tex> и <tex>T(f, x) \le p(|x|)</tex>, где <tex>p</tex> — полином.
Так как <tex>L \in \mathrm{PS}</tex>, то существует детерминированная машина Тьюринга <tex>M</tex>, распознающая его с использованием памяти полиномиального размера. Будем считать, что длина ленты машины <tex>M</tex> есть <tex>r(|x|)</tex>, где <tex>r</tex> — полином, а <tex>n</tex> — длина входа. Пусть <tex>\Omega = |\Sigma \cup Q|</tex>.
Пусть <tex>I</tex> — конфигурация <tex>M</tex>. Размер Конфигурация однозначно задаётся позицией и содержанием рабочей ленты. Введём обозначение <tex>x_{I,i,c}</tex> — в конфигурации равен <tex>\Omega nI</tex> на <tex>i</tex>-том месте стоит символ <tex>c</tex>, где . Тогда размер конфигурации равен <tex>\Omega r(n)</tex> длина входа. Тогда Следовательно всего конфигураций <tex>2^{\Omega r(n)}</tex>.
Введём обозначение <tex>x_{I,i,c}</tex> — в конфигурации <tex>I</tex> на <tex>i</tex>-том месте стоит символ <tex>c</tex>.Тогда выражение Под выражением <tex>\exists I</tex> обозначает будем понимать <tex> \exists x_{I,1,c_1} \, \exists x_{I,1,c_2} \ldots \exists x_{I,1,c_\Omega} \, \exists x_{I,2,c_1} \ldots</tex> Аналогично выражение <tex> \forall I</tex> обозначает <tex> \forall x_{I,1,c_1} \, \forall x_{I,1,c_2} \ldots \forall x_{I,1,c_\Omega} \, \forall x_{I,2,c_1} \ldots</tex>
Рассмотрим функцию <tex>\phi(A, B, t)</tex>, проверяющую следующее условие: конфигурация <tex>B</tex> достижима из конфигурации <tex>A</tex> не более, чем за <tex>2^t</tex> шагов.
Теперь мы можем записать функцию <tex>f(M, w)</tex>, которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w</tex> в формулу из <tex>TQBF</tex>.
<tex>f(M, w) = \exists S \, \exists F \, (S - start) \land (F - accept) \land \phi(S, F, log_2(2^{\Omega r(n)})))</tex>.
Выражения <tex>S - start</tex> и <tex>F - accept</tex> можно записать следующим образом:
<tex>S - start = x_{S, 1, w[1]} \land x_{S, 2, w[2]} \land \ldots \land x_{S, |w|, w[|w|]} \land x_{S, |w| + 1, B} \ldots \land x_{S, \Omega r(n) , B}</tex>.
<tex>F - accept = x_{S, |w| + 1, \#_y} \lor \ldots \lor x_{S, \Omegar(n), \#_y}</tex>.
Докажем, что сведение <tex>f</tex> корректно.
Если <tex>w \in L</tex>, то существует путь из стартовой конфигурации в финишную, причём длины не более, чем <tex>2^{\Omega r(n)}</tex>, а значит формула <tex>f(M, w)</tex> верна.
Если формула <tex>f(M, w)</tex> оказалась верна, то существует путь из стартовой конфигурации в финишную длины не более, чем <tex>2^{\Omega r(n)}</tex>. Значит, ДМТ <tex>M</tex> допускает слово <tex>w</tex>. Тогда <tex>w \in L</tex>.
Таким образом, <tex>TQBF \in \mathrm{PSH}</tex>.

Навигация