TASP – Computer Science edition

Another TASP, another proof by contradiction. This one was found on the mathematics & computer blog QED (in Dutch).

Scooping the Loop Snooper – an elementary proof of the undecidability of the halting problem

No program can say what another will do.
I will prove that although you might work till you drop,
you can’t predict whether a program will stop.

Imagine we have a procedure called P
that will snoop in the source code of programs to see
there aren’t infinite loops that go round and around;

You feed in your code, and the input it needs,
and then P takes them both and it studies and reads
and computes whether things will all end as they should

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.

I’d define a procedure–we’ll name the thing Q–
to tell if it looped, by reading the source;

but if no, Q would go right back up to the top,
and start off again, looping endlessly back,
till the universe dies and is frozen and black.

And this program called Q wouldn’t stay on the shelf;
What behavior results when I do this with Q?

yet P is supposed to speak truly of it.
So if Q’s going to quit, then P should say, “Fine!”–
which will make Q go back to its very first line!

Q uses P’s output to make P look stupid.
If P gets things right then it lies in its tooth;
and if it speaks falsely, it’s telling the truth!

I’ve created a paradox, neat as can be–
and simply by using your putative P.
When you assumed P you stepped into a snare;
Your assumptions have led you right into my lair.

So, how to escape from this logical mess?
By reductio, there cannot possibly be
a procedure that acts like the mythical P.

You can never dscover 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!

Geoffrey K. Pullum


Reacties zijn gesloten.