halting.md

Halting Problem in Python

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.