Thore Husfeldt

The Freeze App Does Not Exist

with 9 comments

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!

Advertisements

Written by thorehusfeldt

June 25, 2012 at 13:48

Posted in Uncategorized

9 Responses

Subscribe to comments with RSS.

  1. […] har også en god og sigende forklaring af standseproblemet på sin egen blog; forklaringen vil appellere til alle, der har en smartphone. Dette indlæg blev udgivet i […]

  2. […] The Bergen people managed to put a full-page article about Turing in the local paper, and I quickly stole their best idea: explain the idea behind the halting problem in terms of phone applications. This led to a quick blog entry: The Freeze App does not Exist. […]

  3. […] The Freeze App Analogy, Simple […]

  4. […] much the same as Turing Machines, since they take in an input, process it and output the result. The freeze app is a good example I came across of what programs cannot compute. Another good example is how we […]

  5. […] The Freeze App Analogy, Simple […]

  6. […] The Freeze App Analogy, Simple […]

  7. […] The Freeze App Analogy, Simple […]

  8. […] The Freeze App Analogy, Simple […]


Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: