What is the halting problem, anyway?

#computerscience

You may have asked yourself, are there problems computers can't solve? And, for example, ventured in to deep philosophical questions like "do we all see the same colors?", "Is the sky really blue?", etc. And while GPT-3 might be able to convincingly fool a human it knowns the answers, it really doesn't. Unfortunately, you've run to a class of very ambiguous, ill-defined problem. We don’t know if computers can solve these problems because they’re so ill-defined that we can’t model them mathematically, and so we can’t cleanly define “solved”.

So, let’s look at a different class of problem. If you think about it, we mostly dictate very well defined problems to computers, like "move these bits of data out of JSON and in to a database", "add all these numbers together", and so on. So, this sort of brings forward this question: Are there well defined questions to which computers cannot produce the answer?

Well, we have a class of problem to which we know computers can trivially solve. Let's look at an example of a well defined problem we know with 100% certainty computers can't solve.

The halting problem

Imagine I am your product manager, you work for a company that builds tools that debug programs. I ask you, can you produce me a program that will tell me if a given piece of code will eventually stop executing. We'll also assume for this use case that we're ignoring programs that do I/O. The world of I/O is messy, and we're mostly concerned with computation bugs. We'll call programs that terminate "halting".

Well, you might intuitively start with some unit tests:

def test_halts?
  expect(halts?("1+1")).to be true
  expect(halts?("while true; end")).to be false
end

A program that just adds 1 and 1 together clearly halts executing, almost immediately in fact. A program that loops forever clearly does not. This problem is well defined. Consume a program and check if it stops. This is similar to the JSON parsing case, in that we can express this to a computer in a very unambiguous day. Let’s look at why we can’t solve this.

Now, we could trivially knock out an implementation of halts? that works for the two inputs above. But what about more complicated cases? What about mapping over an array, what about conditionals that contain loops? What about complex nested while loops with twisty recursive logic? You may be thinking “I could probably knock out solutions to this on a case by case basis, and eventually cover everything. Certainly, you could cover some programs by doing this, but dear reader, it turns out that building halts? in the generic case is quite impossible.

You can't solve this problem

It turns out, this problem is quite unsolvable. The formal proof for this is very complicated, but the intuitive proof can be shown in just a few lines of code. Let's imagine we have already written the halts? function. With that consider the following case:

def do_the_opposite
  # here we are passing this function, “do_the_opposite”
  # to halts?, effectively asking it halts? whether or not
  # do_the_opposite ever finishes executing.
  if halts?(“do_the_opposite”)
    while true
    end
  else
    exit
  end  
end

What we're saying is:

if halts? thinks do_the_opposite halts, then do_the_opposite loops forever
if halts? thinks do_the_opposite executes forever then do_the_opposite exits immediately.

This catches the halts? function in a contradiction, it must be wrong. In other words: we can't define a function which accurately tells us if all programs finish executing. This is the definition of a proof by contradiction. The existence of the halts? function implies a logically impossible universe exists.

Why is this interesting? Well, it more broadly tells us that despite all the power of our modern programming languages, powerful type systems, etc, there are still some problems we can't solve. It also tells us that a bunch of problems that we can't solve are related to the code we work on itself. If you're interested in learning more about exactly what the halting problem says, you can find out more by reading about the church-turing thesis