dmitgu

Category:

2. Алгоритмы-решения. Теорема о неопределимости. Утверждение AntiSol.

  к Оглавлению

Но в то же время язык L содержит множество теорем о свойствах чисел и алгоритмов. Ведь теория Пеано в состоянии «представлять» алгоритмы и позволяет формулировать и доказывать теоремы о них. В частности, имеется теорема о неопределимости. Которая даёт ответ (негативный) на вопрос, может ли какой-либо алгоритм «представить» всё множество теорем теории Пеано. Или, иными словами, представить язык L. 

Речь идет о таком алгоритме Sol(t), который должен был бы возвращать 1 в том случае, если аргумент t является словом языка L и 0 – в противном случае. Слово будет принадлежать языку L в том и только том случае, если t – текст теоремы теории Пеано. Предполагается, что есть способ сопоставить результат (или его отсутствие) работы любого алгоритма Sol(t) для любого слова t с фактом (не)принадлежности данного слова языку L. В этом сопоставлении язык L играет роль «эталона» с которым сравниваются результаты (или отсутствие результата) произвольного алгоритма Sol(t). Эту роль языка L назовём 2-й (Второй) прикладной ролью языка L.

Разбираемые алгоритмы (Sol(t) в данном примере) из 2-й прикладной роли языка будем называть «алгоритмы-решения», что не означает, что они все или какой-то из них способен представить язык L – соответствовать этому «эталону». Но если какой-то алгоритм удовлетворяет требованиям 2-й роли – (всегда останавливается с результатом и результат всегда соответствует «эталону» ) назовём его «корректный алгоритм-решение». 

Перечислим свойства, которыми должен обладать корректный алгоритм-решение, но перечислим их в виде отрицания данных свойств. Потому что произвольный алгоритм-решение Sol(…) не обладает этими свойствами на утверждении AntiSol (которое строится в зависимости от выбранного алгоритма-решения). И приводимое ниже отрицание свойств корректности для алгоритма-решения Sol(…) будет, вместе с тем, свойствами утверждения AntiSol:

1. Не верно, что если AntiSol является теоремой теории Пеано (то есть, словом в языке L), то алгоритм Sol(«AntiSol») возвращает за конечное время подтверждение этого факта, то есть Sol(«AntiSol») = 1.

Сразу оговоримся, что записи вида «AntiSol» или «Sol(…)» обозначают текст утверждения AntiSol на заранее оговоренном языке логики и программный код (тоже текст, фактически) алгоритма Sol(…), записанный оговорённым способом представления алгоритмов в выбранной за основу языка LS теории первого порядка (теория Пеано способна представлять алгоритмы, но не очень наглядно – тут есть что улучшать для практических нужд).

2. Не верно, что если AntiSol НЕ является теоремой теории Пеано (то есть, не является словом в языке L), то алгоритм Sol(«AntiSol») возвращает за конечное время результат о непринадлежности слова AntiSol языку L: Sol(«AntiSol») = 0.  

Я напомню простую идею доказательства теоремы о неопределимости и то, что это за утверждение - AntiSol:

Строится алгоритм ContrSol(), который генерирует в текстовом виде утверждение со своим собственным программным кодом (с помощью процедуры диагонализации) «ContrSol() = 1» и запускает алгоритм Sol(«ContrSol() = 1»). Если запущенный алгоритм Sol(«ContrSol() = 1») вернёт любой результат, кроме 0, то алгоритм ContrSol() вернёт 0. А если запущенный алгоритм Sol(«ContrSol() = 1») вернёт 0, то алгоритм ContrSol() вернёт 1. А если запущенный алгоритм Sol(«ContrSol() = 1») не остановится, то алгоритм ContrSol() тоже не остановится.

Утверждение AntiSol – это вот что: ContrSol() = 1.

Разумеется, алгоритм Sol(«AntiSol») не может подтвердить утверждение AntiSol результатом 1– так как тогда будет верным ContrSol() = 0, что является отрицанием «подтверждённого» результата. Но алгоритм Sol(«AntiSol») не может и отвергнуть утверждение AntiSol результатом 0 – так как тогда будет верным ContrSol() = 1, что является доказательством AntiSol (не напрямую, но доказательство можно построить). 

