Сообщение Re[3]: Проблема Остановки от 23.06.2023 8:51
Изменено 23.06.2023 9:59 cppguard
Re[3]: Проблема Остановки
Здравствуйте, graniar, Вы писали:
G>Реальных архитектур, имеешь в виду с ограничением по используемой памяти? В стиле, как Sinclair выше привел, или нечто более практичное?
Возможно, неправильно выразился. На практике, если нужно доказать алгоритм, то берут конкретную архитектуру и конкретный алгоритм. Если нужно, то модифицируют его. Постановку задачу останова часто неправильно понимают из-за запутанной формулировки. Кажется, что теорема гласит "терминируемость программы невозможно доказать", а в реальности — невозможно доказать терминируемость в общем случае, поэтому и доказательство вида "вот есть программа, для которой невозможно доказать, что она остановится". Но, скажем, int main() { return 0; } вполне себе доказуема в плане останова. Таким образом ценность теоремы в том, что она говорит учёным "не пытайтесь найти универсальный способ анализа алгоритма на предмет останова, корректности и т.д. — в общем случае это невозможно".
И в этом плане сабж перекликается с печально известной гипотезой P = NP. В интернетах любят пугать квантовыми компьютерами и тем роковым днём, когда P = NP будет доказано, и сотни банков падут по всему миру, вода поднимается на 33 метра, а живые позавидуют мёртвым. А на деле, если доказать, что P = NP, то никоим образом полиномиальный алгоритм факторизации простых чисел не возникнет, его ещё нужно будет придумать.
G>Реальных архитектур, имеешь в виду с ограничением по используемой памяти? В стиле, как Sinclair выше привел, или нечто более практичное?
Возможно, неправильно выразился. На практике, если нужно доказать алгоритм, то берут конкретную архитектуру и конкретный алгоритм. Если нужно, то модифицируют его. Постановку задачу останова часто неправильно понимают из-за запутанной формулировки. Кажется, что теорема гласит "терминируемость программы невозможно доказать", а в реальности — невозможно доказать терминируемость в общем случае, поэтому и доказательство вида "вот есть программа, для которой невозможно доказать, что она остановится". Но, скажем, int main() { return 0; } вполне себе доказуема в плане останова. Таким образом ценность теоремы в том, что она говорит учёным "не пытайтесь найти универсальный способ анализа алгоритма на предмет останова, корректности и т.д. — в общем случае это невозможно".
И в этом плане сабж перекликается с печально известной гипотезой P = NP. В интернетах любят пугать квантовыми компьютерами и тем роковым днём, когда P = NP будет доказано, и сотни банков падут по всему миру, вода поднимается на 33 метра, а живые позавидуют мёртвым. А на деле, если доказать, что P = NP, то никоим образом полиномиальный алгоритм факторизации простых чисел не возникнет, его ещё нужно будет придумать.
Re[3]: Проблема Остановки
Здравствуйте, graniar, Вы писали:
G>Реальных архитектур, имеешь в виду с ограничением по используемой памяти? В стиле, как Sinclair выше привел, или нечто более практичное?
Возможно, неправильно выразился. На практике, если нужно доказать алгоритм, то берут конкретную архитектуру и конкретный алгоритм. Если нужно, то модифицируют его. Постановку задачу останова часто неправильно понимают из-за запутанной формулировки. Кажется, что теорема гласит "терминируемость программы невозможно доказать", а в реальности — невозможно доказать терминируемость в общем случае, поэтому и доказательство вида "вот есть программа, для которой невозможно доказать, что она остановится". Но, скажем, int main() { return 0; } вполне себе доказуема в плане останова. Таким образом ценность теоремы в том, что она говорит учёным "не пытайтесь найти универсальный способ анализа алгоритма на предмет останова, корректности и т.д. — в общем случае это невозможно".
И в этом плане сабж перекликается с печально известной гипотезой P = NP. В интернетах любят пугать квантовыми компьютерами и тем роковым днём, когда P = NP будет доказано, и сотни банков падут по всему миру, вода поднимается на 33 метра, а живые позавидуют мёртвым. А на деле, если доказать, что P = NP, то никоим образом полиномиальный алгоритм факторизации простых чисел не возникнет сам собой, его ещё нужно будет придумать.
G>Реальных архитектур, имеешь в виду с ограничением по используемой памяти? В стиле, как Sinclair выше привел, или нечто более практичное?
Возможно, неправильно выразился. На практике, если нужно доказать алгоритм, то берут конкретную архитектуру и конкретный алгоритм. Если нужно, то модифицируют его. Постановку задачу останова часто неправильно понимают из-за запутанной формулировки. Кажется, что теорема гласит "терминируемость программы невозможно доказать", а в реальности — невозможно доказать терминируемость в общем случае, поэтому и доказательство вида "вот есть программа, для которой невозможно доказать, что она остановится". Но, скажем, int main() { return 0; } вполне себе доказуема в плане останова. Таким образом ценность теоремы в том, что она говорит учёным "не пытайтесь найти универсальный способ анализа алгоритма на предмет останова, корректности и т.д. — в общем случае это невозможно".
И в этом плане сабж перекликается с печально известной гипотезой P = NP. В интернетах любят пугать квантовыми компьютерами и тем роковым днём, когда P = NP будет доказано, и сотни банков падут по всему миру, вода поднимается на 33 метра, а живые позавидуют мёртвым. А на деле, если доказать, что P = NP, то никоим образом полиномиальный алгоритм факторизации простых чисел не возникнет сам собой, его ещё нужно будет придумать.