Проблема останова для машины Тьюринга

[Котельников Евгений]

Хочу задать вопрос, который меня волнует довольно давно.

Как известно, для машины Тьюринга существует т.н. <<проблема останова>>,
т.е. невозможность в общем случае установить, закончит ли она свою
работу или будет работать вечно. Обычно после этого делают следствие,
что, мол, раз обыкновенная ЭВМ -- это тоже МТ, то подобная проблема
есть и здесь. Это выражается в том, что нельзя узнать, зациклилась ли
программа, или просто выполняется очень долго.

Но вот в чем вопрос. ЭВМ -- это ведь не просто какая-то там сферическая
машина Тьюринга в вакууме, а её конкретная разновидность, называемая
МТ с конечной лентой (коль скоро память компьютера конечна). Главная
особенность такой машины как раз в отсутствии проблемы останова, для
чего есть несложное конструктивное доказательство. Раз лента конечна,
то и количество возможных конфигураций МТ конечно. Значит, если если
какая-либо конфигурация встречается дважды, машина зациклена.

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

Что думаете?

[Vladimir Ivanov]

Какой-то килобайт памяти - это 2^8192 возможных состояний системы =)

Удобно различать теоретическую и практическую неразрешимость.

Halting problem - классический пример теоретически неразрешимой задачи
(undecidable problem). Красиво и просто. Наверное, поэтому так и
популярна.

Классы сложности P и NP приближенно описывают множество задач,
разрешимых на практике (tractable problems). Пусть и "с точностью до
констант".

На практике различия между undecidable и intractable нет. Пусть для
первого класса неразрешимость доказана строго, а для последнего просто
ещё неизвестен эффективный алгоритм или же не установлен факт
существования/отсутствия такового.

Если Вас интересует конструктивный подход, то стоит взглянуть на
проблему немного иначе - не пытаться анализировать произвольные
алгоритмы, а пытаться создавать систему, которая будет обладать
необходимыми свойствами. Например, никогда не зацикливаться
(totality). Да, система уже не будет Turing-complete (будут
существовать вычислимые фунции, которые невозможно описать в рамках
данной системы), но это компромисс - взамен можно получить другие
полезные свойства.

Можете посмотреть на достижения в области автоматической верификации
программ (formal verification, automated theorem proving,
proof-carrying code, total programming languages). Я не особо в курсе,
но, похоже, что в hardware industry формальные методы - уже стандарт.

2009/11/17 Котельников Евгений <php....@gmail.com>: