Stopproblemet (halting-problemet): Turings bevis for uafgørlighed i datalogi

Halting-problemet (stopproblemet): Turings bevis for uafgørlighed forklaret med intuition, kodeeksempler og betydning for beregnelighed og datalogi.

Halting-problemet (på dansk ofte kaldt stopproblemet) er et centralt problem inden for datalogi og computability-teori. Problemet lyder enkelt: givet et vilkårligt computerprogram og dets input, kan vi afgøre, om programmet på det givne input stopper (terminerer) eller kører videre i al evighed? Et program siges at "løse stopproblemet", hvis det for ethvert andet program og ethvert input kan afgøre, om det andet program vil køre for evigt eller ej.

Enkle eksempler

For at illustrere forskellen mellem et program, der kører uendeligt, og et der stopper, kan man se på to små eksempler:

while True: continue;

Dette program kører i en evighed.

while False: continue;

Dette program stopper straks.

Idéen i beviset (skitse)

Det viser sig, at der ikke findes noget program, der løser stopproblemet for alle mulige indgange. Beviset er en klassisk modstridsargument (reduktion til det absurde) opfundet af Alan Turing i 1936. Fremgangsmåden er at antage, at et sådant program findes, og så vise, at denne antagelse fører til en logisk umulighed.

Antag at der findes et program P, der kan afgøre, om et program F, kørt med input I, kører for evigt. (Bemærk: i denne skitse beskrives P sådan, at det returnerer True netop når F(I) kører for evigt — samme bevis kan formuleres med den modsatte sandhedsværdi ved en lille ændring i konstruktionen.) Formelt kan man tænke på P som en funktion:

def P(F, I):     hvis F(I) kører for evigt: return True     ellers: return False

Når vi antager, at P eksisterer, kan vi konstruere nye programmer baseret på P. Først bygger vi:

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

Q(F) spørger altså: "Vil F, når det får sin egen kildekode som input, køre for evigt?"

Dernæst bygger vi et program R, som bruger Q i sin definition:

def R(F):     if Q(F):         return   # stopper     else:         while True:             continue  # kører for evigt

Tænk nu over, hvad der sker, hvis vi lader R køre på sin egen kildekode, altså R(R). Der opstår to muligheder — og begge fører til en modstrid:

• Antag, at R(R) ikke kører for evigt (dvs. det stopper). Så er P(R,R) = False, altså Q(R) = False. Men Q(R) = False medfører, at R(R) går ind i en uendelig løkke. Det strider mod antagelsen om, at R(R) stopper.
• Antag, at R(R) kører for evigt. Så er P(R,R) = True, altså Q(R) = True. Men Q(R) = True medfører, at R(R) straks returnerer (stopper). Det strider mod antagelsen om, at R(R) kører uendeligt.

I begge tilfælde fås en logisk umulighed. Den eneste antagelse, der kunne være forkert, er at P eksisterer. Derfor findes der ikke noget program P, som altid kan afgøre, om et vilkårligt program kører for evigt — stopproblemet er uafgørligt (undecidable).

Formel betydning og konsekvenser

Konklusion: Der findes intet generelt algoritmisk middel til at afgøre for alle programmer og alle input, om programmet terminerer. Dette er et fundamentalt resultat: nogle spørgsmål om programmer kan ikke afgøres af nogen algoritme.

Nogle vigtige videre pointer:

• Halting-problemet gælder oprindeligt for Turing-maskiner, men resultatet oversættes direkte til de fleste realistiske modeller for beregning (f.eks. moderne programmeringssprog): ingen algoritme kan løse problemet i al almindelighed.
• Halting-problemet er semibeslutsomt i én retning: man kan opbygge et program, som simulerer F(I) og hvis simulationen når en afsluttende tilstand, melder "stop" — derved kan man bekræfte tilfælde hvor F(I) stopper. Men der findes ingen algoritme, der i alle tilfælde både kan bekræfte og afkræfte stop (dvs. problemet er ikke beslutsomt).
• Bevismetoden bruger selvreference og diagonaliseringsidéer og ligger tæt op ad andre umulighedsresultater (Cantors diagonalargument, Gödel's ufuldstændighedssætninger). Den danner grundlaget for mange andre uafgørlighedsresultater, fx Rice's sætning, som siger, at enhver ikke-triviel egenskab ved funktionens adfærd for programmer er uafgørlig.

Praktisk betydning

Selvom stopproblemet er uafgørligt i fuld generalitet, arbejder softwareudviklere og forskere ofte med begrænsede versioner eller heuristikker, som fungerer i praksis for mange konkrete situationer (fx statisk kodeanalyse, termination-proofs for bestemte programkategorier). Resultatet betyder dog, at der aldrig kan findes én automatisk metode, som pålideligt afgør termination for alle tænkelige programmer.

Beviset og idéerne bag stopproblemet er et af de mest grundlæggende resultater i moderne teoretisk datalogi og har dybe konsekvenser for, hvad der er beregneligt.

Spørgsmål og svar

Q: Hvad er Halting-problemet?

Spørgsmål: Hvordan ved vi, om et program løser halting-problemet?

Spørgsmål: Kan man på nogen måde bevise, at der ikke findes et sådant program?

Spørgsmål: Hvad gør P?

Spørgsmål: Hvad gør Q?

Spørgsmål: Hvad gør R?

Spørgsmål: Hvad sker der, når man får R til at kigge på sig selv?

Søg efter bogstav