NP≠P. Док-во от противного-контрпример алгоритмов из NP

[dmitgu]

mihaild в сообщении #1264934 писал(а):

dmitgu, давайте договоримся, что вы всё-таки не будете писать тексты длиннее трех абзацев. Пока что я не помню ни одного случая, чтобы вы написали столько и не возникло вопросов - а текст, идущий после места, к которому есть вопрос, всё равно бесполезен.

Мне не пришло уведомление о продолжении Вашей записи или я его прозевал. И я думал про 3 абзаца Как упростить. Ответ подготовил именно про это. Но сначала отвечу на то, что прозевал:

mihaild в сообщении #1264934 писал(а):

язык $LS$ строится как $(A \cup B) \setminus C$, где
$A$ состоит из слов вида $\overline{t, s}$, где $s$ - строка из единиц, $t$ - теорема арифметики, для которой существует доказательство не длиннее $|s|^n$ ($n$ - некоторая мировая константа)
$B$ состоит из слов вида $\overline{t, a, s}$, где $\overline{t, s} \in A$, $a$ - некоторый алгоритм. От $a$ что-то здесь зависит, или любой алгоритм сойдет?
$C$ состоит из слов вида $\overline{AntiSol, Sol(\ldots, \ldots)}$ (что это такое - я пока не понимаю, если с $A$ и $B$ согласны - напишите, пожалуйста, минимальное количество информации про них, необходимое для определения - например, хотя бы что это такое - алгоритмы? утверждения? что-то еще?)

В общем верно, хотя кроме $s$-прописная есть ещё и $S$-заглавная – там сразу число и оно короткое (в десятичном виде, например). Но, возможно, для $A$ и $B$ она не особо нужна. А вот для $C$ - принципиально необходима.

От $a$ ничего не зависит для $A$ и $B$, и любой алгоритм сойдет, но вот для $C$ - зависит принципиально:

Выражение $AntiSol_S$ строится так, чтобы его принадлежность к числу теорем теории Пеано алгоритм $\operatorname{Sol}(..., ..., ...)$ заведомо не смог подтвердить не то что за допустимое количество шагов, полиномиальное от предельного допустимого размера доказательства $q(S)$, а вообще ни за какое.

При этом данное утверждение всё-таки будет принадлежать языку $LS$ если алгоритм $\operatorname{Sol}(..., ..., ...)$ выдаст результат $0$ («не подтверждаю принадлежность данных слов языку $LS$») достаточно быстро. То есть, утверждение $AntiSol_S$ должно «поступить наоборот» относительно результата

$\operatorname{Sol}(\overline{AntiSol_S}, S, s)$ при корректных $S$, $s$.

Подобные утверждения хорошо известны в логике из доказательств о неразрешимостях. И из доказательства теоремы о неопределимости - в частности. Нам надо воспользоваться «возражающим алгоритмом» $\operatorname{ContrSol}(S)$ со следующим свойством:

$\operatorname{ContrSol}(S) = \operatorname{If}( \operatorname{Sol}(\overline{AntiSol_S}, S, ss(S)) == 0, 1, 0 )$

Это равенство описывает, как работает алгоритм $\operatorname{ContrSol}(S)$, лежащий в основе $AntiSol_S$ и «поступающий наоборот». Алгоритм

If(Проверка логического выражения на истинность, Результат при истине, Результат в ином случае)

широко известен в программировании. Обозначение $X == Y$ выше - это проверка, равны ли результаты от $X$ и $Y$ между собой. И данное сравнение возвращает «истина», если равны, а если не равны, то возвращает «ложь».

В силу того, что равенство $\operatorname{ContrSol}(S) = 1$ и есть утверждение $AntiSol_S$ - приходим к тому, что нам и требовалось, а именно, слово:

$\overline{\operatorname{Sol}(..., ..., ...)}, \overline{AntiSol_S}, S$

Не принадлежит языку $LS$. И это отражает тот факт, что именно $\operatorname{Sol}(\overline{AntiSol_S}, S, s)$ не способен подтвердить принадлежность слова $\overline{AntiSol_S}, S, s$ языку $LS$ - этот факт «быстрый» и не требует рассмотрения никаких доказательств.

Теперь я отвечу про «три абзаца» и формализую принципиальный момент, который, возможно, витает в воздухе и создаёт непонимание что это за язык $LS$.

