68
правок
Изменения
Нет описания правки
|about=2
|statement=<tex> \forall L \in PS , L \leq_p TQBF</tex>
|proof=Рассмотрим какой-то язык <tex>L \in PSPACE</tex>. Построим функцию <tex>f \colon \forall x \in L \Leftrightarrow f(x) \in TQBF</tex>.
Так как <tex>L \in PSPACE</tex>, то существует какая-то детерминированная машина Тьюринга <tex>M</tex>, которая его распознаёт за полиномиальное от размера входа время.
Пусть <tex>I</tex> — мгновенное описание <tex>M</tex>, тогда выражение <tex>\exists I</tex> обозначает <tex> (\exists x_1) (\exists x_2)\cdots(\exists x_n)</tex>, где <tex>\{x_i\}</tex> — все переменные мгновенного описания <tex>M</tex>. Аналогично выражение <tex> \forall I</tex> обозначает <tex> (\forall x_1) (\forall x_2)\dots(\forall x_n)</tex>. Теперь рассмотрим два мгновенных описание <tex>M: A</tex> и <tex>B</tex>. Напишем рекурсивную функцию <tex>\phi(A, B, t)</tex>, которая будет переводить утверждение <tex>A\vdash^tB</tex> в TQBF за полиномиальное относительно длины входа время.
<tex>\phi(A, B, t) = \\ (\exists R) (\forall U) (\forall V) \ \{\phi(U, V, t/2) \lor [\neg(A = U \land R = V) \land \neg(R = U \land B = V)]\}</tex> :Переменые <tex> U </tex> и <tex>V</tex> важны только как пары <tex> (A, R)</tex> и <tex>(R, B )</tex>, поэтому для всех остальных вариантов выражение <tex>[\neg(A = U \land R= V) \land \neg(A R = R U \land B = V)]</tex> будет истинно. Если <tex>A = U \land R = V</tex> то чтобы <tex>\phi(A, B, t)</tex> было истино необходимо наличие такого мгновенного описания <tex>R</tex> чтобы были выполнены два утверждения: <tex>A\vdash^{t/2}R</tex> и <tex>R\vdash^{t/2}B</tex> .
Заметим, что размер функции <tex>\phi(a, B, t)</tex> равен размеру <tex>\phi(A, B, t/2)</tex> с константной добавкой <tex>(\exists R) (\forall U) (\forall V) \ \{\ * \lor [\neg(A = U \land B = R) \land \neg(A = R \land B = V)]\}</tex> .
Теперь мы можем записать функцию <tex>f(M, w)</tex>, которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w</tex> в <tex>TQBF</tex>.
