Turing’s proof of the undecidability of the Halting problem explained in terms of phone applications (“apps”), 100 years after his birthday.

Some apps can freeze your phone

There are apps that will freeze your phone, either out of malice or negligence from the app developer. For example, the app might try to perform some undefined mathematical operation, such as dividing 5 by 0. Your maths teacher will have told you that “5/0” does not make sense, and when a modern computer encounters this expression it will indeed crash; in the worst case taking the rest of the operating system with it. Your phone will lock down or “freeze”, and there is nothing else you can do about it, short of restarting the device. After that you are well advised to remove the app.

Why does it have to come so far? Why do such bad apps exist in the first place? Can’t one test for such behaviour beforehand?

The Freeze app

Imagine a really clever software company did just that. Imagine there was an app, Freeze, that would test a suspicious app and determine if it will freeze your phone or not.

Freeze might work by performing experiments of the suspicious app in a simulated environment without actually freezing your phone, or it might deduce the input app’s behaviour from inspecting its source code, — it’s not important for us just how Freeze accomplishes what it promises.

Freeze is really simple to use. First, you select the suspicious app from a list of installed apps on your phone:

Then Freeze does its analysis, which might take a few minutes, and presents you with the result. Nifty.

The Paradox app

As soon as Freeze hits the store, I will build a new app, which I will call Paradox. It will take me all of 3 minutes to develop, because my own programming effort will be tiny. Paradox mainly works by calling Freeze in a nefarious fashion.

Here is the source code for Paradox (in English, not in a real programming language):

1. Run Freeze and ask it to inspect Paradox.
2. If Freeze returned “OK” then freeze the phone, for example by computing 5/0.
3. If Freeze returned “Not OK” then announce “Freeze detected that Paradox freezes” and terminate gracefully.

In a real programming language, the code would look more like this:

set Result to 
    tell application "Freeze" to
        check application "Paradox"
    end tell
if Result is "OK" then
    display 5/0
else display "Freeze detected that Paradox freezes"
end if

That’s it. I’ll publish my Paradox app and invite you to download it to your phone. Go ahead, nothing bad can happen—after all, you have the Freeze app, don’t you?

Why the Freeze app can’t exist

Is the Paradox app malicious?

There are two possibilities. Either Paradox is a malicious app that freezes the phone, or it is not. We will show that both of these cases is a logical impossibility.

Assume Paradox does freeze the phone. Freeze will have detected this, thus, in Paradox’s code, computation proceeds from line 1 to 3 and Paradox will return “Freeze detected that Paradox freezes” and terminate gracefully. The phone did not in fact freeze, contradicting our assumption. Thus, this case is absurd and we can reject it.

So assume that Paradox does not freeze the phone. Freeze will determine this, so Paradox’s computation will proceed to line 2 and freeze the phone. This, again, contradicts our assumption.

Since both of these cases lead to contradictions, we must go back in our argument we conclude that our initial assumption was wrong. (This is called a proof of contradiction.) Thus, an app like Freeze cannot exist.

“There’s no app for that.”

This is Turing’s main result, from his famous 1936 paper. Instead of a phone he used a fictional computational device that we today call a Turing machine. But phones are just special cases of Turing machines.

Acknowledgements

I think this is a great way of explaining Turing’s proof to a general audience. It’s not mine. I saw it two days ago in a Norwegian newspaper, in a splendid article about Alan Turing for his centenary written by Pål Grønås Drange and Jan Arne Telle from the CS department of Bergen University. This is a great piece of popular science writing; kudos for including a proof of the Halting problem!

• Pål Grønås Drange and Jan Arne Telle, Er du venn med en robot?, Morgenbladet 21 June 2012.
• Halting problem, Wikipedia.