It’s Time for a New Old Language
A rhymed proof that the Halting Problem is undecidable
No procedure exists to judge programs that halt.
Don’t believe me, just see, there’s a proof after all!
I will show, in end, you might work till you drop,
there’s no way you can tell if computation will stop.
Let me give you a procedure, P is its name,
that, for any input you can think in your brain,
it can surely tell, with all of its faults,
if the input does truly, eventually halt.
See, P takes in your program, with suitable data,
it starts, and it works, and a little while later,
P eventually stops and correctly infers
whether or not your input endlessly recurs.
If there’s no endless looping, then P prints out ‘Good.’,
which means work on this input halts as it should.
But if P smells recursion and detects unending loops,
then ‘Bad!’ it would utter, to report the scoop!
Alas, P is really too good to be true,
you see, if I had P and gave it to you,
you could use it to set up a logical bind
that would shatter reason and scramble the mind.
Here’s the trick you can use—and it’s simple to do.
You define a procedure, let’s say you call it Q,
that takes P and its predictions of halting success
to stir up a much terrible logical mess.
For a given program A, one can supply,
the very first step that Q does emprise
is to find out from P what’s the right thing to say
of the looping behaviour of A run on A.
If P answers ‘Bad!’, Q will suddenly stop.
Otherwise, it will go and begin from the top,
so that Q ends in loops, going just forth and back,
till the universe dies, turning frozen, and black.
Now, this program called Q won’t just stay on the shelf;
You would ask me to forecast its run on itself!
“When it reads its own code, can you guess what will it do?
What’s the looping behaviour of Q run on Q?”
If P smells an infinite loop, Q will just quit;
yet P is supposed to speak truly of it.
And if Q’s going to quit, then P should say ‘Good.’,
but that’s exactly what makes Q end up in a loop!
So, Q teases P, and will always scoop it:
Q uses P’s output to make P look stupid.
Whatever P says, it can’t predict Q:
P is right when it’s wrong, how can it speak truth?
You created a paradox, as neat as can be,
and nimbly by using my putative P.
When I made up P, I just stepped into a snare;
my assumptions were wrong and P’s beyond repair.
So, where can this argument possibly go?
I don’t have to tell you; you already know:
we have an absurdum that says there can’t be
a procedure that acts like the mythical P.
— modified version of Pullum, Geoffrey K. “Scooping the loop snooper.” Mathematics Magazine 73.4 (2000): 319-320.