6. NP ≠ P на примере языка LS.
При сведении нашей задачи из класса NP в класс P полиномиальность времени проверки
p₀(|t|, |S|) и p₁(|t|, |S|, |s|) из пп. 6.1 и 6.2 соответственно
должны превратиться в полиномиальность времени на обнаружение решения (или невозможности решения) вида:
p₀₊(|t|, |S|) и p₁₊(|t|, |S|, |s|) соответственно
Но нас будет интересовать специфический случай, с его p₀₊(|t|, |S|), так как проблема на пути поиска решения за данное время тут особенно очевидна:
Есть все основания полагать, что данное небольшое время работы приведёт к противоречию с тем, что после ответа алгоритма-решения при достаточно большом S возникнет доказательство для отвергнутого алгоритмом-решением утверждения (в соответствии со случаем 2 пункта 6.3 прошлого раздела) и доказательство это будет достаточно коротким по меркам пункта 6.2, чтобы вписаться в размеры, диктуемые размером |s|.
При этом единственный случай, когда алгоритм Sol(«AntiSol_S», S, s) может выдать корректный ответ такой:
Sol(«AntiSol_S», S, s) = 0 (случай 2 из пункта 6.3 предыдущего раздела).
Если при этом для утверждения AntiSol_S найдётся доказательство y в пределах из пункта 6.2 прошлого раздела:
|y| ≤ q_S(|s|) - |a|,
то алгоритм-решение Sol(«AntiSol_S», S, s) окажется некорректным – сообщил об отсутствии доказательства утверждения AntiSol_S в допустимых пределах, а доказательство есть и размер его – допустимого размера.
С точки зрения языка LA, где нет ограничений на размер доказательства, любой алгоритм-решение заведомо некорректен, так как случай 6.1 из предыдущего раздела (если пункт 6 переписать для LA) сообщает о невозможности для алгоритма-решения Sol(«AntiSol») (произвольного) найти доказательство для AntiSol, но ответ алгоритма-решения «не нашёл доказательство» создаёт это доказательство в соответствии с пунктом 6.3, случай 2 предыдущего раздела.
Отличие языка LS от языка LA в том, что при Sol(«AntiSol_S», S, …) = 0 альтернатива данному ответу – доказательство утверждения AntiSol_S – может и не уложиться в допустимые пределы q_S(S).
То есть, для того, чтобы свести нашу 1-ю прикладную роль языка LS класса NP к 1-й прикладной роли класса P нам нужно найти соответствующий корректный алгоритм-решение Sol(t, S, s), который в случае пункта 6.1 из прошлого раздела успевает выдать результат 0 за время (количество шагов) в пределах:
N₀₊ ≤ p₀₊(|«AntiSol_S»|, |S|) (или короче – N₀₊ ≤ p₀₊(|t|, |S|)).
И при этом алгоритм-решение Sol(t, S, …) не использует (не обращается) к аргументу s-прописная в большей степени, чем это небольшое количество шагов.
Но помимо этого, в случае 6.1 частью слова является a, которого мы не видим среди аргументов Sol(t, S, s). Его нет среди аргументов потому, что данная информация имеется у алгоритма Sol(…, …, …) в качестве его собственного программного кода. И эту информацию алгоритм может получить при помощи диагонализации, как известно (не термин, а факт) со времён Гёделя.
Способность Sol(…, …, …) в решении вопроса:
Sol(«AntiSol_S», S, s), где s ≠ ss(S)
мы не рассматриваем – в этих случаях слово явно не принадлежит языку LS и алгоритму Sol(…, …, …) не мешает ничего (кроме, может быть, его собственного устройства) дать правильный ответ – 0 (Ноль). Нас интересует только вариант:
Sol(«AntiSol_S», S, s), где s = ss(S)
Итак, чтобы доказать некорректность алгоритма-решения Sol(«AntiSol_S», S, …) будем исходить из того, что он возвращает 0: Sol(«AntiSol_S», S, s) = 0 за количество шагов N₀₊ ≤ p₀₊(|«AntiSol_S»|, |S|) (или короче – N₀₊ ≤ p₀₊(|t|, |S|)). При этом s = ss(S). И нам нужно доказать, что для достаточно большого S-заглавного можно при этом доказать утверждение AntiSol_S доказательством с размером Q₀ = |y| таким, что:
Q₀₊ ≤ q_S(|s|) - |a|.
Вот и будем соответствующее доказательство строить в несколько этапов…
1.1. Для разбираемого случая
Sol(«AntiSol_S», S, s) = 0
у нас есть истинное (доказуемое за фиксированное число шагов) утверждение для произвольного S:
( Sol(«AntiSol_S», S, ss(S)) = 0 ) ⇒ AntiSol_S.
Подобные импликации крайне просто доказываются для алгоритмов - благодаря аксиоме равенства J2.
У нас есть простое верное равенство для произвольного S:
ContrSol(S) = If( Sol(«AntiSol_S», S, ss(S)) = 0, 1, 0)
Это равенство описывает, как работает алгоритм ContrSol(S), лежащий в основе AntiSol_S и «поступающий наоборот». Алгоритм
If(Условие, Результат при истине, Результат в ином случае)
широко известен в программировании. Если обозначить приведенное равенство как A(i), где
i обозначает Sol(«AntiSol_S», S, ss(S)), и пусть
j обозначает 0 (Ноль), тогда
Воспользуемся аксиомой J2:
( i = j ) ⇒ ( A(i) ⇒ A(j) )
Переписав его с учётом истинности A(i) в виде:
( i = j ) ⇒ A(j), и получим подстановкой:
( Sol(«AntiSol_S», S, ss(S)) = 0 ) ⇒ ( ContrSol(S) = If( 0 = 0, 1, 0) )
А с учётом свойств алгоритма If(…, …, …) получим:
( Sol(«AntiSol_S», S, ss(S)) = 0 ) ⇒ ( ContrSol(S) = 1 )
В силу того, что равенство ContrSol(S) = 1 и есть утверждение AntiSol_S – приходим к тому, что и требовалось доказать:
( Sol(«AntiSol_S», S, ss(S)) = 0 ) ⇒ AntiSol_S.
Какого размера будет этот этап доказательства с учётом необходимой подстановки конкретного значения S? С учётом того, что строки доказательства пункта 1.1 – производные от «Sol(…, …, …,)» и числа S и количество строк фиксировано – будет полином от размеров тех же |«Sol(…, …, …,)»| и размера |S|. Но для единообразия вместо |«Sol(…, …, …,)»| используем |t| = | «AntiSol_S»|, что приведёт к завышению полинома, но тем более он будет давать большую величину, чем наибольший размер нашего доказательства для пункта 1.1. И получим полином q_1 такого вида:
q_1(|t|, |S|)
Заметим, что обсуждаемая импликация истинна и её можно вообще сделать схемой аксиом для произвольного алгоритма-решения Sol(…, …, …) и такое расширение теории Пеано будет вполне корректным вариантом теории первого порядка для арифметики. И уж в этом случае оценка размера доказательства конкретной реализации данной схемы аксиом очевидно соответствует последнему ограничивающему алгоритму.
1.2. Осталось решить, какой длины можно построить доказательство для
Sol(«AntiSol_S», S, s) = 0 при s = ss(S)
Если бы алгоритм был без аргументов, то для такого варианта:
SolSpec_S() = 0 и количестве шагов его работы N_Spec
длина доказательства была бы в пределах полинома:
q_2(|«SolSpec_S()»|,N_Spec)
что довольно очевидно, так как каждый шаг работы алгоритма потребует полиномиального количества шагов логического вывода, которые представляют этот шаг и размер которых зависит от размера алгоритма. Степени этого полинома нас тут не интересуют, но важно, что зависимость полиномиальная.
Как свести алгоритм с аргументами к алгоритму без аргументов? Самый простой путь: составной алгоритм, в котором в первой части нужные значения аргументов присваиваются переменным, а затем во второй части вызывается исходный алгоритм с данными переменными в качестве аргументов. Тогда условный программный текст (где знак равенства – это присваивание, многоточие – нужные числа, а результат работы программы – это результат алгоритма в последней строке программного кода) для SolSpec_S() на базе Sol(«AntiSol_S», S, s) был бы таким:
t = «AntiSol_S»;
S = …;
s = ss(S);
Sol(t, S, s);
Но в этой программе нас не устраивает строка s = ss(S). Она может работать неполиномиально долго по сравнению со всей остальной программой. Поэтому в отношении операций с аргументом s-прописная нам надо переделать алгоритм Sol(t, S, s) на такой, в котором каждое обращение к любому i-му символу аргумента s-прописная заменялось бы на обращение к функции:
Func_S(i)
и эта функция эмулировала бы аргумент-строку s-прописная, возвращая:
Символ «1», если 1 ≤ i ≤ S
или информацию о выходе запроса за пределы данных, если i < 1 или i > S.
Очевидно, что такую модернизацию алгоритма Sol(t, S, s) в некий алгоритм
SolX(t, S)
можно осуществить и довольно легко. В название алгоритма добавлен символ «Икс», что часто делают для «улучшенных» версий алгоритмов или данных – вроде файлов типа «.docx» вместо прежних «.doc», например – этот «Икс» - кусочек от слова «Extention».
И вот с учётом такой модернизации наша программа для SolSpec_S() примет вид:
t = «AntiSol_S»;
S = …;
SolX(a, S);
И очевидно, что верно:
SolSpec_S() = Sol(«AntiSol_S», S, s) при s = ss(S)
То есть, для последнего равенства есть доказательство или его можно и вовсе аксиоматизировать, в некую схему аксиом.
Размер доказательства для последнего равенства – аналогично прошлому пункту 1.1 можно оценить (не больше чем) так:
q_2(|t|, |S|)
1.3. Последнее равенство позволяет нам свести вопрос о работе алгоритма:
Sol(«AntiSol_S», S, s) = 0 при s = ss(S)
К работе алгоритма
SolSpec_S() = 0
Но это уже позволяет оценить размер доказательства, который доказывает последнее равенство:
q_3(|«SolSpec_S()»|,N_Spec) , где N_Spec – количестве шагов работы SolSpec_S().
Если посмотреть на программу, то там всё - производное от программного кода алгоритма Sol(…, …, …) и числа S. При этом размеры этих производных данных полиномиально зависят от размеров |Sol(…, …, …)| и |S| (аргумент s-прописная, который зависит неполиномиально, мы в последней версии исключили), поэтому последний ограничивающий алгоритм можно переписать так:
q_4(|«Sol(…, …, …)»|, |S|, N_Spec) , где N_Spec – количестве шагов работы SolSpec_S().
Еще и количество шагов работы программы SolSpec_S() тоже полиномиально зависит от количества N₀₊ шагов работы нашего исходного алгоритма-решения, от размеров исходного алгоритма |Sol(…, …, …)|, размеров |S|, размеров |« Func_S(…)»| – с учётом дополнительных строк в SolSpec_S() в сравнении с исходным Sol(«AntiSol_S», S, s = ss(S)) и заменой части кода и части шагов выполнения в самой Sol(«AntiSol_S», S, s = ss(S)) на операции с функцией Func_S(i) (модернизация до SolX(a, S)).
То есть, найдётся некоторый полином, для которого верно:
N_Spec ≤ p_1(|«Sol(…, …, …)»|, |«Func_S(…)»|, |S|, N₀₊)
С учётом того, что |«Func_S(…)»| меняется (полиномиально по размерам) только от |S|, то его можно оставить как часть зависимости полинома от |S|, но исключив, как отдельный аргумент. Тогда последнюю оценку можно переписать так:
N_Spec ≤ p_2(|«Sol(…, …, …)»|, |S|, N₀₊)
Тогда:
q_4(|«Sol(…, …, …)»|, |S|, N_Spec) ≤ q_4(|«Sol(…, …, …)»|, |S|, p_2(|«Sol(…, …, …)»|, |S|, N₀₊) )
Композиция полиномов даёт полином с теми же аргументами, что у всех полиномов композиции. Поэтому имеем:
q_4(|«Sol(…, …, …)»|, |S|, N_Spec) ≤ q_5(|«Sol(…, …, …)»|, |S|, N₀₊)
Поскольку |AntiSol_S| ≥ |«Sol(…, …, …)»|, а |AntiSol_S| обозначаем тут как |t|,
то можно заменить в последнем неравенстве правую часть так:
q_4(|«Sol(…, …, …)»|, |S|, N_Spec) ≤ q_5(|t|, |S|, N₀₊)
Значит, размер для доказательство
SolSpec_S() = 0
будет в пределах
q_5(|t|, |S|, N₀₊)
Но мы знаем, что
N₀₊ ≤ p₀₊(|t|, |S|)
И это даёт такое ограничение при подстановке:
q_5(|t|, |S|, p₀₊(|t|, |S|))
И опять, раскрывая композицию полиномов, получаем верхний предел для размера доказательства для равенства
SolSpec_S() = 0
такой:
q_6(|t|, |S|)
1.4. Теперь у нас есть полная информация о построении доказательства утверждения AntiSol_S для случая 2 пункта 6.3 предыдущего раздела и можно выяснить, в каких пределах находится размер данного доказательства:
1. Доказываем SolSpec_S() = 0 из пункта 1.3 с размером этой части доказательства не более чем q_6(|t|, |S|) символов;
2. Доказываем SolSpec_S() = Sol(«AntiSol_S», S, s) при s = ss(S) из пункта 1.2 с размером этой части доказательства не более чем q_2(|t|, |S|) символов;
3. Из пунктов 1 и 2 выводим по аксиомам равенства Sol(«AntiSol_S», S, s) = 0, о размере скажем после пунктов о доказательстве;
4. Доказываем ( Sol(«AntiSol_S», S, ss(S)) = 0 ) ⇒ AntiSol_S из пункта 1.1 с размером этой части доказательства не более чем q_1(|t|, |S|) символов;
5. Из пунктов 3 и 4 выводим по правилу MP искомое утверждение AntiSol_S, о размере скажем после пунктов о доказательстве;
Таким образом, доказательство утверждения AntiSol_S построено. Если считать размер доказательства в этапах (очень простых) 3 и 5 вместе не превышающим следующий полином:
q_7(|t|, |S|)
То суммарный размер Q₀₊ для доказательства утверждения AntiSol_S не превысит некого полинома q₀₊(|t|, |S|) = q_1(|t|, |S|) + q_2(|t|, |S|) + q_6(|t|, |S|) + q_7(|t|, |S|):
Q₀₊ ≤ q₀₊(|t|, |S|)
Сравниваем этот ограничивающий алгоритм с ограничивающим алгоритмом на размер доказательства из пункта 6.2 предыдущего раздела:
|y| ≤ q_S(|s|) - |a|
Очевидно, что для достаточно больших S верно:
q₀₊(|t|, |S|) + |a| ≤ q_S(|s|)
так как размер |s| экспоненциально велик относительно размеров |t|, |S|, |a| при достаточно больших S. А степень полинома q_S(|s|) не имеет значения, когда под знаком степени – экспоненциально растущая величина |ss(S)|: такой полином превысит любой другой полином q₀₊(|t|, |S|) + |a|, если у другого полинома под степенью любое значение экспоненциально отстаёт в своём росте от значения |ss(S)|.
Таким образом, мы доказали, что для достаточно больших S и случай 2 пункта 6.3 предыдущего раздела оказывается невозможным для корректного решения алгоритмом-решением (произвольным) Sol(…, …, …). А это означает, что свести язык LS из класса сложности NP к классу сложности P невозможно. То есть, доказано:
NP ≠ P.
