Beslissingsprobleem
Het beslissingsprobleem is een probleem uit de wiskunde en informatica, dat vraagt of het mogelijk is vast te stellen of een bepaald algoritme al dan niet eindigt als het wordt toegepast op een bepaalde invoer. 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.
[bewerk] Bewijs van de onbeslisbaarheid
Het eigenlijke bewijs is natuurlijk complex, maar dit komt grotendeels doordat diverse technische punten, zoals een precieze definitie van 'algoritme', moeten worden behandeld. De kern van het bewijs is ongeveer dit:
De onbeslisbaarheid van het beslissingsprobleem kan bewezen worden met behulp van een bewijs uit het ongerijmde. Dat wil zeggen, neem aan dat we een programma halt(A,x) hebben, dat als resultaat "1" geeft als het algoritme A eindigt indien toegepast op invoer x, en "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) 0 oplevert, en oneindig door blijft gaan als halt(A,A) 1 oplevert.
De vraag is nu, eindigt paradox als het paradox als invoer krijgt?
Indien ja, dan zal dus 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 dus 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 paradox(paradox) kan niet eindigen en niet niet eindigen. Tegenspraak, dus onze oorspronkelijke aanname, dat halt bestaat, is onjuist.
[bewerk] Turingmachine
Het was voor zijn bewijs van de onbeslisbaarheid van het beslissingsprobleem, meer precies voor het geven van een definitie van algoritme, dat Turing het later beroemd geworden idee van de Turingmachine bedacht.
