Anatoly Vorobey (avva) wrote,
Anatoly Vorobey
avva

Category:
  • Mood:

Чайтин, окончание

Напишу окончание начатого неделю назад введения в базисные идеи Чайтина.


Итак, я закончил в прошлый раз на том, что для любой формальной системы (например, теории множеств) существует число N, так что эта формальная система не может ни для какой конкретной строки X доказать, что она имеет сложность больше N. И как частный случай этого - не может доказать ни для одной строки X длиной N или больше, что она случайна.

Осталось собственно написать две простых вариации на эту тему. Одна, очень красивая и очень легко следующая из уже вышеизложенного, касается элегантных программ.

Пусть у нас есть программа длиной N бит, которая, когда мы её запускаем, выдаёт какую-то строку на выходе. Назовём нашу программу элегантной, если нет никакой другой программы длиной меньше N бит, которая выдаёт ту же строку.

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

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

Доказательство будет очень похоже на случай со сложностью строк. Во-первых, условимся в точности, что значит "доказать элегантность программы размером больше N". Скажем, с формальной точки зрения это будет формула ψp,N, которая утверждает следующее:
"p является кодом некоторой машины Тюринга, которая, если её запустить, в конце концов остановится и выдаст на выходе строку S, и более того, если k - код любой другой машины Тюринга, которая в конце концов останавливается и выдаёт строку S, то размер машины k не меньше размера машины p; и кроме того, размер машины p больше N".
Такое описание уже легко скрупулёзно формализовать.

Предположим теперь, что для какого-то N в нашей формальной системе есть доказательства вида ψp,N, для каких-то программ p (одной или более, чем одной, неважно). Напишем следующую программу, размер которой зависит от N:
Наша программа генерирует все возможные формальные док-ва в нашей системе одно за другим в порядке их длины. Затем она проверяет правильность таких доказательств, и если док-во верно, проверяет, не доказывает ли оно строку вида ψp,N, для нашего N, и для любого p. Как только программа находит такое доказательство, она берёт это самое p - код машины Тюринга, и запускает её на универсальной машине Тюринга - т.е. симулирует её пробег. Когда этот пробег заканчивается, наша программа выдаёт на свой выход именно ту строку, что выдала p во время своего "виртуального" пробега.

Что делает наша программа? Она находит какую-то машину Тюринга длиной больше N, для которой есть формальное док-во её элегантности, и запускает её, выдавая затем её выходные данные в качестве своих. Пусть p будет та машина Тюринга, к-ю наша программа первой найдёт (а какую-то она найдёт, т.к. мы предположили, что для данного N есть доказательства элегантности каких-то программ размером больше N). Тогда ясно, что наша программа и p выдают одинаковый результат.

Каков размер нашей программы? В ней есть несколько кусков постоянного размера - генератор всех доказательств, модуль, проверяющих их на верность, модуль, реализующий универсальную машину Тюринга для запуска на ней любой другой машины. И только один кусок переменного размера - само число N, для записи которого требуются log(N) двоичных знаков. Итак, длина нашей программы - log(N)+c, где c - какая-то константа. А длина элегантной программы p, выдающей тот же результат - больше N по определению.

Теперь уже всё понятно. Для достаточно большого N будет выполнятся N > log(N)+c, и мы получим противоречие: с одной стороны, программа p элегантна, с другой стороны, программа короче её (длиной log(N)+c) выдаёт тот же результат. Это противоречие заставляет нас признать, что для таких N не существует формальных доказательств элегантности ни одной программы длиннее N. Что и требовалось доказать.



И последний, несколько неожиданный результат - простое доказательство невозможности решения проблемы остановки с помощью элегантности программ. Напомню, что проблема остановки (the halting problem) сформулирована так: при наличии машины Тюринга и начальных данных (аргументов) для неё, определить, остановится она когда-нибудь, если её запустить на этих входных данных, или нет. Самым первым нетривиальным результатом в теории вычислимости как раз и было доказательство Тюрингом того факта, что проблему остановки решить невозможно.

