This particular example was derived from an SO post, though I know there's at least one website that precedes this post by a few years. There are other great examples that derive contradictions in other ways, such as this one.
Suppose I could write a python program that told me whether a particular program halted on a given input:
def halts(prog, inp):
"""Returns True if prog halts on inp, otherwise returns False"""
# I have no clue how to implement this. Let's just stub it out for now.
return None
Now I get the idea (perhaps inspired by the voice in my head that usually tells me to eat Doritos) to write the following function:
def mkFunny(prog):
"""Makes a funny function by taking a program and running it on itself."""
if halts(prog,prog): # Line 1
while True: # Line 2
pass # Line 3
else: # Line 4
sys.exit(0) # Line 5
Since mkFunny is a program, and it takes a program as input, I can feed it to itself. This is really not so strange--if you've ever compiled a compiler, you're doing the exact same thing.
haha = mkFunny(mkFunny) # Ha ha so funny.
Now it might occur to us that maybe mkFunny will infinite loop when its fed itself (I dunno, maybe there's a really weird bug). We'd like some assurance that this won't happen, so we try to run our halts function on it:
h = halts(mkFunny, mkFunny) # Oof
What should h be?
If h is True
, then mkFunny halts. That means that mkFunny
made it to line 5
when run on itself (otherwise it would infinite loop). But to make it to line
5, we must have decided on Line 1 that halts(prog,prog)
is False
. What is
prog here? It's mkFunny. That means that halts(mkFunny,mkFunny) is false. Uh
oh.
Well maybe the universe explodes when h is True
, but what if it's False
?
That would mean that mkFunny
doesn't halt, i.e. it infinite loops. The
only way it could do this is by hitting the loop in Lines 2 and 3. But to
get there, we must have decided on Line one that halts(mkFunny,mkFunny)
is
True
. Dang.
So no matter what we do, our function for the Halting problem, halts
, ends up
contradicting itself when run on mkFunny,mkFunny
. This means that our
supposition waaaaaay up at the top of the file must have been wrong, and
so we cannot write such a function.