Гм… Дело не в количестве абзацев, наверно - часто большая книга читается проще маленькой о том же, потому что в большой изложено более последовательно и понятно. Тем более в математике ужать некоторые мысли в несколько абзацев невозможно.

В моём последнем большом тексте тут я написал громоздкие формулы с большим количеством новых обозначений без аккуратной подготовки. Такие формулы «с потолка» понятны, когда ты сам их придумываешь, но не когда читаешь чужой текст.

Меня «унесло» в собственные мысли, когда по ходу формализации (которая была затеяна благодаря обсуждению тут и Вам в частности) я решил, что можно доказать не только первопричину вопроса о $NP \ne P$, но и само это неравенство. Не то, чтобы это сильно принципиальная возможность, но это может помочь донести и сильно принципиальное . Поэтому много чего пересмотрел, не очень чётко связал новое со старым и не слишком внятно изложил.

К тому же, есть принципиальное отличие языка $LS$ от языков класса $NP$ из учебников. Это отличие у меня не получалось сформулировать, а тем более трудно спросить про него «со стороны», раз предмет вопроса не формализован. Поэтому это принципиальное отличие я сейчас сформулирую. Я и остальное переписал до конца, но не буду добавлять ещё три страницы, так как в ходе обсуждения порядок и терминология могут измениться.

Итак:

Ставится вопрос о решении (сведении) языка $LS$ класса $NP$ к классу $P$. И при этом должен произойти переход от алгоритма проверки $\operatorname{Ls}(w, y)$ к алгоритму-решению $\operatorname{Sol}(w)$. В учебниках по теории алгоритмов рассматриваются только такие языки класса $NP$, что для алгоритма-решения $\operatorname{Sol}(w)$ предполагается переданным для рассмотрения о принадлежности языку только одно слово - слово $w$. Но мы рассмотрим язык $LS$, который содержит и слова вида:

$\overline{\operatorname{Sol}(...)}, w’$, где $w’$ либо совпадает с $w$, либо содержит только часть информации из $w$.

И в этом случае алгоритму решению $\operatorname{Sol}(w)$ переданы для рассмотрения 2 слова вида

1. $w$

2. $\overline{\operatorname{Sol}(...)}, w’$

При этом мы исходим из того, что алгоритм-решение $\operatorname{Sol}(...)$ располагает информацией о своём собственном программном коде $\overline{\operatorname{Sol}(...)}$ в той же мере, что и о значении переданного ему аргумента $w$ (аксиома рефлексии).

Но поскольку алгоритм-решение может вернуть только один результат, то язык $LS$ должен быть построен так, чтобы для обоих слов правильный результат произвольного алгоритма-решения $\operatorname{Sol}(...)$ всегда был одним и тем же.

Назовём это свойство «свойством согласованности языка $LS$».

Вот такое у языка $LS$ принципиальное отличие от языков класса $NP$ из учебников. Обсуждать дальше имеет смысл, если язык $LS$ можно признать языком класса $NP$, не смотря на сформулированное только что его отличие от «привычных» языков класса $NP$.

[venco]

(прописная)

dmitgu в сообщении #1272430 писал(а):

В общем верно, хотя кроме $s$-прописная есть ещё и $S$-заглавная – там сразу число и оно короткое (в десятичном виде, например).

Между прочим, "прописная" и "заглавная" - это одно и тоже. Вы, скорее всего, имели в виду "строчная".

[mihaild]

dmitgu в сообщении #1272430 писал(а):

Тем более в математике ужать некоторые мысли в несколько абзацев невозможно.

Но всегда возможно разбить неужимаемую мысль на несколько.

$\operatorname{Sol}$ - это какой-то конкретный алгоритм, или он выступает параметром?
Если конкретный - то какой? Если параметр - то есть ли какие-то ограничения?

[dmitgu]

mihaild в сообщении #1272475 писал(а):

$\operatorname{Sol}$ - это какой-то конкретный алгоритм, или он выступает параметром?
Если конкретный - то какой? Если параметр - то есть ли какие-то ограничения?

Это в принципе любой произвольный алгоритм. Включая и все возможные алгоритмы-решения. Просто для любого алгоритма можно построить соответствующее ему утверждение $AntiSol_S$, которое этот алгоритм не сможет подтвердить как принадлежащий языку $LS$ при данном S - это широко используется в логике, но без S, потому что в логике нет ограничений на длину доказательства.

