Halteerbaarheidsprobleem (stopprobleem): wat het is en waarom onbeslisbaar

Halteerbaarheidsprobleem (ook wel het stopprobleem genoemd) is een fundamenteel probleem in de computerwetenschap. Het gaat erom: gegeven een willekeurig programma en een invoer, bestaat er een algoritme dat in alle gevallen beslist of dat programma uiteindelijk stopt (terminates) of voor altijd blijft draaien (infinite loop)?

Intuïtie en eenvoudige voorbeelden

Een paar eenvoudige programma's laten het verschil zien:

 terwijl True: doorgaan;

dit programma zal nooit stoppen (het blijft voor eeuwig draaien), terwijl

 terwijl False: doorgaan;

direct stopt omdat de lus niet wordt betreden.

Het halteerbaarheidsprobleem vraagt of er een algemeen programma bestaat dat, van elk ander programma en zijn invoer, correct kan aangeven of dat andere programma ooit stopt of juist oneindig blijft lopen. Het verrassende en belangrijke antwoord is: nee — zo'n algemeen beslisser bestaat niet. Hieronder volgt een toegankelijke motivatie en het klassieke bewijs van Alan Turing uit 1936.

Opzet van het bewijs (bewijs uit het ongerijmde)

Stel, om tot een contradictie te komen, dat er wél een programma P bestaat dat het probleem kan oplossen. In deze uitleg nemen we P zo dat P(F, I) Waar teruggeeft als programma F met invoer I voor altijd draait, en Vals als het stopt. (Je kunt ook kiezen voor de omgekeerde betekenis; de vorm van het bewijs verandert daar niet door.)

Zo verondersteld programma P:

def P(F, I):     als F(I) voor eeuwig loopt:         teruggeven Waar;     anders:         teruggeven Vals;

Met dit denkbeeldige P bouwen we twee nieuwe programma's Q en R. Q gebruikt P om te bepalen wat er gebeurt als een programma naar een kopie van zichzelf kijkt:

def Q(F):     terugkeer P(F, F);

Q(F) is dus Waar precies als F(F) voor eeuwig draait.

Vervolgens definieer R als volgt: R vraagt Q wat er gebeurt voor een gegeven F; als Q(F) Waar zegt, stopt R meteen; als Q(F) Vals zegt, gaat R in een oneindige lus en draait voor eeuwig.

def R(F):     als Q(F):         terugkeren;               // termineren     anders:         terwijl True: doorgaan;  // loop voor altijd

De contradictie: kijk wat er gebeurt als R zichzelf controleert

Nu vragen we ons af wat er gebeurt als R als invoer aan zichzelf wordt gegeven, dus we bekijken R(R). Er zijn slechts twee mogelijkheden: R(R) stopt of R(R) loopt voor eeuwig. We laten zien dat beide mogelijkheden tot een tegenspraak leiden.

• Stel dat R(R) stopt. Omdat R(R) stopt, is het waar dat R(R) niet voor eeuwig draait. Maar volgens de definitie van R gebeurt R(R) alleen als Q(R) Waar is (want als Q(R) Waar retourneert, dan doet R(R) 'terugkeren' en stopt). Q(R) geeft Waar terug precies wanneer P(R,R) Waar is, dat wil zeggen precies wanneer R(R) voor eeuwig zou draaien. Dus uit Q(R) Waar volgt: R(R) draait voor eeuwig. Dat is in tegenspraak met de aanname dat R(R) stopt.
• Stel dat R(R) voor eeuwig draait. Als R(R) voor eeuwig draait, volgt uit de definitie van Q en P dat Q(R) Vals moet zijn (want Q(R) is Waar alleen als R(R) voor eeuwig draait — let op de consistentie van de oorspronkelijke P-definitie). Maar als Q(R) Vals is, dan leidt de definitie van R ertoe dat R(R) uitvoert: terwijl True: doorgaan; — oftewel R(R) zou voor eeuwig draaien. Dat lijkt op het eerste gezicht geen directe tegenspraak, dus het is belangrijk de logica precies in orde te hebben: met de gekozen betekenissen voor P en Q leidt elke mogelijke waarde van Q(R) tot een uitslag van R(R) die precies de tegenovergestelde eis stelt voor Q(R). In beide gevallen ontstaat een onmogelijkheid omdat R(R) zowel wel als niet voor eeuwig moet draaien volgens de keten van gevolgtrekkingen.

Kort gezegd: ongeacht of R(R) stopt of blijft draaien, leidt dat tot een tegenstrijdigheid met wat P en dus Q zouden zeggen over R(R). Dat betekent dat onze oorspronkelijke aanname — dat er een besluitende functie P bestaat die voor alle programma's en invoeren correct bepaalt of ze stoppen — onmogelijk is. Er bestaat dus geen algemeen programma dat het halteerbaarheidsprobleem oplost.

Wat dit resultaat betekent

• Het halteerbaarheidsprobleem is onbeslisbaar (undecidable): er is geen algoritme dat voor elk mogelijke programma en invoer met zekerheid kan bepalen of dat programma stopt.
• Dit is een van de eerste en belangrijkste voorbeelden van een onoplosbaar probleem in de theoretische informatica. Het toont fundamentele grenzen aan wat computers en algoritmen in het algemeen kunnen beslissen.
• Belangrijk onderscheid: hoewel er geen algemeen beslisser bestaat, kun je wél een programma schrijven dat, gegeven een programma F en invoer I, het blok simuleert en als F(I) stopt het resultaat rapporteert. Dat algoritme zal dus altijd "ja" (en stoppen) wanneer F(I) daadwerkelijk stopt, maar wanneer F(I) niet stopt zal het zelf ook nooit stoppen. Daardoor is de halter-vergelijkbare verzameling semi-beslisbaar (recursively enumerable), maar de complementaire verzameling (de programma's die juist nooit stoppen) is niet semi-beslisbaar.
• Het bewijs gebruikt zelf-referentie en diagonaliseringsideeën. Alan Turing formuleerde dit resultaat in 1936 en legde daarmee de basis voor de moderne theorie van berekenbaarheid en Turingmachines. Zie Alan Turing voor meer historische context.

Gevolgen en verdere opmerkingen

Het onbeslisbaarheidsresultaat voor het halteerbaarheidsprobleem heeft veel gevolgen: vele andere eigenschappen van programma's of functies zijn ook onbeslisbaar (vaak via reducties van het halting-probleem), en het vormt de basis voor resultaten zoals Rice's stelling. In de praktijk betekent dit dat er geen volledig automatische, foutloze algemene analyzer bestaat die voor álle programma's kan bepalen of ze foutvrij zijn, zullen stoppen, of andere niet-triviale gedragskenmerken hebben.

Het haltprobleem is een elegant en diepgaand resultaat: eenvoudig te beschrijven, maar met verstrekkende consequenties over de grenzen van computatie.