В цикле <tex>(1)</tex> перебираются все ''Prover'' 'ы, которые отвечают на <tex>f(n)</tex> запросов, каждый ответ имеет размер <tex>p(n)</tex>. В цикле <tex>(2)</tex> перебираются все вероятностные ленты размера <tex>p(n)</tex>. Так как <tex>V</tex> {{---}} корректен, то если нашелся ''Prover'', при котором <tex>V</tex> допускает слово с вероятностью, большей <tex>\frac{2}{3}</tex>, то данное слово принадлежит <tex>L</tex>, иначе {{---}} не принадлежит. Очевидно, что данная программа требует полином дополнительной памяти. Значит <tex>L \in \mathrm{PS}</tex>, следовательно <tex>\mathrm{IP} \subset \mathrm{PS}</tex>.
* <tex>\mathrm{PS} \subset \mathrm{IP}</tex>
}}
== Формулировка =='''[[Класс IP|IP]]''' = '''[[Класс PS|PS]]'''== Доказательство ===== IP ⊂ PS ===Рассмотрим язык Докажем, что <tex>L \mathrm{TQBF} \in \mathrm{IP}</tex>. Чтобы детерминированная машина Тьюринга Так как <tex>m</tex> могла установить принадлежность слова <tex>x</tex> языку <tex>L\mathrm{TQBF} \in \mathrm{PSC}</tex>, ей нужно перебрать все ответы <tex>P</tex> и вероятностные ленты <tex>V</tex>, просимулировав <tex>V</tex> с этими данными и посчитав вероятность допуска. Ясното из этого будет следовать, что эти действия потребуют не более <tex>p(|x|)</tex> памяти, а значит <tex>L \in mathrm{PS</tex>.=== PS ⊂ IP ===Докажем, что язык <tex>TQBF } \subset \in mathrm{IP</tex>. Этого достаточно, так как <tex>TQBF \in PSC}</tex>.
Введем следующую арифметизацию булевых формул с кванторами:* Пусть дана формула <tex>Q_1 \lnot x ldots Q_m \to 1-X</tex>* <tex>x \land y \to XY</tex>x* <tex>x \lor y \to X+Y-XY = 1-phi(1-X)(1-Y)</tex>* <tex>\exists x \varphi(x) \to \sum\limits_{X=0}^{1} A_\varphi(X)</tex>x_1, где <tex>A_\varphi</tex> — полиномldots , получившийся в результате арифметизации <tex>\varphi</tex>* <tex>\forall x \varphi(x) \to \prod\limits_{X=0}^{1} A_\varphi(Xx_m)</tex>Результат этого выражения будет ненулевым в том и только . В процессе [[Арифметизация булевых формул с кванторами|арифметизации]] она перейдет в том случае, если исходная формула была истинна. Рассмотрим пример: <tex>R_1 \varphi=\forall x_1 \forall x_2 \cdots \forall x_{k-1} \exists x_k (x_k \lor \lnot x_k)</tex> <tex>ldots R_m A_\varphi = \prod\limits_{X_1=0}^{1}\prod\limits_{X_2=0}^{1}\cdots \prod\limits_{X_{k-1}=0}^{1}\sum\limits_{X_k=0}^1phi(1-X_k(1-X_k)) = 2^{2^{(k-1)}}</tex>Для записи этого числа нужно <tex>2^{(k-1)}</tex> бит. Если <tex>k x_1,\gg \log|\varphi|</tex>ldots, это число невозможно передать за полиномиальное относительно длины исходной формулы время. Чтобы избежать таких больших чисел, приходится проводить все операции по какому-нибудь простому модулю <tex>p</tex>. Начало интерактивного протокола: * ''P'' выбирает простое <tex>p</tex> и <tex>k \equiv A_\psi \pmod{p}</tex> и посылает их ''V'' (<tex>p</tex> посылается вместе с его сертификатом простотыx_m).* ''V'' проверяет <tex>p</tex> на простоту, а <tex>k</tex> на неравенство нулю.Хотелось бы воспользоваться Воспользуемся протоколом из , описанным в [[Sharp SATЛемма о соотношении coNP и IP|доказательства доказательстве принадлежности #SAT к классу IP]]. Для этого необходимо, проверяя чтобы степень полиномов <tex>A_i(1)\cdot A_i(0)=A_x_{i-+1}(r_{i})</tex> в случае, когда <tex>x_i</tex> связан квантором была полиномиальной относительно длины входа. Преобразуем выражение с помощью оператора линеаризации к виду <tex>R_1 L_1 \ldots R_i L_1 L_2 \ldots L_i \ldots R_m L_1 L_2 \forall</tex>, и <tex>A_i(1)+A_i(0)=ldots L_m A_{i-1}\phi(r_{i}x_1,\ldots,x_m)</tex> для квантора <tex>\exists</tex>. К сожалению, сразу этот протокол применить нельзяРазмер новой формулы не превосходит квадрата исходной, потому что произведение может увеличить степень полинома в два раза, а это может потребовать передачи по протоколу полиномов экспоненциальной длины, что не уложится по временипревосходит двух. Поэтому потребуемТогда, используя условия, чтобы между появлением переменной описанные в [[Арифметизация булевых формул с кванторами|леммах 2 и первым ее использованием было не более одного квантора <tex>\forall</tex>3]], для проверки ответов, присылаемых ''Prover'' 'ом, можно построить искомый протокол. Для этого заменим все суффиксы вида Значит <tex>\forall x_mathrm{i+1TQBF} \tau(x_1, x_2, in \ldots, x_i, x_mathrm{i+1IP})</tex> на , следовательно <tex>\forall x_mathrm{i+1PS} \exists x_1',\ldots,x_i'(x_1=x_1')\land(x_2=x_2')\land subset \ldots \land(x_i=x_i')\land \tau(x_1', x_2', \ldots, x_i', x_mathrm{i+1IP})</tex>. Это преобразование не изменит выполнимости формулы, количество ее переменных увеличится лишь в полином от их первоначального количества раз, а сама формула тоже увеличится не более, чем полиномиально. Теперь можно использовать протокол из [[Sharp SAT|#SAT]] для получившейся формулы}}, передаваться будут полиномы константной степени.