Если угодно, то теорема о неопределимости в формальной логике, это доказательство вот чего:

$NF \ne F$

только речь идет не о классе с полиномиальным ограничением $P$, а о классе с ограничением (финитным), и не о $NP$, где полиномиальная проверка от размера слова, а о $NF$, где для любого конечного сертификата проверка финитная. У меня есть теперь интересное сопоставление, почему в формальной логике надо одно слово для доказательства неполноты, а у меня (для теории алгоритмов) - 2. И почему требуется в теории алгоритмов аксиома рефлексии для того, чтобы от теорем о неразрешимости и неполноте в логике перейти к их аналогам в теории алгоритмов. А то кажется, что теория алгоритмов от них ушла, якобы. Не ушла Но просто требуется понять, что имеет место ещё и теорема рефлексии - о программном коде, который тоже - информация.

[mihaild]

Верно ли, что $C$ - это язык, состоящий из слов вида $\overline{AntiSol_S, Sol, S, s}$, где $Sol$ - произвольный алгоритм от трех аргументов, $S$ - запись двоичного числа, $s$ - унарная запись того же числа, $AntiSol_S$ доказуемо эквивалентно $Sol(\Antisol_S, S, s) = 1$?
(тут надо посмотреть, насколько эффективна теорема о неподвижной точке, но это можно потом)

[dmitgu]

mihaild в сообщении #1272565 писал(а):

Верно ли, что $C$ - это язык, состоящий из слов вида $\overline{AntiSol_S, Sol, S, s}$, где $Sol$ - произвольный алгоритм от трех аргументов, $S$ - запись двоичного числа, $s$ - унарная запись того же числа, $AntiSol_S$ доказуемо эквивалентно $Sol(\Antisol_S, S, s) = 1$?

Не совсем. Речь о слове, которое не принадлежит $LS$ и оно без $s$-прописная (оно просто не используется в данном случае алгоритмом проверки).

А $AntiSol_S$ - это

$\operatorname{If}(\operatorname{Sol}(\overline{AntiSol_S}, S, ss(S)) == 0, 1, 0 ) = 1$
Для случая, когда
$\operatorname{Sol}(\overline{AntiSol_S}, S, ss(S))$ останавливается.

или в кратком виде:
$\operatorname{ContrSol}(S) = 1$

Тут фишка в том, что $AntiSol_S$ для $|s| < |ss(S)|$ будет ещё "недоказуемее" для $\operatorname{Sol}(\overline{AntiSol_S}, S, s)$, чем для $ss(S)$, так как набор возможных доказательств ещё меньше.

Но вот для $S_+ > S$ вполне возможен корректный ответ:

$\operatorname{Sol}(\overline{AntiSol_S}, S_+, ss(S_+)) = 1$

Это называется "задним умом" найти нужный ответ. То есть, если

$\operatorname{Sol}(\overline{AntiSol_S}, S, ss(S))$ быстро выдаст 0, то он этим создаст доказательство для $AntiSol_S$ и с другим аргументом вместо $S$ вполне может это доказательство и найти. Но сначала это доказательство он должен создать - то есть, нарушить требования к корректному алгоритму-решению для языка класса $P$.

Аналогия с жизнью тут очевидна - мы тоже часто можем позже констатировать свои прошлые действия и оценивать их "со стороны", в отличие от момента совершения.

[mihaild]

dmitgu в сообщении #1272602 писал(а):

А $AntiSol_S$ - это

$\operatorname{If}(\operatorname{Sol}(\overline{AntiSol_S}, S, ss(S)) == 0, 1, 0 ) = 1$

Непосредственно такая формула может и не существовать. Вспомните формулировку теоремы о неподвижной точке - там получается не синтаксическое равенство, а доказуемая эквивалентность.

dmitgu в сообщении #1272602 писал(а):

Для случая, когда
$\operatorname{Sol}(\overline{AntiSol_S}, S, ss(S))$ останавливается.

Непонятно. Мы определяем $AntiSol$ только для этого случая? Или для другого определяем его как-то еще?

Насколько я понимаю, вы по алгоритму $Sol$ и строке, содержащей запись числа (унарную или бинарную?), строите формулу $AntiSol$. Если вы ее строите с использованием теоремы о неподвижной точке - то напишите явно, к какой арифметической формуле с одной свободной переменной она применяется.
(запись утверждений вида "алгоритм останавливается (за такое-то время) с таким-то результатом" считаем известной)

