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#.)

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# ;)