Stopprobleem

Het zwarte plan:, Operatie Cinderella

Het stopprobleem, ook bekend als het 'halting problem', is het beslissingsprobleem uit de wiskunde en informatica, om te bepalen of een algoritme bij een eindige invoer in een eindig aantal stappen eindigt of dat het eindeloos blijft doorgaan. Het is een bekend voorbeeld van een wiskundig probleem dat onbeslisbaar is, en een van de eerste als dusdanig herkende problemen. Dit werd bewezen door Alan Turing in 1936.

DefinitieBewerken

Het stopprobleem is informeel gedefinieerd het volgende beslissingsprobleem:

Gegeven een programma   en een invoerwaarde  , bepaal of   met invoer   na een eindig aantal stappen wel of niet stopt.

Om het stopprobleem formeel te definiëren, moeten we afspreken wat we onder het begrip programma verstaan. Oorspronkelijk werd het stopprobleem voor turingmachines geformuleerd, maar analoog kan het ook voor andere turingvolledige formalismes worden gedefinieerd.

De invoer van een turingmachine bestaat uit een rij symbolen, een tekenreeks. Om turingmachines als invoer voor andere turingmachines op te kunnen vatten, moeten we ze eerst coderen, of programmeren. We kunnen bijvoorbeeld alle Turingmachines op een rij zetten, en dan het volgnummer in deze rij als de code voor de turingmachine gebruiken. Als   een code voor een turingmachine is, dan schrijven we   voor de turingmachine die door   gecodeerd wordt. Bovendien schrijven we   voor de code van het paar  . Het stopprobleem kan nu formeel als volgt worden gedefinieerd:

 

Beslissingsproblemen worden ook vaak gedefinieerd als de verzameling van positieve invoerwaardes, dus alternatief luidt de definitie van het stopprobleem:

 

OnbeslisbaarheidBewerken

Alan Turing bewees in 1936 dat het stopprobleem onbeslisbaar is. Dat betekent dat er geen turingmachine bestaat die in alle gevallen correct beslist, of een turingmachine met een bepaalde invoerwaarde in een eindig aantal stappen stopt of niet.

Bewijs dat het stopprobleem onbeslisbaar is
  • De onberekenbaarheid van het stopprobleem wordt bewezen met een bewijs uit het ongerijmde. Neem daarom aan dat er een programma halt(A, x) is, dat als het algoritme A wordt toegepast op de invoer x, het als resultaat "1" geeft als het eindigt , en het resultaat "0" als het niet eindigt.
  • Vorm nu het algoritme paradox(A), dat voor een algoritme A een waarde geeft, geeft niet welke, als halt(A, A) het resultaat 0 oplevert, en oneindig door blijft gaan als halt(A, A) het resultaat 1 oplevert.
  • De vraag is nu, eindigt het algoritme paradox als het paradox als invoer krijgt?
  • Indien ja, dan zal volgens de definitie van paradox, halt(paradox, paradox) 0 moeten opleveren. Volgens de definitie van halt, betekent dit dat paradox niet eindigt met paradox als invoer.
  • Indien nee, dan zal, volgens de definitie van paradox, halt(paradox, paradox) 1 moeten opleveren. Volgens de definitie van halt, betekent dit dat paradox eindigt met paradox als invoer.
  • Dus kan paradox(paradox) niet eindigen, maar ook niet niet eindigen. Tegenspraak, dus de oorspronkelijke aanname, dat halt bestaat, is onjuist.


Het was voor zijn bewijs, of beter gezegd voor het geven van een definitie van het algoritme, dat Turing het later beroemd geworden idee van de turingmachine bedacht.

BronnenBewerken

  • (en) Elaine Rich, Automata, Computability and Complexity. Theory and Applications., 2008