[dmitgu]

mihaild в сообщении #1272769 писал(а):

dmitgu в сообщении #1272602

писал(а):
А $AntiSol_S$ - это

$\operatorname{If}(\operatorname{Sol}(\overline{AntiSol_S}, S, ss(S)) == 0, 1, 0 ) = 1$
Непосредственно такая формула может и не существовать. Вспомните формулировку теоремы о неподвижной точке - там получается не синтаксическое равенство, а доказуемая эквивалентность.

Это совершенно точно строится при помощи процедуры диагонализации из формальной логики. Я даже привожу пример работающей программы, которая печатает свой собственный текст. Не в последней заметке, в ЕДРИД, а в предыдущей. Могу и тут привести. Классическая возможность строить программу, внутри которой стоит её собственный текст - точнее, эквивалентый её собственному (если посмотреть на несколько шагов, какое значение примет переменная).

Если словами:

$\operatorname{ContrSol}(S)$ - можно записать и как
$\operatorname{Contr}( \overline{\operatorname{Sol}(..., ..., ...)}, S )$ - которая выписывает текст (на основе своего собственного) для $\overline{AntiSol_S}$ и эмулирует работу

$\operatorname{Sol}(\overline{AntiSol_S}, S, ss(S))$, поступая "наоборот" - в зависимости от результата.

При этом $S$- краткая запись числа (десятичная, например). А $ss(S)$ - строка $s$ максимальной допустимой длины. И она не генерируется, а эмулируется при работе названного алгоритма - есть только там, докуда "дошла каретка". Поэтому время на её создание не тратится.

Если уж углубляться в построение
$\operatorname{Contr}( \overline{\operatorname{Sol}(..., ..., ...)}, S )$
то там предусмотрен и случай для не-остановки. Параллельно с эмуляцией работы
$\operatorname{Sol}(\overline{AntiSol_S}, S, ss(S))$
происходит и "тупой перебор" доказательств на предмет того, что это доказательство для
$\overline{AntiSol_S}$
и если такое доказательство обнаружится, то немедленно выдаётся 0. То есть - опровержение. А в силу того, что теория непротиворечива - такого не случиться. А это гарантирует, что даже при не-остановке - $\overline{AntiSol_S}$ не будет иметь доказательства.

Вообще-то для теории Пеано даже без параллельной проверки такое невозможно (доказуемость $\overline{AntiSol_S}$ при не остановке указанной эмуляции), но это довольно трудно обосновать. Но в принципе есть такие омега-противоречивые (но без реальных противоречий) теории из-за которых Россер придумал 1-ю теорему Гёделя с своей форме. Ну а у меня этот нюанс устраняется "параллельной проверкой".

mihaild в сообщении #1272769 писал(а):

Если вы ее строите с использованием теоремы о неподвижной точке

Не, не... Я уже забыл нюансы (но могу вспомнить - у меня даже где-то записано), но теорема о неподвижной точке вообще не годится. Там неполиномиальная нумерация и что-то неконструктивное. Процедура диагонализации - быстро, конструктивно и миллион раз проверено )

[mihaild]

Давайте не путать формулы и алгоритмы (они хоть и связаны, но всё же разные объекты).
И чтобы ничего не упустить, давайте вводить всё по частям, и явно выписывать все аргументы.

Для начала мы строим алгоритм $ContrSol_0$, принимающий три аргумента - строку $x$, алгоритм $Sol$ и число $S$ в двоичной записи. Он запускает $Sol$ с аргументами $x, S, ss(S)$ и, если $Sol$ на этих аргументах выдает $0$, то выдает $1$, если $Sol$ выдает $1$, то выдает $0$. Так?
(тут какие-то ограничения на время работы есть, или как повезет?)
(потом мы сможем использовать $ContrSol_0$ в другой программе, которая вместо $x$ будет что-то подставлять; но лучше вынести квайн в отдельный шаг явно)

dmitgu в сообщении #1272818 писал(а):

Классическая возможность строить программу, внутри которой стоит её собственный текст - точнее, эквивалентый её собственному

Это теорема о рекурсии (аналог теоремы о неподвижной точке для программ). Диагонализация - про другое.

[dmitgu]

mihaild в сообщении #1272865 писал(а):

