The Halting Problem and the Church-Turing Thesis


Two weeks ago at PDC Dustin “former blogger” Campbell and I sat down with Keith and Woody to record an episode of Deep Fried Bytes. The show hasn’t been posted yet, but I’m sure it will turn out great.

We talked about all sorts of things, from me shamelessly promoting my book to Silverlight 4.0 to the new IntelliTrace feature of Visual Studio 2010. If you haven’t already heard about it, IntelliTrace is pretty kickass. Essentially it allows you to step backwards in time while debugging. Read this for more info.

Anyways, while we were talking about historical debugging I believe it was Keith who asked if IntelliTrace could detect if a program was in an infinite loop. Being the true Computer Science gangsta that I am, I took the opportunity to name drop BOTH the Halting Problem AND the Church-Turning Thesis. (Hell yeah!)

So this blog post is about explaining both of these somewhat pedantic but fundamentally important concepts.

The Problem

I give you a program and you tell me through any form of analysis if that program will terminate or not. That sounds simple enough, I mean it’s the year 2009 for crying out loud. We might not have flying cars but we do have automated stock trading and WiFi on airplanes.

Spoiler alert: it’s not possible. No matter how hard you try you cannot devise a general algorithm to determine if a program terminates or not. (Obviously you can determine if some programs terminate, but no single algorithm can determine if any program halts or not.)

However in order to prove this with rigor we need a more concrete notion of a program. (For example, are we talking about F# apps written on CLR 4.0 or a Perl script?) Fortunately, this guy already came up with a good theoretical notion of a algorithm and/or program. Enter the Turing machine.

In 1936 a British mathematician named Alan Turing proposed a theoretical model of computation called a Turing machine. (Note that I didn’t say computer because those things hadn’t been invented yet. The first electronic computer came along a decade later in 1946.) Generally speaking, a Turing machine is a finite state machine operating over an infinite tape of input. At each step the machine reads a character from the tape, and then based on its current state and the character read, transitions to a new state, advances the tape one position left or right, and possibly write a character back to the tape.  Eventually the Turing machine will wind up in a special state designated as either an accept state or reject state.

You use a Turing Machine to compute the answer to a Boolean problem (aka a decision problem). For example, given input “RACECAR”, answer whether or not it is a palindrome. The Turing Machine is obviously a far cry from the CLR, but in 1936 Turing machines were the bee’s knees.

Anyways, the specifics of how Turing machines work aren’t that important. Primarily they serve as a way describe the implementation of any algorithms in a mathematical context. We can use the Turning machine as the backdrop for proving whether or not any arbitrary program will terminate. This is known as the Halting Problem.

The Halting Problem

The halting problem is defined as: given a program (Turing machine) and its input (initial tape state), determine if the program will terminate (eventually land on an accept or reject state.)  In other words, if you have a program that takes another program as an input return true if that program halts, otherwise return false.

This seems pretty obvious when you see programs like:

open System

while true do
    Console.WriteLine("Not done yet...")


But what about any program? Turing proved that this is undecidable which means that it is impossible to construct an algorithm that will produce a correct answer every time. A sketch of the proof can be found here, but it goes something like this:

1. Suppose by way of contradiction that you have a function H(p, i) that for a program p and input i returns true if the program halts and false if the program goes into an infinite loop. (That is, H is a solution to the halting problem.) Note that H always terminates.

2. Now consider another function K(p) that is the somewhat of an inverse of H. K takes a Turing machine as input and calls H to check if K’s input halts or not. If K’s input halts, then K goes into an infinite loop. If K’s input does not halt then K returns true. (Note that we are taking K’s argument and converting into a valid input to H since a Turing machine can be encoded as the input into the same Turing machine.)

// H, determines if a program halts
let H (p : TuringMachine, i : TuringMachineInput) =
    if p.TerminatesWithInput(i) then
        true
    else
        false
    
// K, designed to screw with H
let K (p : TuringMachine) =
    // If the input program/input DOES NOT halt...
    if H(p, p.ToString()) = false then
        // return true
        true
    else
        // Otherwise, go into an infinite loop
        while true do 
            ()


Here’s where it gets crazy. What happens if we run program H with the program K and program input K?

match H(K, K.ToString()) with
| true  -> printfn "K with itself as input terminates"
| false -> printfn "K with itself as input does not terminate"

Case 1.) H returns true. Thus, K terminates. However, inside of K it calls H(K, K.ToString()) which if that returned true would have caused an infinite loop – meaning K doesn’t terminate. A contradiction.

Case 2.) H returns false. Thus, K does not terminate. By definition however, K only went into an infinite loop if H(K, K) returned true. (Meaning that by definition of H, K terminates.) Therefore, we arrive at another contradiction.

Since we have found a situation where function H cannot return either true or false, we can conclude that no such program H exists. You can read the original paper On computable numbers, with an application to the Entscheidungs problem here but the main takeaway is that “no Turing machine can determine if an arbitrary Turing machine will halt or not”.