Стандартное доказательство этого факта выглядит так. Предположим, что какой-то алгоритм, т.е. какая-то машина Тюринга M решает проблему остановки. Теперь соорудим новую хитрую машину Тюринга D, использующую M внутри себя в качестве "подпрограммы", и "скормим" эту D самой M, попросив M выяснить, остановится когда-нибудь D или нет. При этом D сконструирована так хитро, что мы получаем противоречие при любом возможном ответе M. Отсюда следует, что M не может существовать.

(следующие два абзаца - для желающих увидеть это классическое доказательство во всех подробностях. Те, кому неинтересно, могут их пропустить. Сначала мы предполагаем, что существует машина M, которая решает проблему остановки. Машина M таким образом получает два аргумента: строку, являющуюся описанием какой-то машины Тюринга, и строку, являющуяся начальными аргументами: M(T, A). Когда М запускают, она проверяет, остановится ли машина T если запустить её с аргументами A, и отвечает "да" или "нет". Теперь мы конструируем машину D, которая действует следующим образом. Она получает один аргумент X, и запускает машину M (симулирует её пробег) на аргументах (X,X) -- даёт X машине M и в качестве описания машины, и в качестве описания аргумента. Если M(X,X) отвечает "нет", то D отвечает "да". Если M(X,X) отвечает "да", то D входит в бесконечный цикл и никогда не останавливается.

Теперь мы запускаем нашу машину M в свою очередь с аргументами (D,D), т.е. спрашиваем её, что будет, если машину D запустить с аргументом, равным её собственному описанию. Что может ответить M? Если она ответит "да", это значит, что D(D) остановится, но из описания D это может случится, только если M(D,D) ответит "нет". Если она ответит "нет", это значит, что D(D) никогда не остановится, но из описания D следует, что это может случится, только если M(D,D) ответит "да". Таким образом, если M(D,D) равно "да", то оно равно "нет", а если оно равно "нет", то оно равно "да". Мы получаем противоречие, которое и доказывает, что M существовать не может)


Теперь докажем то же самое утверждение - невозможность решения проблемы остановки - путём Чайтина. Это оказывается очень просто.

Предположим, что есть алгоритм для решения того, останавливается данная машина Тюринга на данных исходных данных, или нет. Тогда есть также алгоритм для решения того, является данная программа элегантной или нет. Почему? Очень просто. Пусть нам дали программу p длиной N, и спрашивают элегантная ли она. Переберём все возможные программы длиной меньше N (их конечное число), и для каждой из них спросим с помощью алгоритма решения проблемы остановки, останавливается ли она. Если да, то запустим её и проверим, когда она остановится, не равен ли её результат результату работы p. Если хотя бы для одной программы будет равен, p не элегантна; иначе p элегантна.

Возможность узнать, какие программы останавливаются, даёт нам "безопасный" способ запустить все программы, которые мы хотим запустить, и проследить их исполнение до результата. Без решения проблемы остановки такой метод не сработал бы, т.к. мы не могли бы заранее знать, не попадём ли случайно на программу длиной меньше N, которая никогда не останавливается, и не "зависнем" ли вместе с ней, запуская её.

Но если у нас есть алгоритм для решения того, какие программы элегантны, мы можем теперь результат работы этого алгоритма преобразовать в формальное доказательство того факта, что p элегантна (ведь мы используем формальную систему, которая формализует всю математику, включая все наши предыдущие рассуждения!). Значит, для любой элегантной программы p у нас будет формальное доказательство её элегантности. Но это как раз и противоречит полученному нами в прошлом пункте доказательству того, что наши способности в этом деле весьма ограниченны.



На этом я, пожалуй, закончу. Если кому-то интересно узнать больше о работах Чайтина, например о замечательном числе Омега, можно обратиться к статьям самого Чайтина на его сайте, например, тем, ссылки на которые я дал в прошлой записи, а после них - к более продвинутым.
Subscribe
  • Post a new comment

    Error

    default userpic

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