?

Log in

No account? Create an account
Чайтин, окончание - Поклонник деепричастий [entries|archive|friends|userinfo]
Anatoly Vorobey

[ website | Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Links
[Links:| English-language weblog ]

Чайтин, окончание [ноя. 28, 2002|11:04 pm]
Anatoly Vorobey
[Настроение |contentcontent]

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


Итак, я закончил в прошлый раз на том, что для любой формальной системы (например, теории множеств) существует число 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 у нас будет формальное доказательство её элегантности. Но это как раз и противоречит полученному нами в прошлом пункте доказательству того, что наши способности в этом деле весьма ограниченны.



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

Comments:
From: ex_ilyavinar899
2002-11-28 03:48 pm
Я подробно не читал твой постинг, но множество подобных результатов содержатся в книжке Kolmogorov Complexity and Its Applications by Li and Vitanyi.
(Ответить) (Thread)
[User Picture]From: lnvp
2002-11-28 03:57 pm
Интересные и приятные (элегантные :^) ) результаты. Спасибо большое (и за первую серию тоже)!
(Ответить) (Thread)
[User Picture]From: marta_pops
2002-11-29 04:24 am

Оффтопик страшный

Уважаемый Анатолий, посоветвали спросить у вас.
Не могу залогиниться. LJ выдает следующее:

path=/; domain=.livejournal.com Set-Cookie: permlogin=; expires=Thursday, 01-Jan-1970 00:00:00 GMT; path=/ Set-Cookie: permlogin=; expires=Thursday, 01-Jan-1970 00:00:00 GMT; path=/; domain=.livejournal.com Set-Cookie: ljfastserver=; expires=Thursday, 01-Jan-1970 00:00:00 GMT; path=/ Set-Cookie: ljfastserver=; expires=Thursday, 01-Jan-1970 00:00:00 GMT; path=/; domain=.livejournal.com Cache-Control: private, proxy-revalidate Pragma: no-cache ETag: "77679aef04fa8f5313e13dbc95cd84f1" Content-Type: text/html; charset=utf-8 Content-Language: en Expires: Fri, 29 Nov 2002 11:59:41 GMT X-Cache: MISS from www.livejournal.com Transfer-Encoding: chunked Connection: close ¯ ·d ¸593

Что же делать?
(Ответить) (Thread)
[User Picture]From: avva
2002-11-29 04:41 am

Re: Оффтопик страшный

Честно говоря, не знаю. Возможно, какая-то проблема с прокси по дороге.
(Ответить) (Parent) (Thread)
[User Picture]From: marta_pops
2002-11-29 04:43 am

Re: Оффтопик страшный

может где еще спросить?
(Ответить) (Parent) (Thread)
[User Picture]From: avva
2002-11-29 04:44 am

Re: Оффтопик страшный

Есть такая штука - support.
(Ответить) (Parent) (Thread)
(Удалённый комментарий)
[User Picture]From: avva
2002-11-29 07:33 am

Re: вопрос можно? :)

Клуб в смысле реальный, помещение?
(Ответить) (Parent) (Thread)
[User Picture]From: sapfo
2002-11-30 06:00 pm

Re: вопрос можно? :)

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

наверное, тут и возникнут сложности?
(Ответить) (Parent) (Thread)
[User Picture]From: avva
2002-12-01 10:48 am

Re: вопрос можно? :)

Боюсь, что да ;)

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

С точки зрения интернациональных законов я не очень знаю, что происходит.

С точки зрения "а может, мы и не против, нам-то что", я сейчас узнаю это у Брэда, как только получу ответ, сообщу ;)
(Ответить) (Parent) (Thread)
[User Picture]From: avva
2002-12-01 10:56 am

Re: вопрос можно? :)

О, Брэд уже ответил.

Он не против совершенно и даже приветствует это, но при условии, что есть соответствующий дисклеймер о том, что Ваш клуб не связан напрямую (not associated - не уверен, как это правильно переводят) с сайтом LiveJournal.com. Т.е. понятно, что не надо об этом на униформах официантов писать ;) но, предположим, если есть меню с символикой, то где-нибудь в нём пусть будет такого рода дисклеймер. Это возможно по-Вашему?

Ещё он пишет:
I just want pictures. And she should tell people to get paid accounts,
or something. :)

Второе предложение скорее шутка, а первое скорее всерьёз ;)
(Ответить) (Parent) (Thread)
[User Picture]From: sapfo
2002-12-01 11:44 pm

Re: вопрос можно? :)

супер :)))) спасибо.

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

так что если остальные два члена проекта поддержат идею жж-клуба, дело будет :)))
(Ответить) (Parent) (Thread)
[User Picture]From: avva
2002-12-02 01:06 am

Re: вопрос можно? :)

Здорово, всяческой удачи Вам. Будет здорово, если выйдет, по-моему ;)
(Ответить) (Parent) (Thread)
[User Picture]From: malaya_zemlya
2002-11-29 01:13 pm
ЖЖ, собака, зажевал пол-поста. Вторая попытка...

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

Интересно, а с квантовыми компьютерами кто-нибудь подобным образом разбирался?
(Ответить) (Thread)
[User Picture]From: avva
2002-11-29 05:03 pm

Re:

Вы совершенно правы насчёт маленьких программ, мне это тоже в голову пришло.

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

(Ответить) (Parent) (Thread)
[User Picture]From: malaya_zemlya
2002-11-29 07:27 pm

Re:

я думаю, что квантовые компьютеры могут иметь дополнительные ограничения по сравнению с классическими ввиду своей обратимости.

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




(Ответить) (Parent) (Thread)
[User Picture]From: avva
2002-12-02 10:57 am

Re:

Обратимый компьютер может симулировать необратимые вычисления - это впервые доказал Беннетт в 73-м году.

(я об этом только знаю, саму статью Беннетта не читал)

C.H.Bennett, Logical Reversibility of Computation
IBM J. Res. Develop. 17:525-532, 1973.

См. также http://www.cwi.nl/~paulv/physics.html
и статью "Reversible simulation of irreversible computation" на ней, там есть другие ссылки и введение в тему. Я её сейчас нашёл специально, чтобы выцепить ссылку на Беннетта, которой под рукой не оказалось.
(Ответить) (Parent) (Thread)
[User Picture]From: malaya_zemlya
2002-12-02 08:18 pm

Re:

Я сейчас готовлю более обстоятельный ответ, а пока
вот нашел указанную статью Бенетта в электронном виде:

http://www.aeiveos.com/~bradbury/Authors/Computing/Bennett-CH/LRoC.html
(Ответить) (Parent) (Thread)
[User Picture]From: avva
2002-12-04 04:48 pm
Спасибо, с удовольствием почитал. Правда, за всеми подробностями не следил, только за общей идеей, но вроде всё кашерным выглядит.
(Ответить) (Parent) (Thread)