Единственное, чего нам не хватает в свойствах утверждения AntiSol – того, чтобы в случае, если алгоритм Sol(«AntiSol») не останавливался, то утверждение AntiSol не было словом языка L (не доказывалось в нём). 

Для чего нам нужно это свойство утверждения AntiSol? Для того, чтобы всё указывало алгоритму Sol(«AntiSol») на отсутствие для него возможности найти подтверждение (доказательство) утверждения AntiSol. Понятно, что сам он не может найти доказательство утверждения AntiSol в непротиворечивой теории и вернуть информацию (результат 1) об этом– иначе сразу было бы противоречие. Но в некоторых даже непротиворечивых теориях для некоторых алгоритмов Sol(«AntiSol»), которые не останавливаются, может быть доказано соответствующее им утверждение AntiSol. И тогда отсутствие остановки (и результата) у алгоритма Sol(«AntiSol») не было бы однозначным расхождением с логикой теории – хоть доказательство сам алгоритм Sol(«AntiSol») найти и не смог, но и 0 он не вернул, потому что утверждение AntiSol всё же имеет доказательство! 

Однако такую возможную неоднозначность легко устранить небольшой модернизацией алгоритма ContrSol(): 

Помимо запуска алгоритма Sol(«AntiSol») алгоритм ContrSol() запускает параллельно ещё и перебор всех доказательств теории. И поступит наоборот, если будет в процессе перебора обнаружено доказательство AntiSol (то есть – вернёт 0). Тогда в непротиворечивой теории утверждение AntiSol не будет доказано, если Sol(«AntiSol») не остановится. 

Поэтому теперь формулируем третье свойство для утверждения AntiSol:

3. Верно, что если алгоритм Sol(«AntiSol») не останавливается, то утверждение AntiSol НЕ является теоремой теории Пеано (то есть, не является словом в языке L). 

Аналогично, при решении вопроса NP vs P необходимо решить вопрос о конкретном алгоритме-решении SolNP(t) с полиномиальным относительно размера слова языка LNP, временем работы. И вопрос этот в том, соответствуют ли результаты работы SolNP(t) языку LNP. И это соответствие для сравнения языка и результатов работы алгоритма – тоже 2-я (Вторая) прикладная роль разбираемого языка. 

Притом эта 2-я прикладная роль «персонализирована» в отношении каждого проверяемого алгоритма, так как проверку на соответствие потенциально можно провести в отношении любого конкретного алгоритма. И, значит, 2-я прикладная роль подразумевает возможность однозначной идентификации конкретного алгоритма – вплоть до получения его программного кода. И такая возможность является принципиальной для нашего дальнейшего исследования.

Первая прикладная роль для языка LNP та, которая определяет его принадлежность к классу сложности NP. Некий алгоритм LcNP(t, y). Подобные алгоритмы будем называть далее «алгоритм проверки». 

Если для языка LNP нет ни одного подходящего SolNP(t), то язык LNP не является языком из класса P и неравенство NP ≠ P доказано.

Но если бы имелся алгоритм SolNP(t), полиномиально быстрый относительно размера |t| и результаты которого соответствуют языку LNP, то данный алгоритм позволил бы задать 3-ю (Третью) прикладную роль для языка LNP. И эта прикладная роль была бы полной и доказала (по определению) принадлежность языка LNP классу сложности P.

По аналогии с теоремой о неопределимости для языка L из логики, можно ожидать аналогичной теоремы и для языка LNP, а вместе с этим и доказательства неравенства NP ≠ P. Но прежде чем пытаться переносить свойства языка L на некий язык LNP – попробуем «перевести» формальную логику и язык L к тому виду, который используется в теории алгоритмов.

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

Error

default userpic

Your reply will be screened

Your IP address will be recorded 

When you submit the form an invisible reCAPTCHA check will be performed.
You must follow the Privacy Policy and Google Terms of use.