Для начала мы строим алгоритм $ContrSol_0$, принимающий три аргумента - строку $x$, алгоритм $Sol$ и число $S$ в двоичной записи. Он запускает $Sol$ с аргументами $x, S, ss(S)$ и, если $Sol$ на этих аргументах выдает $0$, то выдает $1$, если $Sol$ выдает $1$, то выдает $0$. Так?

Не совсем. Никакого $x$ нет. Из программного кода алгоритма $\overline{Sol}$, числа $S$ и своего собственного программного кода $ContrSol_0$ строит текст утверждения $\overline{AntiSol_S}$ и запускает эмуляцию работы $Sol$ с аргументами $\overline{AntiSol_S}, S, ss(S)$. Эмуляция - потому что значение $ss(S)$ эмулируется, а не генерируется перед запуском.

Я так понял, что Вы под $ContrSol_0$ понимаете то, что я обозначал выше как $Contr$.

mihaild в сообщении #1272865 писал(а):

(тут какие-то ограничения на время работы есть, или как повезет?)

Никаких. Всё зависит от эмуляции работы $Sol$.

mihaild в сообщении #1272865 писал(а):

но лучше вынести квайн

Не знал, что есть специальное слово для выдачи своего программного кода )

-- 07.12.2017, 18:28 --

mihaild в сообщении #1272865 писал(а):

Это теорема о рекурсии (аналог теоремы о неподвижной точке для программ). Диагонализация - про другое.

Смысл понятен - я так назвал процедуру из "Леммы о диагонализации" как она называется у Булоса и Джеффри в "Вычислимость и логика".

[mihaild]

dmitgu в сообщении #1272889 писал(а):

Смысл понятен - я так назвал процедуру из "Леммы о диагонализации" как она называется у Булоса и Джеффри в "Вычислимость и логика".

Ну да, я это и понимал под теоремой о неподвижной точке. Разная терминология, видимо (или я уже забыл, что как называлось).

dmitgu в сообщении #1272889 писал(а):

Я так понял, что Вы под $ContrSol_0$ понимаете то, что я обозначал выше как $Contr$.

Не совсем. $ContrSol_0$ - пока просто алгоритм (к которому мы потом, возможно, будем применять диагонализацию).
В формулировке леммы о диагонализации есть формула $B$. Вот ее и хочется выписать более-менее явно.

[dmitgu]

mihaild в сообщении #1272896 писал(а):

Не совсем. $ContrSol_0$ - пока просто алгоритм (к которому мы потом, возможно, будем применять диагонализацию).

А! Ок.

-- 07.12.2017, 19:02 --

mihaild в сообщении #1272896 писал(а):

dmitgu в сообщении #1272889

писал(а):
Смысл понятен - я так назвал процедуру из "Леммы о диагонализации" как она называется у Булоса и Джеффри в "Вычислимость и логика".
Ну да, я это и понимал под теоремой о неподвижной точке.

В теории алгоритмов есть ещё теорема о неподвижной точке - я думал, Вы про неё. Она отличается и там адская нумерация, если её пытаться применять практически - такие у меня смутные воспоминания. Можно их и прояснить, был бы в этом смысл )

[mihaild]

mihaild в сообщении #1272865 писал(а):

Для начала мы строим алгоритм $ContrSol_0$, принимающий три аргумента - строку $x$, алгоритм $Sol$ и число $S$ в двоичной записи. Он запускает $Sol$ с аргументами $x, S, ss(S)$ и, если $Sol$ на этих аргументах выдает $0$, то выдает $1$, если $Sol$ выдает $1$, то выдает $0$. Так?

Фиксируем?

Если да, то, видимо, дальше мы вводим параметризованную двумя параметрами арифметическую формулу $B_{Sol, S}(x)$, утверждающую, что $ContrSol_0(x, Sol, s)$ выдает единицу?

[dmitgu]

mihaild в сообщении #1272931 писал(а):

Фиксируем?

Если да, то, видимо, дальше мы вводим параметризованную двумя параметрами арифметическую формулу $B_{Sol, S}(x)$, утверждающую, что $ContrSol_0(x, Sol, s)$ выдает единицу?

Вроде нормально. Ок.

[mihaild]

Теперь мы применяем теорему лемму о диагонализации и находим формулу $AntiSol_{Sol, S}$, такую что $\vdash AntiSol_{Sol, S} \leftrightarrow B_{Sol, S}(\overline{AntiSol_{Sol, S}})$?
И строим язык $C$ как множество троек $AntiSol_{Sol, S}, Sol, S$?