Haltingproblemet (datorvetenskap): definition, bevis och olösbarhet

Haltingproblemet: förklaring, formellt bevis och varför det är olösbart — en tydlig genomgång av teori, reduktioner och implikationer för datorvetenskap.

Halting-problemet (även kallat stopp‑problemet) är ett grundläggande beslutsteoretiskt problem inom datavetenskap. Problemet kan formuleras så här: finns det ett algoritmiskt sätt att, givet vilket som helst datorprogram P och dess indata I, avgöra om P med indata I till slut stannar (haltar) eller kör för evigt? Ett program som alltid kan ge detta svar för alla program och indata kallas en beslutsprocedur för halting‑problemet.

Exempel

Två enkla programexempel visar skillnaden mellan program som stannar och som aldrig stannar:

while True:     fortsätt  # kör i en evig slinga  while False:     fortsätt  # stannar omedelbart (körs aldrig)

Dessa exempel är triviala att analysera, men frågan är om det finns någon generell metod som korrekt kan avgöra detta för alla tänkbara program.

Bevisidé — varför problemet är olösbart

Alan Turing visade 1936 att ett sådant allmängiltigt program inte kan finnas. Beviset är ett motsägelsebevis (reduktion till motsatsen) och bygger på att man antar att en sådan beslutsprocedur existerar och sedan konstruerar ett program som leder till motsägelse.

Antag att det finns ett program P som tar emot två argument: ett program F och ett indata I, och returnerar True om F kör för evigt på indatat I, annars False. (Detta är antagandets beslutsprocedur för halting‑problemet.)

def P(F, I):     om F(I) löper för evigt:         returnera True     annars:         returnera False

Med P kan vi definiera ett program Q som använder P för att undersöka vad som händer när ett program körs på en kopia av sig självt:

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

Slutligen konstruerar vi ett program R som beter sig på följande paradoxala sätt: R tar ett program F som indata, frågar Q(F) och gör precis motsatsen till vad Q(F) säger om "F kör på sig själv":

def R(F):     if Q(F):         return   # avsluta     annars:         while True:             continue  # kör för evigt

Nu undersöker vi vad som händer när vi kör R på sig självt, alltså R(R). Två möjligheter finns:

• Antag att R(R) inte kör för evigt (d.v.s. den stannar). Då måste Q(R) ha varit False (eftersom R stannar endast i fallet Q(R) är False). Men Q(R) returnerar P(R, R). Så P(R, R) sade att R(R) inte kör för evigt — vilket innebär att P förutsäger att R(R) stannar. Enligt R:s definition skulle Q(R) = False i så fall göra att R(R) går in i en evig slinga. Detta motsäger antagandet att R(R) stannar.
• Antag istället att R(R) kör för evigt. Då måste Q(R) ha varit True (eftersom R går i en evig slinga endast när Q(R) är True). Men Q(R) returnerar P(R, R), så P(R, R) sade att R(R) kör för evigt. Enligt R:s definition skulle Q(R) = True då få R(R) att avsluta omedelbart. Detta motsäger antagandet att R(R) kör för evigt.

I båda fallen uppstår en motsägelse. Den enda antagande som kan vara fel är att P existerar. Därför kan inget program P finnas som korrekt avgör för alla program och indata om de halter.

Detta är kärnan i Turings bevis för att halting‑problemet är olösbart (undecidable).

Formell förklaring och alternativa formuleringar

Formellt kan man uttrycka problemet så här: det finns ingen algoritm H som för alla kodade program e och indatan x alltid bestämmer om programmet med kod e halter på x. Om man kodar program som naturliga tal blir halting‑mängden H = { (e,x) | program e halter på indata x } icke‑beslutbar.

Beviset använder en diagonaliseringsidé liknande Cantors diagonalisering och bygger på att man kan låta program läsa och köra andra program (och sig själva) — en egenskap som Turingmaskiner och de flesta modeller för beräkning har.

Viktiga konsekvenser

• Ingen universell avslutsgenerator: Det finns inget allmänt verktyg som alltid kan avgöra om ett godtyckligt program stannar. Detta begränsar vad automatiska analysverktyg och verifieringsmetoder kan garantera.
• Semibeslutsbarhet (rekursivt uppräknelig): Halting‑mängden är rekursivt uppräknelig — det finns en algoritm som, givet (F,I), simulerar F på I och om F stannar så upptäcker vi det (och kan då acceptera). Men om F inte stannar kommer simuleringen aldrig att ge något slutligt svar. Alltså kan man känna igen haltereglerna men inte icke‑haltereglerna.
• Vidare olösbarhetsresultat: Genom reduktioner kan man visa att många andra problem om program och deras beteende är olösbara. Ett generellt resultat är Rice's sats (Rice's theorem): alla icke‑triviala semantiska egenskaper hos program är olösliga.
• Praktisk betydelse: I praktisk programanalys används heuristiker, approximativa analyser och formella metoder som fungerar för begränsade språkklasser eller speciella fall, men det finns inga allmängiltiga metoder som garanterat löser problemet för alla möjliga program.

Historisk kommentar

Beviset och konceptet infördes av Alan Turing 1936 i samband med hans arbete om beräkningsbarhet och Turingmaskiner. Resultatet var centralt för framväxten av modern teoretisk datavetenskap och visar gränserna för algoritmers förmåga.

Vidare läsning

• Introduktion till Turingmaskiner och formella språk
• Begrepp som rekursivitet, rekursivt uppräknelighet och beslutsbarhet
• Rice's sats och andra olösbarhetsresultat

Frågor och svar

F: Vad är Halting-problemet?

F: Hur vet vi om ett program löser haltingproblemet?

F: Finns det ett sätt att bevisa att det inte finns något sådant program?

Fråga: Vad gör P?

Fråga: Vad gör Q?

F: Vad gör R?

Fråga: Vad händer när du får R att titta på sig själv?

Sök med bokstav