Стоп-проблем

Стоп-проблемът (на английски: halting problem) е проблем теорията на изчислимостта, който се състои в това дали е възможно да бъде определено, ако е дадена произволна компютърна програма и дадени входни данни за нея, дали програмата някога ще завърши или ще работи безкрайно много време.

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

Контекст

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

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

while (true) continue

не спира никога; тя се изпълнява в безкраен цикъл. От друга страна, програмата

print „Hello, world!“

спира.

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

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

Важност и последствия

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

Така например, едно от последствията от нерешимостта на стоп-проблема е нерешимостта на проблема за това дали е възможно да се определи дали всяко твърдение за естествените числа е вярно или не. Това е така, понеже твърдението, че дадена програма винаги спира, при дадени входни данни, може да се преобразува в еквивалентно твърдение за естествените числа. Ако даден алгоритъм решава дали дадено твърдение за естествените числа е вярно, то той може да каже дали предното твърдение (еквивалентно на задачата за спирането, но за естествените числа) е вярно. Но това е невъзможно, понеже проблемът за спирането е нерешим.

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

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

Неразрешен научен въпрос остава задачата за това да се намери детерминистичен физически процес, който да бъде контролиран по някакъв начин и чиито резултат да е резултат на изчисление; такъв процес би могъл да бъде използван като изчислителна машина − хиперкомпютър − който евентуално би могъл да разреши стоп-проблема.