Проблемът за спиране (Halting) — какво е и защо е неразрешим

Разберете защо проблемът за спиране (Halting) е неразрешим: ясно обяснение и класическо доказателство със самовглеждащи се програми и парадоксални конструкции.

Проблемът за спиране е основен въпрос в теорията на изчислимостта и информатиката. Формулиран накратко, той гласи: съществува ли алгоритъм, който за произволна друга програма и нейния вход може да каже дали тази програма ще спре (завърши) или ще работи вечно? Отговорът е отрицателен: такъв универсален алгоритъм не съществува — проблемът за спирането е неразрешим (undecidable).

Какво означава "решаване на проблема за спиране"

С други думи, търсим програма P, която приема описание на програма F и вход I и връща:

• true, ако F, изпълнена с вход I, никога не спира (работи вечно);
• false, ако F(I) спира (завършва) след краен брой стъпки.

(Обратно формулиране също е възможно: често в литературата се търси алгоритъм, който да казва дали F(I) ще спре — това е еквивалентно формулиране.)

Примери за разбиране

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

while True:     continue;   # зацикля завинаги  while False:     continue;   # никога не изпълнява цикъла и спира веднага 

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

Доказателство по идея на Тюринг (провеждане чрез противоречие)

Доказателството на неразрешимостта е от Алън Тюринг (1936). Идеята е да се предположи, че съществува програма P, която решава проблема за спирането, и да се постигне логическо противоречие чрез конструкция на специални програми.

Да приемем, че съществува P с поведението:

def P(F, I):     if F(I) работи вечно:         return True     else:         return False 

Ползваме P, за да дефинираме следните програми:

def Q(F):     return P(F, F) 

Q взема програма F и пита P дали F, стартирана върху копие на самата себе си, работи вечно.

def R(F):     if Q(F):         return  # прекратява     else:         while True:             continue  # работи вечно 

Сега питаме какво ще се случи, ако стартираме R с аргумент R (т.е. R(R)). Има само две възможни ситуации:

• Ако R(R) не работи вечно (спира), то по дефиниция на R това означава, че Q(R) е вярно. Но Q(R) връща P(R,R), което твърди, че R(R) работи вечно — противоречие.
• Ако R(R) работи вечно, то по дефиниция на R това означава, че Q(R) е невярно. Но Q(R) = P(R,R) е невярно, което означава, че R(R) не работи вечно — пак противоречие.

И в двата случая се стига до логическо противоречие, следователно първоначалното предположение, че съществува P, е невярно. Следователно няма алгоритъм, който да решава общия проблем за спирането.

Ключови идеи и защо доказателството работи

• Доказателството използва самореференция — програми, които получават описанието на себе си като вход.
• Комбинацията от универсален тест P и конструиране на програма, която обръща резултата на този тест при самоприложение, води до парадокс (диагонализация).
• Това е аналогично на други резултати като парадокса на Ламбда-функциите и аргументите на Гьодел за непълнотата — показва естествено ограничение на алгоритмичната способност да решава всички въпроси за поведението на програми.

Точни формулировки и свойства

• Формално: не съществува тотална изчислима функция H, която за произволна двойка (M, w) (Машина на Тюринг M и вход w) решава дали M спира на w.
• Проблемът за спирането е рекурсивно изброим (recursively enumerable, semi-decidable): ако дадена машина M спира на вход w, можем да симулираме M на w и да открием това — в този случай симулаторът ще спре и ще потвърди. Но ако M не спира на w, симулацията ще върви вечно и никога няма да даде отрицателен отговор. С други думи, проблемът е в клас RE, но не и в co-RE.
• От неразрешимостта на проблема за спирането следват и много други неразрешими въпроси чрез редукции (например: дали дадена програма никога няма да отпечата нещо, дали два програми винаги дават еднакъв резултат и др.).

Последствия и приложения

Неразрешимостта има значими практически и теоретични последици:

• Не може да се напише общо верно средство за автоматична проверка, което за всяка произволна програма и вход да каже дали програмата ще спре. Това поставя граници на автоматичното доказване и статичния анализ.
• Много практически инструменти (статични анализатори, проверители на свойства, терминатион проквери) работят със хелпер техники, които са коректни, но непълни — те могат да определят спиране или безпогрешно да намерят грешки в много реални случаи, но няма да работят за всички възможни програми.
• Като следствие от общи резултати като теоремата на Райс (Rice's theorem), всяко нетривиално семантично свойство на програмите е неразрешимо.

Практически бележки

• За реални програмни езици и полезни подмножества от програми често има алгоритмични методи, които работят: например, за ограничени модели (структурирани езикови подмножества, терминиращи логики) може да има автоматични доказатели.
• Верификацията в индустрията използва комбинация от статичен анализ, тестове, интерактивни доказателни асистенти и експертиза — за да се справи с практическите случаи, въпреки теоретичните ограничения.

Това доказателство и ограничение са открити от Алън Тюринг през 1936 г. и остават един от фундаменталните резултати в теорията на изчисленията и компютърните науки.

Въпроси и отговори

В: Какво представлява проблемът за спирането?

В: Как да разберем дали дадена програма решава проблема на спирането?

В: Има ли начин да се докаже, че не съществува такава програма?

В: Какво прави P?

В: Какво прави Q?

В: Какво прави R?

В: Какво се случва, когато накарате R да погледне себе си?

Търсене по буква