While speaking in terms of Turing machines is great, but how does this relate to real programs? It’s highly unlikely that you are coding in Microsoft Visual Turing Machine .NET™. In order to apply our solution to the Halting Problem more broadly we need a way to compare different forms of computation. (In other words prove that Perl code is equivalent to Visual Basic .NET given enough if-statements and days spent in front of a debugger.)

Church-Turing Thesis

Back in the mid 30’s the Turing machine wasn’t the only game in town. Alonzo Church had also come up with a theoretical notion of computation known as the lambda calculus. (Which serves as the theoretical underpinning of functional programming languages, like F#.)

Alonzo Church, 1903-1995

While Turing Machines were described in terms of states, transitions, and an infinite tape of values, the lambda calculus was really just a way of encoding mathematical functions.

Anyways, the Church-Turing Thesis postulated that Turing machines and the lambda calculus could compute the same things. In other words, any program you can write with a Turing machine could also be written with the lambda calculus. Any notion of computation which can convert any of its programs into a Turing machine is known as being Turing complete. While I can’t cite any proofs off hand, it’s generally assumed that modern languages like F# or <your favorite language here> are Turing complete. (No matter how simple the language, if it supports recursion, while loops, and integers then it’s probably Turing complete.)

While you can try to write some amazing library for detecting infinite loops, I can write the same code using a Turing machine. And, since it has been proving that no Turing machine can solve the Halting Problem, neither can your amazing library.

Summary

This blog post covers a lot of ground, but the bottom line is as follows:

  • Turing machines are a theoretical notion of computation
  • The Halting Problem asks if an arbitrary Turing machine will terminate or not
  • The Halting Problem is undecideable
  • The Church-Turing Thesis states that sufficiently advanced computational systems are all equivalent*
  • Therefore, it is undecideable if an arbitrary program in your favorite language halts or not

*Most people think that Turing machines (and equivalent forms of computation) offer all the computational power possible. Meaning no matter how fancy the computational scheme, you can do the same thing with a Turing machine. However, it is possible that quantum computers offer more computational power than Turing machines and thus could possibly solve the Halting problem.

Hopefully this blog post was general enough to be approach able but detailed enough to keep the pedants at bay. If you are interested in theoretical Computer Science you should buy Programming F#. The book has absolutely nothing to do with any of this stuff, but if there were a program that could solve the Halting Problem I’m sure it would be written in F# 😉

Comments (7)

  1. Well, there’s a joke about it. When faced with a question from his boss about whether he could write a program that will tell if another program finishes or not, this guy promptly says "yes" and gets to work.

    Two minutes later, he is finished. He has written not one, but two programs. One always prints "yes", the other always prints "no". He says: one of them will give you the right answer!

  2. Charles Petzols wrote a great book about Turing last year.

    http://www.charlespetzold.com/AnnotatedTuring/

  3. quantum computers …

    Has anyone modeled the brain as a quantum computer?

    42

    Thanks, really enjoyed your writng style.

  4. John Clements says:

    You write "Anyways, the Church-Turing Thesis postulated that Turing machines and the lambda calculus could compute the same things." Not to put too fine a point on it, but this is incorrect.  The Church-Turing thesis has nothing to do with the equivalence of the lambda calculus and turing machines (they are equivalent), but rather with the notion of whether this is a "good" definition of computability. The fuzziness of this question is the reason that this is a "thesis" and not a "theorem".

    The wikipedia page is correct on this, and provides lots of good detail.

  5. Allen says:

    Great post. Just one little nitpicky point. The ENIAC was the first electronic programmable computer. The first electronic computer was the Atanasoff-Berry Computer (ABC) at Iowa State University in 1942

    http://en.wikipedia.org/wiki/Atanasoff%E2%80%93Berry_Computer

  6. V P says:

    There is absolutely no chance that quantum computers would solve the Halting problem. The same proof that applies to classical computers applies to quantum computers, namely that feeding a (quantum) machine that determines whether a (quantum) machine halts its own description would lead to a contradiction.

    Quantum computers are thought to be more powerful in a computational complexity sense only, not in a computability sense (they are not hyper-computers). What this means is that quantum computers are known to be able to solve certain problems *faster* than a conventional computer, possibly even exponentially faster (though the only *proven* speedup so far is polynomial, see Grover’s Algorithm). There are known quantum algorithms for certain problems that are exponentially faster than the fastest known classical algorithms, and they can make certain problems tractable (solvable within a reasonable amount of time) on a quantum computer that are not known to be tractable on a classical one. The most famous example of this is Shor’s algorithm for factoring numbers into primes. However, unlike Grover’s algorithm, which is proven to be more efficient (though modestly so) than any classical algorithm, it is possible that a classical algorithm will still be found for fast factoring (it is suspected that it won’t.)

    Another thing that often gets written about incorrectly in the popular press is that quantum computers can solve NP-complete problems in polynomial time. This is also not thought to be the case.

  7. ChrSmith says:

    Re: VP

    Thanks for the thoughtful comment!