The halting problem is "undecidable": there's no algorithm which can tell you if an arbitrary program with an arbitrary input will halt or not. IE, if you give me a proposed "halt-detector", I can inspect it and come up with a program and input for which it would give the wrong answer.
Most people think that's a cool mathematical theory but don't know the real world relevance, because computers aren't Turing machines and have finite memory, so all programs are guaranteed to halt. I once saw a keynote speaker say their programming language was stronger than Turing-complete because all programs in it had a timeout, and so they solved the halting problem.
To better understand why the halting problem is so important, it's better to look at what the world would be like if it was solvable.
A recursively enumerable problem is a boolean problem where any true answer can be determined in a finite time. We can come up with an algorithm that, if the answer is "true", halts and returns "true", and if the answer is "false", either returns "false" or runs forever. Here's a recursively enumerable problem:
def sum_of_two_primes(num): for p1 in range(2, num): for p2 in range(2, num): if is_prime(p1) and is_prime(p2) and p1 + p2 == num: return True return False x = 4 while sum_of_two_primes(x): x += 2
This algorithm runs until it finds an even number that's not the sum of two primes, then halts. Goldbach's Conjecture, one of the oldest unsolved problems in all of mathematics, says that there's no such number. This algorithm halts iff Goldbach's conjecture is false.
If the halting problem was solvable, then anyone with a computer could prove Goldbach's conjecture in an afternoon.
This is also why "all computers halt anyway" doesn't really "solve" the halting problem. Let's say the computer has finite memory, so there's a largest integer that can be stored without crashing. Our algorithm then looks like this:
while sum_of_two_primes(x) and x < 999_999_999_999_999: x += 2
Yeah sure this program always halts, but it's no longer checking Goldbach's conjecture. It only checks it up to a certain number! The original algorithm was useful because it could potentially run forever, and capping the runtime takes that property away. It's no longer interesting to us.
A huge number of unsolved math problems are recursively enumerable: odd perfect numbers, the ABC conjecture, the Riemann hypothesis, P vs NP, etc. If there existed a halt detector then we could shove mathematics centuries into the future.1 But the halting problem is provably undecidable, so we live in a very different world.
This is a very rough sketch of how you'd do it:
First, write a bash script
P1 that runs a SAT solver on every possible SAT problem and halts if any of them take exponential time. You don't actually have to run
P1, just call
HALTS(P1, Solver) to see if the solver solves all problems in polynomial time.
P2 enumerate all strings and calls
HALTS(P1, str) on them. If P1 halts (or errors), then
str was not a polynomial-time SAT solver, so move onto the next string. If P1 halts, have P2 halt. Then
HALTS(P2) is true iff there is some SAT solver which solves all SAT problems in polynomial time, ie
HALTS(P2) <=> P = NP.2
(You'd have to figure out how to check if a specific problem took exponential time, but that's a lot easier than proving all of P vs NP!)
You're reviewing PR for a completely unfamiliar codebase. You see that pure function
f has been refactored into
f', and want to check that the two give identical outputs on every input. With a halt detector, that's trivial:
EQL(f, g)that iterates through all possible inputs and checks that
f(x, y, z) == g(x, y, z).
HALTS(EQL, f, f').
Now, in our world, this is impossible. In fact, we can prove there's no program
EQL that can check if two arbitrary functions are identical. Let's say
EQL(f, g) did exist. Then define
HALTS(p, args) like this:
def HALT(p, args): def q: p(args) return iden # some function return EQL(q, iden)
Now HALT returns true iff q returns
iden, which happens iff p halts, meaning we've bootstrapped a halt detector, which we already know is impossible.
Is this again made uninteresting if we assume finite memory.
p always terminates so
q always returns
HALT always returns true, as all programs terminate. But at the same time,
HALTS(EQL, f, g) no longer tells us if
g are equal, only that they are for a subset of inputs. That's just property testing!
The more general version of this is Rice's theorem: determining any non-trivial semantic property of a program is undecidable. So no perfect optimization tools, no perfect bug finders, no perfect backwards-compatibility checkers. Again, this is in the general case, where we have to come up with an algorithm that works for all programs and inputs. In the specific case, say in a specific domain with specific classes of inputs, this can be possible. But it'll require a lot more time and effort than you'd need if you just had a halt-detector.
If the halting problem was decidable, we'd be able to trivially prove a huge class of theorems, solve a huge class of numerical problems, and make our lives as programmers way way easier. But it's undecidable, so we can't. We're stuck programming on earth.
Short notice, I know, but I'll be a guest at Marianne Bellotti's Model Monday tonight! Marianne's a cool friend of mine and is currently working on the Fault modeling language. The talk starts at 7 PM Central time and will probably be about modeling in TLA+, but who knows where it will actually go.
For all this I'm assuming that the halt detector runs in feasible time. It could be a galactic algorithm that provably checks halting but runs in too long a time to be usable. Even in that case, though, the existence of such an algorithm would reveal deep connections between all computable theorems, which would itself be one of the greatest developments in mathematics. ↩
Oops, this is wrong! Or at least oversimplified. Someone pointed out that since P2 uses a halt detector, detecting if it halts is a higher class of unsolvability that regular Turing-complete programs. To my understanding, if the halting problem was decidable, this wouldn't matter, but because it's undecidable, a magic
HALTS oracle couldn't tell if a program that uses
HALTS will halt. ↩