Изменения

Перейти к: навигация, поиск
Нет описания правки
<tex>TQBF=\{Q_1 x_1 Q_2 x_2 \cdots Q_n x_n \phi(x_1, x_2, \dots, x_n), Q_i \in \{\forall, \exists\}\}</tex>
}}
Чтобы доказать, что <tex>TQBF \in PSPSPACE-complete</tex> необходимо показать что:
{{Лемма
|about=1
|statement=<tex>TQBF \in PSPSPACSE</tex>|proof=Чтобы доказать это просто приведём программу, которая требует <tex>O(n)</tex> дополнительной памяти и работает за конечное время. <tex>solve(Q_1 x_1 Q_2 x_2 \cdots Q_n x_n \phi(x_1, x_2, \dots, x_n))</tex> '''if''' <tex>Q_1 == \forall</tex> '''return''' <tex>solve(Q_2 x_2 \cdots Q_n x_n \phi(0, x_2, \dots, x_n)) \land solve(Q_2 x_2 \cdots Q_n x_n \phi(1, x_2, \dots, x_n))</tex> '''if''' <tex>Q_1 == \exists</tex> '''return''' <tex>solve(Q_2 x_2 \cdots Q_n x_n \phi(0, x_2, \dots, x_n)) \lor solve(Q_2 x_2 \cdots Q_n x_n \phi(1, x_2, \dots, x_n))</tex>Эта программа требует <tex>O(n)</tex> дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — <tex>n</tex>
}}
{{Лемма
|about=2
|statement=<tex> \forall L \in PS \Rightarrow L \leq_p TQBF</tex>
|proof=Рассмотрим какой-то язык <tex>L \in PSPACE</tex>. Построим такую функцию <tex>f : \forall x \in L \Leftrightarrow f(x) \in TQBF</tex>
}}
68
правок

Навигация