5.2. Язык LS, пункт 6.
6. Для тех, кто решил читать заметку с этого пункта, дадим сводную информацию. Язык LS из класса NP соответствует следующему алгоритму проверки (по которому язык LS и можно отнести к классу NP) – Ls(t, S, a, s, y). В неисключительных случаях (об исключительных будет в п. 6.1) аргументы «не подтвердят» слово языка и результат будет 0 (Ноль), если не будет исполнено хоть одно из следующих условий:
S – число, записанное в позиционном виде (например, в десятичном – вроде 3001) :
s = ss(S), где алгоритм ss(S) возвращает строку длиной S, состоящую только из символов «1»;
a – текст (программный код) некоторого алгоритма типа «Sol(…, …, …)» или же текст «-»;
t – текст некоторого утверждения на языке теории Пеано;
y – текст некоторого доказательства на языке теории Пеано;
|y| – размер текста y ограничен: |y| ≤ q_S(S) - |a|, где q_S(S) = 1000 * S^n, n – некоторая фиксированная степень, и, разумеется, условие на размер нарушено, если q_S(S) ≤ |a|;
Утверждение с текстом в t доказывается доказательством с текстом в y в рамках теории Пеано (или любой другой заранее оговорённой теории арифметики, если она более полная и удобная для наших целей, чем теория Пеано);
Если случай не из пункта 6.1 и перечисленные условия выполнены, то:
Ls(t, S, a, s, y) = 1.
Ещё мы условились, что записи вида «AntiSol_S» или «Sol(…, …, …)» обозначают текст утверждения AntiSol_S на заранее оговоренном языке логики и программный код (тоже текст, фактически) алгоритма Sol(…, …, …), записанный оговорённым способом представления алгоритмов в выбранной за основу языка LS теории первого порядка (теория Пеано способна представлять алгоритмы, но не очень наглядно – тут есть что улучшать для практических нужд).
И, разумеется, мы пользуемся не «гёделевыми номерами», которые дают неполиномиально огромное представление для информации (число 10, например, имеет вид «1111111111»), а принятым в «человеческом» и «компьютерном» мире представлением в виде текстов и чисел в позиционном (десятичном, например) представлении.
Теперь – о времени работы алгоритма проверки для разных случаев, словах языка LS, сертификатах, их размере и исключениях:
6.1. Для случаев, подходящих под шаблон
Ls(«AntiSol_S», S, «Sol(…, …, …)»,…, …) количество шагов работы – в пределах полинома p₀(|t|, |S|, |a|). В силу того, что в данном случае t = «AntiSol_S», чей размер полиномиально зависит от размера |a| = |«Sol(…, …, …)»| и от размера |S|, а при этом |«Sol(…, …, …)»| < |«AntiSol_S»|, то в p₀(|t|, |S|, |a|) можно заменить |a| на |t| и ограничивающий алгоритм останется ограничивающим (количество шагов работы алгоритма проверки не превысит результат данного ограничивающего алгоритма) и при этом он останется полиномиальным. И его тогда можно переписать в виде:
p₀(|«AntiSol_S»|, |S|) (что равно p₀(|t|, |S|)).
Проверку под шаблон 6.1 алгоритм Ls(t, S, a, s, y) проводит в первую очередь и – если соответствие обнаружено – возвращает 0 в пределах указанного времени (количества шагов).
Кстати, многоточия в конце Ls(«AntiSol_S», S, «Sol(…, …, …)»,…, …) стоят потому, что аргументы s, y в данном случае не используются и тут алгоритм зависит, фактически, от трёх аргументов, возвращая 0: Ls(«AntiSol_S», S, «Sol(…, …, …)»,…, …) = 0.
И, напомню, случай 6.1 относится к тому слову (словам!), принадлежность которого отвергается и смысл этого отказа такой: «Алгоритм Sol(«AntiSol_S», S, …) не может найти доказательство для утверждения AntiSol_S». Можно было бы добавить «…в пределах доказательств допустимого размера», но найти доказательство для утверждения AntiSol_S алгоритм Sol(«AntiSol_S», S, …) не может в принципе. Поэтому не может «вообще» и, в силу этого, «…в пределах доказательств допустимого размера» в том числе.
Раз нет доказательств, значит, нет и соответствующей длины доказательства. А то, что результат (0 – Ноль) алгоритм проверки выдаёт очень быстро, независимо от аргумента s (и от размера |s|) – соответствует оптимизации получения самого короткого и быстрого результата из возможных правильных результатов. Так, полиномиальность поиска доказательства рассчитывается от самого короткого из доказательств. И, кстати, тоже может не зависеть от аргумента s – если бы мы включили в алгоритм Ls(t, S, a, s, y) проверку утверждений на соответствие схеме аксиом из логики предикатов, например.
Вариант из 6.1 – это как 1-я прикладная роль языка из класса P – алгоритм типа Lp(w): у этого алгоритма есть «ограничивающий алгоритм» на количество шагов до получение результата (скорость работы) – p(|w|) – полиномиальный от размера |w|. Если рядом «положить» значение некоторого сертификата s, от которого ничего не зависит, то ведь всё равно этот сертификат можно дописать в качестве аргумента: Lp(w, s), хоть он и не используется. Но надо ли после этого считать, что ограничивающий алгоритм стал теперь таким: p(|w|, |s|)? Разумеется, нет.
И «нет» потому, что важна логика работы алгоритма, а не форма записи.
Вообще-то спец. случай пункта 6.1 касается принадлежности языку LS слов вида:
t, S, a, s. Соответствующие им сертификаты имеют вид:
y.
Отвергнутые «по шаблону» пункта 6.1 слова имеют вид:
«AntiSol_S», S, «Sol(…, …, …)»,s.
Разумеется часть слова a (которая в данном случае равна «Sol(…, …, …)») не присутствует среди аргументов алгоритма-решения Sol(«AntiSol_S», S, s), так как эта информация для алгоритма-решения присутствует в качестве его собственного программного кода. И – в отличие от аргументов – это неизменная и неустранимая данность для данного алгоритма-решения – независимо от того, «понимает» он её или «не понимает».
Но кроме специального случая – при котором соответствующие слова языку LS как раз не принадлежат – в остальном принадлежность слов данного вида ничем не отличается от принадлежности слов из пункта 6.2. Просто часть a в пункте 6.2 уже не является частью слова (а становится частью сертификата). Такая «одинаковость» (кроме спец. случая) связана с тем, что в языке LS мы учитываем только ту ограниченность возможностей алгоритмов-решений, которая следует из теоремы о неопределимости. Но эта ограниченность полностью исчерпывается специфическими случаями (хоть их и бесконечное количество для каждого алгоритма-решения) из пункта 6.1.
6.2. Для остальных случаев количество шагов работы алгоритма проверки – в пределах p₁(|t|, |S|, |s|), впрочем, и пункт 6.1 соответствует пункту 6. Но случай 6.1 является более жёстким ограничением – неполиномиально более жёстким, так как в случае 6.2 членом полинома является размер |s|, растущий экспоненциально относительно размера |S|.
Случай 6.2. относится к словам вида:
t, S, s.
Эти слова не учитывают алгоритм-решение, который ищет доказательство утверждения t и не содержат эту часть (a) в составе слова.
Но эти слова из случая 6.2 зачастую принадлежат языку LS, то есть, имеют соответствующий подтверждающий сертификат вида:
a, y.
И этот сертификат включает в себя часть a.
При этом его суммарный размер ограничен (требование корректности) алгоритмом
1000 * |s|^n, где n – некоторая фиксированная степень:
|a| + |y| ≤ 1000 * |s|^n, что повторяет сказанное в начале пункта 6 про размер доказательства |y|:
|y| ≤ q_S(|s|) - |a|
Для 1-й прикладной роли языка из класса NP алгоритм проверки должен работать полиномиальное время относительно размера слова. Но при этом алгоритм проверки зависит и от сертификата. А из-за этого и сертификат – в своей значимой части – должен по своему размеру быть в подобных же полиномиальных пределах относительно размера слова.
Именно поэтому у ограничивающих полиномиальных алгоритмов на время работы проверки и на размер сертификата зачастую стоят одни и те же размерные аргументы. Хотя у ограничивающего алгоритма на размер может быть и нечто меньшее (сколь угодно) – условия на полиномиальность всё равно будут исполнены, пункт 6.1 тому пример.
6.3. Если алгоритм-решение Sol(«AntiSol_S», S, s) для слова из специального случая 6.1 возвращает 1 при корректном s = ss(S):
Sol(«AntiSol_S», S, s) = 1 (случай 1),
то доказательства для утверждения AntiSol_S нет, и, напротив, имеется доказательство для его отрицания. То есть, ответ данного алгоритма-решения на данном слове в этом случае заведомо не корректен.
Если же алгоритм-решение Sol(«AntiSol_S», S, s) для слова из специального случая 6.1 возвращает 0 при корректном s = ss(S):
Sol(«AntiSol_S», S, s) = 0 (случай 2),
то логическое доказательства для утверждения AntiSol_S имеется, но, вопрос – соответствует ли размер данного доказательства допустимым размерам:
|y| ≤ q_S(|s|) - |a|.
Но если размер данного доказательства соответствует указанному пределу, то ответ данного алгоритма-решения на данном слове и в этом случае оказывается не корректным.
Если же алгоритм-решение Sol(«AntiSol_S», S, s) для слова из специального случая 6.1 не возвращает никакого ответа при корректном s = ss(S) (случай 3), то данное слово действительно не принадлежит языку LS и это подтверждается при любых сертификатах алгоритмом проверки. То есть, и в данном случае работа алгоритма-решения Sol(«AntiSol_S», S, s) оказывается не корректной.
Значит, единственный случай, при котором алгоритм-решение Sol(«AntiSol_S», S, s) может выдать корректный результат – случай 2. И результат этот должен быть 0. И этот результат соответствует результату работы алгоритма проверки Ls(«AntiSol_S», S, «Sol(…, …, …)»,…, …) = 0 за полиномиальное количество шагов работы – в пределах p₀(|«AntiSol_S»|, |S|) (что равно p₀(|t|, |S|)).
Поэтому при сведении нашей задачи из класса NP в класс P полиномиальность времени проверки для случая 2 p₀(|t|, |S|) должна превратиться в полиномиальность времени на обнаружение решения (или невозможности решения) вида p₀₊(|t|, |S|).
И вот идея доказательства для NP ≠ P:
Здесь очевидно, что при достаточно больших S данное предельное время работы алгоритма-решения из случая 2 экспоненциально мало по сравнению с допустимым размером доказательств: |y| ≤ q_S(|s|) - |a|, так как размер |s| = |ss(S)| экспоненциально велик по сравнению и с размером |a|, и с аргументами в p₀₊(|t|, |S|) при достаточно больших S.
А это значит, что для достаточно больших S среди допустимых доказательств найдётся и то, в котором будет вывод и для случая 2: Sol(«AntiSol_S», S, ss(S)) = 0, и для вытекающего из него утверждения AntiSol_S. А это и будет означать, что алгоритм Sol(«AntiSol_S», S, ss(S)) не смог подтвердить истинность утверждения AntiSol_S для которого есть доказательство среди доказательств допустимого размера.
А поскольку алгоритм Sol(…, …, …) произвольный, то это будет означать отсутствие корректных алгоритмов-решений, делающих язык LS языком класса P. То есть – оказывается доказанным неравенство NP ≠ P.
Конечно, в нескольких абзацах выше изложено доказательство NP ≠ P в общих чертах, а детали – как строить вывод для утверждения AntiSol_S при корректном времени работы алгоритма-решения Sol(«AntiSol_S», S, ss(S)) = 0 и почему размер вывода будет допустимого размера – изложены в следующем разделе.
