Изменения

{{Теорема|author== Формулировка ==Шамир'''[[Класс IP|statement=<tex>\mathrm{IP]]''' } = '''[[Класс \mathrm{PS}</tex>|PS]]'''== Доказательство =proof==== * <tex>\mathrm{IP } \subset \mathrm{PS}</tex> ===Рассмотрим язык <tex>L \in \mathrm{IP}</tex>. Чтобы детерменированная машина Тьюринга Пусть <tex>mV</tex> могла установить принадлежность слова {{---}} ''Verifier'', соответствующий <tex>xL</tex> языку , <tex>Lp(n)</tex>{{---}} время его работы, ей нужно перебрать все ответы <tex>Pf(n)</tex> и вероятностные ленты {{---}} количество его запросов к ''Prover'' 'у. Напишем программу, распознающую язык <tex>VL</tex>, просимулировав на полиномиальной памяти. <tex>VU(x)</tex> с этими данными и посчитав вероятность допуска. Ясно, что эти действия потребуют не более <tex>p(n \leftarrow |x|)</tex> памяти, а значит '''for''' <tex>L P \in PSleftarrow Prover[f(n), p(n)]</tex>. //(1)=== <tex>PS count \subset IPleftarrow 0</tex> ===Докажем, что язык '''for''' <tex>TQBF r \in IP\{0, 1\}^{p(n)}</tex>. Этого достаточно //(2) '''if''' <tex>V(x, так как r)\bigm{|}_{P} = 1</tex> <tex>TQBF count</tex>++ '''if''' <tex dpi = "160">\in PSCfrac{count}{2^{p(n)}} \ge \frac{2}{3}</tex>. '''return''' 1 '''return''' 0

Введем следующую арифметизацию булевых формул с кванторами:* В цикле <tex>\lnot x \to (1-X)</tex>* перебираются все ''Prover'' 'ы, которые отвечают на <tex>x \land y \to XYf(n)</tex>* запросов, каждый ответ имеет размер <tex>x \lor y \to X+Y-XY = 1-p(1-Xn)</tex>. В цикле <tex>(1-Y2)</tex>* перебираются все вероятностные ленты размера <tex>\exists x \varphip(xn) </tex>. Так как <tex>V</tex> {{---}} корректен, то если нашелся ''Prover'', при котором <tex>V</tex> допускает слово с вероятностью, большей <tex>\to frac{2}{3}</tex>, то данное слово принадлежит <tex>L</tex>, иначе {{---}} не принадлежит. Очевидно, что данная программа требует полином дополнительной памяти. Значит <tex>L \sumin \limits_mathrm{X=0PS}^</tex>, следовательно <tex>\mathrm{1IP} A_\varphi(X)subset \mathrm{PS}</tex>.* <tex>\forall x \varphi(x) \to mathrm{PS} \prodsubset \limits_{X=0}^mathrm{1IP} A_\varphi(X)</tex>Результат этого выражения будет ненулевым в том и только в том случае, если исходная формула была истина.

Рассмотрим пример: Докажем, что <tex>\varphi=mathrm{TQBF} \forall x_1 in \forall x_2 \cdots \forall x_mathrm{k-1IP} \exists x_k (x_k \lor \lnot x_k)</tex> . Так как <tex>A_\varphi = \prod\limits_{X_1=0}^{1}\prod\limits_{X_2=0}^{1}\cdots \prod\limits_{X_{k-1}=0}^mathrm{1TQBF}\sumin \limits_{X_k=0}^1(1-X_k(1-X_k)) = 2^{2^mathrm{(k-1)}PSC}</tex>Для записи , то из этого числа нужно будет следовать, что <tex>2^\mathrm{(k-1)PS}</tex> бит. Если <tex>k \gg subset \log|\varphi|</tex>, это число невозможно передать за полиномиальное относительно длины исходной формулы время. Чтобы избежать таких больших чисел, приходится проводить все операции по какому-нибудь простому модулю <tex>pmathrm{IP}</tex>.

Начало интерактивного протокола: * ''P'' выбирает простое Пусть дана формула <tex>pQ_1 \ldots Q_m \phi(x_1, \ldots ,x_m)</tex> и . В процессе [[Арифметизация булевых формул с кванторами|арифметизации]] она перейдет в <tex>k R_1 \equiv ldots R_m A_\psi phi(x_1,\pmod{p}</tex> и посылает их ''V'' (<tex>p</tex> посылается вместе с его сертификатом простотыldots,x_m).* ''V'' проверяет <tex>p</tex> на простоту, а <tex>k</tex> на неравенство нулю.Хотелось бы воспользоваться Воспользуемся протоколом из , описанным в [[#SATЛемма о соотношении coNP и IP|доказательства доказательстве принадлежности #SAT к классу IP]]. Для этого необходимо, лишь проверяя чтобы степень полиномов <tex>A_i(1)\cdot A_i(0)=A_x_{i-+1}(r_{i})</tex> в случае, когда по была полиномиальной относительно длины входа. Преобразуем выражение с помощью оператора линеаризации к виду <tex>X_iR_1 L_1 \ldots R_i L_1 L_2 \ldots L_i \ldots R_m L_1 L_2 \ldots L_m A_\phi(x_1,\ldots,x_m)</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',subset \ldots,x_i'(x_1=x_1')\land(x_2=x_2')\land \ldots \land(x_i=x_i')\tau(x_1', x_2', \ldots, x_i', x_mathrm{i+1IP})</tex>. От такого преобразования количество переменных увеличится лишь в полином от их первоначального количества раз, сама формула тоже увеличится не более, чем полиномиально. Теперь после арифметизации по протоколу из [[#SAT]] будут передаваться полиномы не выше второй степени.}}