Есть такая классическая проблема о том, возможно ли в принципе проанализировать любую программу и предсказать, зависнет она или нет.
Типа доказано, что нет.
Только это доказательство какое-то совсем неубедительное. Слишком оно абстрактное, не поддающееся "приземлению".
Ну то есть, вот допустим я написал такую программу-анализатор, которая принимает на вход начальное состояние виртуальной машины и выдает ответ, остановится она или нет.
Но! Сам процесс анализа запускается на большей машине, которая включает и программу-анализатор и анализируемую машину.
Что такое программа-анализатор, которой скормили ее саму? Получается рекурсия. Машина которая содержит анализатор и (машину, которая содержит анализатор и (машину,...))
Помнится, лет 15 назад, когда впервые услышал о проблеме остановки, натыкался на какое-то более сложное доказательство, не вникал, но там запомнился побочный вывод о существовании верхней границы Колмогоровской сложности.
Здравствуйте, graniar, Вы писали:
G>Есть такая классическая проблема о том, возможно ли в принципе проанализировать любую программу и предсказать, зависнет она или нет.
Только нагрузочное тестирование, только хардкор. И вотчдог к нему в нагрузку.
Здравствуйте, graniar, Вы писали:
G>Что такое программа-анализатор, которой скормили ее саму? Получается рекурсия. Машина которая содержит анализатор и (машину, которая содержит анализатор и (машину,...))
Не пойму, о чём ты. sha256sum /usr/bin/sha256sum прекрасно работает, без всяких рекурсий. Точно так же ты можешь запустить halt-analyzer /usr/bin/halt-analyzer.
Здравствуйте, graniar, Вы писали:
G>Есть такая классическая проблема о том, возможно ли в принципе проанализировать любую программу и предсказать, зависнет она или нет. G>Типа доказано, что нет. G>Только это доказательство какое-то совсем неубедительное.
А ты в курсе, почему алгоритм называется "Диагонализатор"? Он диаги анализирует?
Здравствуйте, vsb, Вы писали:
vsb>Не пойму, о чём ты. sha256sum /usr/bin/sha256sum прекрасно работает, без всяких рекурсий.
Но вообще-то ты нашел хороший пример, это как раз то место, где я считаю доказательство потеряло смысл.
Ведь анализатор анализирует не просто код, а конкретное состояние машины.
А там предлагается анализатору скормить просто код анализатора без его входящих данных.
Здравствуйте, graniar, Вы писали:
G>А там предлагается анализатору скормить просто код анализатора без его входящих данных.
Исследуя математические функции, ты предпочтет иметь дело с уравнениями, а не каким-то набором значений. Можно определить область допустимых значений, экстремумы, разрывы и т.д.
Также и с кодом (помним про частично рекурсивные функции).
Здравствуйте, Nuzhny, Вы писали:
N>Исследуя математические функции, ты предпочтет иметь дело с уравнениями, а не каким-то набором значений. Можно определить область допустимых значений, экстремумы, разрывы и т.д. N>Также и с кодом (помним про частично рекурсивные функции).
Любые уравнения, производные и тд абстракции, все они имеют элементарный смысл, все можно приземлить конкретным примером типа бесконечно малых приращений.
Абстрагирование просто позволяет экономить вычислительные ресурсы, но оно не создает новых выводов.
Здравствуйте, graniar, Вы писали:
A>>А ты в курсе, почему алгоритм называется "Диагонализатор"? Он диаги анализирует?
G>Наверное от слова диагональ, типа тестит диагональные элементы матрицы.
Это отсылка к Кантору. Очень сильное колдунство, лежит в основе мноооого чего, потому что фундаментальное. И поэтому странно читать вот такие наезды:
G>Только это доказательство какое-то совсем неубедительное.
Здравствуйте, Alekzander, Вы писали:
A>Очень сильное колдунство, лежит в основе мноооого чего, потому что фундаментальное.
Непонятное колдунство это как корявый код легаси, может и много где применяется, но не гарантирует от сложно-уловимых уязвимостей.
Очередной аргумент про необходимость формализации математических знаний.
A>И поэтому странно читать вот такие наезды: G>>Только это доказательство какое-то совсем неубедительное.
Ну так весь смысл доказательства — убедить читателя. Почему бы не пожаловаться, если оно с этим не справляется.
Может конкретно это, приведенное в Вики доказательство — некорректно.
Здравствуйте, Alekzander, Вы писали:
A>Это математика, а не суд.
Перефразируя известный анекдот, Я попросил их привести доказательство этой теоремы, на что мне было сказано: "У нас математикам верят на слово". Вот тогда-то во мне и открылся большой математический талант!
Здравствуйте, graniar, Вы писали:
G>Любые уравнения, производные и тд абстракции, все они имеют элементарный смысл, все можно приземлить конкретным примером типа бесконечно малых приращений. G>Абстрагирование просто позволяет экономить вычислительные ресурсы, но оно не создает новых выводов.
Создаёт же. Исследовать бесконечности без соответствующего математического аппарата, а лишь конкретными значениями, ты не сможешь.
Здравствуйте, Nuzhny, Вы писали:
N>Создаёт же. Исследовать бесконечности без соответствующего математического аппарата, а лишь конкретными значениями, ты не сможешь.
Бесконечности — это чистые абстракции, которые не имеют никакого отображения в реальности. И все их можно так или иначе заменить.
Для конкретного примера — допустим есть какое-то сложное выражение с тригонометрическими функциями. Пользуясь тригонометрическими тождествами мы можем его упростить и потом посчитать, разложив в степенные ряды. А можем сразу разложить в степенные ряды и посчитать эту громоздкую конструкцию не пользуясь никакими тригономтерическими тождествами. Результат будет тот же с точностью до погрешности вычисления.
Тоже самое, например, с интегралом. Можно вычислить аналитически, а можно посчитать численным методом.
Здравствуйте, graniar, Вы писали: G>Но! Сам процесс анализа запускается на большей машине, которая включает и программу-анализатор и анализируемую машину.
Поздравляю, вы напоролись на контр-интуитивное поведение бесконечностей.
Все доказательства проблемы останова неявно содержат в себе предположение о том, что как программа, так и её состояние, никак не ограничены по размеру.
Если бы это было не так, то у нас есть совершенно очевидный алгоритм, который прекрасно работает:
1 делаем два экземпляра нашей машины, A и B, инициализируем каждый переданной нам программой и входными данными
2 делаем 1 шаг вычислений на машине А
3 делаем 2 шага вычислений на машине B
4 сравниваем состояние машин:
— если хотя бы одна из них остановилась — программа останавливается
— если ни одна не остановилась, но состояния совпали — программа зацикливается
— иначе — продолжаем с шага 2.
Если пространство состояний машины конечно, то наш алгоритм закончит своё выполнение за конечное количество шагов.
А вот если это пространство — бесконечно, как у МТ, то машина может бесконечно переходить во всё новые и новые состояния, не останавливаясь и не зацикливаясь. И после каждого шага мы по-прежнему не будем знать, остановится она, зациклится, или так и продолжит бесконечное ациклическое выполнение.
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
Здравствуйте, graniar, Вы писали:
G>Для конкретного примера — допустим есть какое-то сложное выражение с тригонометрическими функциями. Пользуясь тригонометрическими тождествами мы можем его упростить и потом посчитать, разложив в степенные ряды. А можем сразу разложить в степенные ряды и посчитать эту громоздкую конструкцию не пользуясь никакими тригономтерическими тождествами. Результат будет тот же с точностью до погрешности вычисления. G>Тоже самое, например, с интегралом. Можно вычислить аналитически, а можно посчитать численным методом.
Нет, это так не работает. Есть устойчивость вычислений, не всё можно вычислить приближённо и рядами. Сначала функцию исследуют на устойчивость, подбирают конкретные методы. Ты сходу не сможешь функцию Бесселя рядами Тейлора посчитать, потому что там в середине ряда будет большой факториал. И вообще, очень много неустойчивых решений, которые преодолеваются как раз аналитическим исследованием.
Здравствуйте, Sinclair, Вы писали:
S>Поздравляю, вы напоролись на контр-интуитивное поведение бесконечностей.
Имхо, "настоящие бесконечности" (в отличие от бесконечно малых/больших но конечных), это бессмысленная, вводящая в заблуждение, синтаксическая конструкция.
Везде, где можно, лучше обходиться без них.
S>Все доказательства проблемы останова неявно содержат в себе предположение о том, что как программа, так и её состояние, никак не ограничены по размеру.
Но первоначальное состояние то ограничено.
Более того, самые простые начальные состояния явно можно проанализировать аналитически.
Значит, если теорема о неразрешимости остановки верна, есть условие некоторого минимального начального размера, или минимальной Колмогоровской сложности состояния.
А что, если переформулировать проблему без бесконечностей, но чтобы она по прежнему имела тот же практический смысл?
S>Если пространство состояний машины конечно, то наш алгоритм закончит своё выполнение за конечное количество шагов.
А если пространство состояний конечно, но наш алгоритм должен закончить свое выполнение за очень большое, но зависящее от начального размера время, например C*exp(exp(size))?
Здравствуйте, Nuzhny, Вы писали:
N>Нет, это так не работает. Есть устойчивость вычислений, не всё можно вычислить приближённо и рядами. Сначала функцию исследуют на устойчивость, подбирают конкретные методы. Ты сходу не сможешь функцию Бесселя рядами Тейлора посчитать, потому что там в середине ряда будет большой факториал. И вообще, очень много неустойчивых решений, которые преодолеваются как раз аналитическим исследованием.
Ну наверное есть какие-то другие элементарные пути. В конце-концов, все практически значимые вопросы относятся к моделированию физической реальности и сама эта реальность может выступать в роли вычисления. Ну это уже пошло больше в область философии, материализм vs идеализм.
Здравствуйте, graniar, Вы писали:
G>Только это доказательство какое-то совсем неубедительное. Слишком оно абстрактное, не поддающееся "приземлению".
Тоже пытался понять, но забил, когда понял, что у нас так-то машина Тьюринга, в которой лента памяти бесконечная. А вот если взять подмножество МТ в виде реальных архитектур да ещё и добавить ограничений (например, запретить безусловный переход), то всё отлично поддаётся анализу, и терминируемость доказывается.
