Bewijs van onberekenbaarheid

Het stopprobleem is het probleem uit de wiskunde en informatica, of het mogelijk is vast te stellen of een algoritme bij een eindige invoer eindigt in een eindig aantal stappen of eindeloos blijft doorgaan. Het is in z’n algemeenheid een bekend voorbeeld van een wiskundig probleem dat onberekenbaar is, en een van de eerste als dusdanig herkende problemen. Dit werd bewezen door Alan Turing in 1936.

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 onberekenbaarheid van het stopprobleem 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.

Het was voor zijn bewijs van de onberekenbaarheid van het stopprobleem, meer precies voor het geven van een definitie van algoritme, dat Turing het later beroemd geworden idee van de Turingmachine bedacht, die de basis zou vormen van onze informatica.

Blijft dat bugs in software alleen kunnen achterhaald worden door het uittesten van de software in kwestie.

Omdat het wiskundig bewijs ook op onze darmen dreigt te werken geven we  hieronder het poëtisch bewijs van het Stopprobleem.

SCOOPING THE LOOP SNOOPER

A proof that the Halting Problem is undecidable

Geoffrey K. Pullum
(School of Philosophy, Psychology and Language Sciences, University of Edinburgh)

No general procedure for bug checks succeeds.
Now, I won’t just assert that, I’ll show where it leads:
I will prove that although you might work till you drop,
you cannot tell if computation will stop.

For imagine we have a procedure called P
that for specified input permits you to see
whether specified source code, with all of its faults,
defines a routine that eventually halts.

You feed in your program, with suitable data,
and P gets to work, and a little while later
(in finite compute time) correctly infers
whether infinite looping behavior occurs.

If there will be no looping, then P prints out ‘Good.’
That means work on this input will halt, as it should.
But if it detects an unstoppable loop,
then P reports ‘Bad!’ — which means you’re in the soup.

Well, the truth is that P cannot possibly be,
because if you wrote it and gave it to me,
I could use it to set up a logical bind
that would shatter your reason and scramble your mind.

Here’s the trick that I’ll use — and it’s simple to do.
I’ll define a procedure, which I will call Q,
that will use P‘s predictions of halting success
to stir up a terrible logical mess.

For a specified program, say A, one supplies,
the first step of this program called Q I devise
is to find out from P what’s the right thing to say
of the looping behavior of A run on A.

If P‘s answer is ‘Bad!’, Q will suddenly stop.
But otherwise, Q will go back to the top,
and start off again, looping endlessly back,
till the universe dies and turns frozen and black.

And this program called Q wouldn’t stay on the shelf;
I would ask it to forecast its run on itself.
When it reads its own source code, just what will it do?
What’s the looping behavior of Q run on Q?

If P warns of infinite loops, Q will quit;
yet P is supposed to speak truly of it!
And if Q‘s going to quit, then P should say ‘Good’
— which makes Q start to loop! (P denied that it would.)

No matter how P might perform, Q will scoop it:
Q uses P‘s output to make P look stupid.
Whatever P says, it cannot predict Q:
P is right when it’s wrong, and is false when it’s true!

I’ve created a paradox, neat as can be —
and simply by using your putative P.
When you posited P you stepped into a snare;
Your assumption has led you right into my lair.

So where can this argument possibly go?
I don’t have to tell you; I’m sure you must know.
By reductio, there cannot possibly be
a procedure that acts like the mythical P.

You can never find general mechanical means
for predicting the acts of computing machines.
It’s something that cannot be done. So we users
must find our own bugs. Our computers are losers!

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s