dmitgu (dmitgu) wrote,
dmitgu
dmitgu

Category:

2. Программа Гильберта и теория алгоритмов

к Оглавлению

Гильберт формализовал процесс доказательства, сделав его проверку доступным даже алгоритмам. Доказательство теперь не только приводило к выводам о некоторых формальных объектах, но и само стало одним из таких формальных объектов, доступных логическому анализу.

Целью такой формализации было применение методов формальной математики к ней самой с целью доказательства непротиворечивости.

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

Итак, в области логической полноты и доказательства непротиворечивости мы получили ответы – пусть и отрицательные. Теперь не решённым и принципиальным стал вопрос о поиске тех доказательств, которые есть. И вопрос это такой:

Вопрос о поиске доказательств

Найдётся ли универсальный алгоритм-решение, который сумеет находить в предоставленной ему теории (произвольной) ответ на вопрос, если этот ответ в теории есть? Найти, например, доказательство интересующей теоремы, если эта теорема имеет доказательство в теории и это доказательство имеет какие-то разумные размеры? А если подходящего доказательства нет, то чтоб алгоритм сообщил и об этом. И чтобы выдавал свои результаты в разумные сроки.

В предыдущем разделе были сформулировали задачи, пригодные для проверки доказательств – задачи из класса NP+. А вопрос о возможности быстро их решать (находить доказательства) – это вопрос о их сводимости к задачам из класса P+.

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

Казалось бы, необходимая формализация проведена математиками ещё в эпоху Гильберта, но нет – для наших целей она слишком «грубая». Та формализация была рассчитана на применение к теориям, без всяких ограничений по размеру доказательств теории и тем более по «времени работы». Последнее («время работы») к доказательству вообще не применимо, но зато является важной характеристикой для работы алгоритма (количество шагов его работы, если он останавливается).

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

1.2. Между корректными теориями и алгоритмами, от которых мы ждём ответа, есть важное отличие в том, что для них означает «отсутствие результата». В теории, например, когда нет доказательства для интересующего нас утверждения, то мы считаем, что «теория не знает». А корректный алгоритм-решение должен выдать ответ, что нужного доказательства нет – что он его не нашёл. То есть – корректный алгоритм-решение должен остановиться с негативным результатом как минимум. Это – принципиальное отличие, которое позволяет корректному алгоритму «понять» свою неспособность к чему-либо, как мы увидим далее.

1.3. Не вдаваясь в детали, напомню, что Гёдель представлял запись логических формул и доказательств как произведение простых чисел в разных степенях. То есть, если в математической формуле/доказательстве некий математический символ стоит на некотором месте, то этот символ и это место задают соответствующее простое число и его степень. И из таких сомножителей получалось число, которое соответствовало данной формуле/доказательству.

Так вот, такое представление формул/доказательств не годится для решения вопросов о полиномиальности времени работы алгоритмов в силу того, что разложение числа на простые сомножители относится к задачам с не решенной сложностью и, видимо, является неполиномиально сложной задачей. На трудности разложения числа на простые сомножители строятся некоторые системы шифрования с открытым ключом. Вычислить произведение простых чисел легко, а вот узнать по заданному числу из каких простых чисел оно состоит – неполиномиально трудно (видимо). И вопрос о (не)равенстве классов P и NP – всего лишь попытка первого приближения к доказательству/опровержению стойкости таких методов шифрования.

1.4. Кроме того, в эпоху Гильберта математики разбирали «стандартную интерпретацию» математических теорий о натуральных числах. А эта интерпретация – о «счётных палочках». Если математик говорил тогда о 10, то это означало 10 каких-то единиц. Тогда число 11234 будет соответствовать не строке из 5 цифр, а более чем 11000 единицам и такая интерпретация – заведомо неполиномиальная относительно привычного для нас десятичного представления чисел. И даже аргументы для алгоритмов на ленте машины Тьюринга понимались в такой же «стандартной интерпретации» как блоки единиц. Будем называть модель стандартной интерпретации «интерпретация S».

Разумеется, когда мы решаем вопрос о полиномиальности работы алгоритмов, то мы не можем считать запись аргумента алгоритма в виде блока единиц приемлемой. Тогда 11234 будет записано блоком единиц длинной более 11000 штук, а обычные компьютерные алгоритмы запишут тот же аргумент в паре байт. И как мы в интерпретации S сможем тогда получать правильные выводы о полиномиальных компьютерных алгоритмах, если в нашей интерпретации они изначально неполиномиальны? Никак. Поэтому нам надо пользоваться моделью интерпретации C:


Tags: NP≠P дискуссии, ЖЖвЖЖ математика
Subscribe

  • Post a new comment

    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.
  • 0 comments