Haltingprobleem

Haltingprobleem is de vraag of een computerprogramma P samen met zijn invoer x ooit zal stoppen (halteren) of onbeperkt zal blijven draaien. Het is een fundamenteel onderwerp binnen de berekenbaarheidstheorie en werd geïntroduceerd door Alan Turing in 1936 als onderdeel van zijn werk over wat computers kunnen doen.

Inhoudelijk stelt men zich voor dat er een algoritme bestaat, Halts(P, x), dat voor alle programma’s P en invoeren x bepaalt of P op x zal halteren. Turing toonde echter aan dat zo’n algorithme niet bestaat. Een gebruikelijke contrapropositie gaat als volgt: veronderstel dat er zo’n Halts bestaat. Definieer vervolgens een programma D dat op invoer P het volgende doet: als Halts(P, P) waar is, dan blijft D voor altijd draaien, anders stopt D. Dan bekijken we D met invoer D. Als Halts(D, D) waar is, dan blijft D draaien, maar dat betekent dat Halts(D, D) onjuist is. Als Halts(D, D) niet waar is, dan stopt D, wat betekent dat Halts(D, D) waar zou moeten zijn. Dit levert een tegenspraak op, zodat Halts niet bestaat. Daardoor is de halting-probleem onbeslisbaar in het algemeen.

Het probleem is wel semi-beslisbaar (recursief oplegbaar): er bestaat een machine die zal stoppen en accepteren wanneer een programma daadwerkelijk halt, maar er bestaat geen machine die voor alle gevallen altijd stopt en beslist. De halting-probleem onderstreept de grenzen van automatische redeneermiddelen en heeft invloed op programmakeuring, formele verificatie en de theoretische begrippen rondom berekenbaarheid.