Задача за спирането

Задачата за спирането е проблем от теорията на алгоритмите: ако са дадени произволна компютърна програма и входни данни за нея, да се определи със сигурност дали програмата някога ще завърши изпълнението си върху тези данни, или ще работи вечно.

През 1936 г. Алън Тюринг доказва, че няма алгоритъм, който да дава отговор на тази задача за всички програми и входни данни. Предизвикателство и впоследствие ключова част от доказателството се оказва намирането на математическо определение за термините компютър и програма. Тюринг постига това с въвеждането на понятието машина на Тюринг. Така става възможно да се докаже, че задачата за спирането е нерешима.

Контекст

Задачата за спирането се отнася за свойство на компютърни програми в пълни изчислителни модели, т.е. всички програми, които могат да бъдат написани на език за програмиране, еквивалентен на машина на Тюринг. Проблемът се състои в това да се определи дали дадената програма при зададените входни данни ще спре (с други думи, ще даде отговор след крайно количество време), или ще се изпълнява безкрайно дълго. В тази абстрактна теоретична постановка не съществуват ресурсни ограничения като количеството изчислителна памет и времето, което ще е нужно на машината, за да реши задачата; програмата, която трябва да определи дали някоя друга програма ще спре, може да използва неограничено количество време и памет, преди самата тя да спре (т.е. да даде отговора, който се търси).

Например следната програма, описана на псевдокод, не спира никога:

while (true) continue

От друга страна, програмата

print „Hello, world!“

спира.

За тези две програми отговорът е лесен, но за по-сложни програми задачата е трудна.

Тюринг доказва, че не съществува алгоритъм, който да дава правилен отговор за всяка програма при произволни входни данни. Това се доказва чрез допускане на противното и достигане до противоречие.

Значение и следствия

Задачата за спирането има историческо значение: тя е първата задача, за която е доказано, че е нерешима. Доказателството на Тюринг е публикувано през май 1936 г., а доказателството на Алонсо Чърч за нерешимостта на съответната задача в ламбда-смятането е от април 1936 г. Двамата работят независимо един от друг над този въпрос. По-късно са открити и множество други нерешими задачи. Типичен метод за доказване на нерешимостта на една или друга задача е свеждането ѝ до вече известна нерешима задача.

Така например, не е възможно да се определи за всяко твърдение относно естествени числа дали е вярно. Тоест не съществува сигурен метод за съставяне на доказателства в аритметиката. Това е така, понеже задачата за спирането може да се преформулира в еквивалентна задача за естествени числа.

Подход към заобикаляне на проблема е предложен от Грегъри Чайтин. Той дефинира вероятността за спиране Ω — това е вероятността случайно избрана програма (машина на Тюринг) да спре. Тази вероятност е трансцендентно число, което може да бъде дефинирано, но не може да бъде изчислено. Може да се докаже, че няма алгоритъм, който да изчислява цифрите на тази трансцендентна дроб, макар че първите няколко цифри могат да бъдат изчислени в някои прости случаи.

Докато доказателството на Тюринг показва, че няма общовалиден метод (алгоритъм), който да определя дали програмите спират, все пак някои частни случаи могат да бъдат решени. За някои алгоритми може да бъде доказано, че ще спрат при всякакви входни данни. Но всяко доказателство трябва да бъде разработено специално за конкретния алгоритъм. Не съществува механично, общовалидно решение, което да важи за всички машини на Тюринг. Съществуват единствено евристични методи, които имат успех в мнозинството случаи. Това направление в информатиката се нарича автоматизиран анализ на приключването.