e2e4 писал(а):
Профессор Снэйп писал(а):
Ну вот берём мы такое свойство программ (синтаксически правильно написанных): при любых входных данных заканчивать вычисления за конечное число шагов, не впадая в бесконечный цикл. Теорема Райса гарантирует, что не существует другой программы, которая бы по тексту исходной программы распознавала, обладает она или нет этим свойством.
теорема чем-то напоминает теорему Гёделя о неполноте...
Эти вещи действительно тесно связаны между собой.
Как доказывается теорема Гёделя (первая, есть ещё и вторая)? Строится формула, утверждающая свою собственную недоказуемость (из арифметики Пеано). Она не может быть доказуемой, ибо она тогда была бы истинна и недоказуема по своему смыслу. Значит, она недоказуема. Значит, она истинна, а её отрицание (ложное) тоже недоказуемо. Это так, вкратце, я конечно же опускаю многие существенные детали.
Проверка того, что последовательность утверждений является формальным доказательством --- чисто механический процесс, его можно поручить машине. То бишь множество доказуемых формул алгоритмически перечислимо. Если бы мы могли решать проблему остановки, то перечислимые множества были бы разрешимыми и мы могли бы верифицировать (в виде формул) утверждения о недоказуемости конкретных формул, причём они были бы доказуемы. Другими словами, мы могли бы доказывать недоказуемость средствами самой арифметики Пеано и трюк, используемый при доказательстве теоремы Гёделя, уже бы не прошёл. В связи с этим можно считать, что из справедливости теоремы о неполноте следует неразрешимость проблемы остановки.
Обратно, саму проблему остановки можно записать в виде формулы, доказуемость которой была бы равносильна разрешимости проблемы. Таким образом, верно и обратное: справедливость теоремы Гёделя есть следствие неразрешимости проблемы остановки.
Терема Гёделя о неполноте стоит на том, что не существует формулы специального вида (так называемой
-формулы), утверждающей недоказумость других формул (
-формула, утверждающая доказуемость, имеется).
-формулы же замечательны тем, что они определяют в точности те функции, которые алгоритмически вычислимы...
... ... ...
Не уверен сейчас, конечно, что этот навскидку написанный трёп свободен от изъянов. Надо посидеть, повыписывать детали... делать это на ночь глядя пока не хочется. В-принципе, я уже давно не вникал глубоко в вещи, связанные с теоремами о неполноте. Хотя когда-то, несколько лет назад, имел счастье проникнуться ими довольно основательно...
Чего на самом деле всем желаю
.
