Проблема остановки и память
От: Куть  
Дата: 15.09.15 20:08
Оценка: 6 (1)
Привет всем!
Недавно читал на хабре статью "Неразрешимые задачи и нижние оценки. Лекция Александра Шеня в Яндексе".
В очередной раз послушал о неразрешимости проблемы остановки. И мне не даёт покоя одна мысль, которой хочу с вами поделиться.
Суть проблемы остановки в следующем: доказано, что не существует программы (Анализатора), которому на вход подаётся программа, а на выходе — true, если программа останавливается и false, если она не останавливается.
Все доказательства неразрешимости проблемы остановки основываются на том, что у программ в распоряжении бесконечная память (бесконечная лента в машине Тьюринга).
Но, если мы требуем от Анализатора конечное время для остановки, и скорость работы Анализатора так же конечна, то логично было бы потребовать от программ работать с конечной памятью.

А с конечной памятью проблема останова становится разрешимой, Анализатор существует.

Доказательство:
Анализатор будет использовать виртуальную машину для запуска программ. Пусть "состояние" — это текущий снимок программы (слепок памяти, состояние регистров — всё то, что однозначно определяет условные переходы). Если дано "состояние 1", то с помощью виртуальной машины можно однозначно определить "состояние 2", в котором программа будет на следующем шаге, то есть мы имеем односвязный список состояний. Если программа останавливается, то список состояний не имеет циклов. Если программа не останавливается, то список состояний обязательно содержит цикл (т.к. память конечна, то и количество состояний конечно). Задача свелась к поиску цикла в односвязном списке, которую любят задавать на собеседованиях. А эта задача имеет решение.

У меня 3 вопроса:
1. Есть ли ошибки в моём доказательстве?
2. Может ли иметь теоретическое или практическое применение Анализатор для программ с конечной памятью?
3. Что ломается в доказательствах неразрешимости при ограничении памяти?
проблема остановки
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.