70
правок
Изменения
Нет описания правки
{{Теорема
|author=Шамир
|statement=<tex>\mathrm{IP} = \mathrm{PS}</tex>
|proof=
* <tex>\mathrm{IP} \subset \mathrm{PS}</tex>
Рассмотрим язык <tex>L \in \mathrm{IP}</tex>, а также ''Verifier'' и ''Prover'', соответствующие этому языку. Так как ''Verifier'' ограничен полиномиальным временем работы, то можно считать, что размер вероятностной ленты, размер ответов ''Prover'' 'а и количество дополнительной памяти, используемой ''Verifier'' 'ом тоже ограничены некоторым полиномом. Построим программу, которая будет перебирать все возможные вероятностные ленты и для каждой из них будет симулировать работу ''Verifier'' 'а, перебирая все возможные ответы ''Prover'' 'а, а затем вернет наиболее часто встречающийся результат, возвращаемый ''Verifier'' 'ом. Данная программа использует полиномиальное количество дополнительной памяти. Значит <tex>L \in \mathrm{PS}</tex>. Поэтому <tex>\mathrm{IP} \subset \mathrm{PS}</tex>
* <tex>\mathrm{PS} \subset \mathrm{IP}</tex>
}}
== Формулировка ==
'''[[Класс IP|IP]]''' = '''[[Класс PS|PS]]'''
Введем следующую арифметизацию булевых формул с кванторами:
* <tex>\lnot x \to 1-X</tex>
* <tex>x \land y \to XY</tex>x
* <tex>x \lor y \to X+Y-XY = 1-(1-X)(1-Y)</tex>
* <tex>\exists x \varphi(x) \to \sum\limits_{X=0}^{1} A_\varphi(X)</tex>, где <tex>A_\varphi</tex> — полином, получившийся в результате арифметизации <tex>\varphi</tex>
