## Wednesday, February 20, 2013

### Halting problem

The question posed by the halting problem is:  Given an arbitrary program from a turing complete system and an input for that program, determine if the program yields output or if it processes the input forever, never yielding output.

Named the halting problem because we are trying to decide if the program halts (yields output).

The halting problem is not decidable.  That is to say that using turing complete systems, it is not possible to create a program that is able to examine arbitrary programs and decide if they halt or not for a given input.  Unfortunately, the proof is a proof by contradiction, so there's not really a lot of insight as to why the halting problem cannot be answered.  But it is a useful exercise in understanding the types of thinking that come up when analyzing a rule system.  You may think a set of rules sound just fine, but someone clever may be able to subvert your entire system.

The first thing to consider is a program that doesn't halt.  In lambda calculus this would look something like this:

( λ x . x x ) ( λ x . x x )

Okay, so the second ( λ x . x x ) is fed into the first ( λ x . x x ).  The second ( λ x . x x ) then becomes "x".  So every instance of x needs to be replaced by ( λ x . x x ).  And the result is:

( λ x . x x ) ( λ x . x x )

The exact same thing that we started with.  And then we do the same thing again and again.  This process continues forever.  This is a program that doesn't halt.

Next, let's define what the interface for a halting problem function would look like.

halt?( input, program ) -> true if the program halts with input, false otherwise

It's a function that takes a program and the target input as parameters and then it returns true or false depending on whether or not the program halts given that input.

A naive implementation of this function might look something like:

function halt?( input, program )
if program( input ) then
return true
else
return false
end

This will work perfectly if the program does in fact halt on the input.  But if the program does not halt on the input, then our halt? function will also never halt.  So we'll never get to return false.  Whatever, the halt? function does, it can't actually do it by running the program and seeing what the result it.  It needs to do some sort of more sophisticated analysis.  However, this more sophisticated analysis turns out to be impossible (for arbitrary programs at least).  Let's consider the following function:

function G( input )
if F( input, input ) == false then
return false
else
( λ x . x x ) ( λ x . x x ) // ie loop forever
end

The function F is to be considered as potentially any function that takes two inputs and returns true or false.

Now let's see what kind of behavior the G function has when we pass it itself.

G( G )

Well, it really depends on what the behavior of F is right?  Fortunately, F either returns true or it returns false, so we can define the G function's behavior piecewise.

G( G ) = false, when F( G, G ) = false
G( G ) = , when F( G, G ) = true

Hmm … what's the deal with ""?  That symbol actually has a lot of different meanings.  Like most things in mathematics, its horribly overloaded and means a lot of different things depending on the context.  It means things like 'does not terminate', undefined, falsity (a concept I'm not sure I fully grasp), etc.  This symbol is useful here because G might not return any value.  And in that case instead of saying, "G doesn't return any value because it fails to terminate," we can instead say .  It's like a shortcut.

Let's redefine the halt? function using the new symbol and the piecewise style.

halt?( input, program ) = false, when program( input ) =
halt?( input, program ) = true, otherwise

Okay, this seems simple enough, but what's the connection with proving that the halting problem can't be solved?  Well earlier I said that the F function can be any function that takes two parameters and returns true or false.  Well, the halt? function is a function that takes two parameters and returns true or false.  Let's see what happens when the F function is actually our halt? function.  First notice that G is taking itself as input.  So let's describe the behavior that we expect from the halt? function if we were using it to analyze whether or not the G function halts when given itself as an input.

halt?( G, G ) = true, when G( G ) = false
halt?( G, G ) = false, when G( G ) =

Okay, that's basically the piecewise description of halt? above, but with the parameters input and program both replaced by G.  Additionally, we can replace the "true, otherwise" portion with G( G ) = false because we know that's the only time that the function G halts with an input of itself.  Now let's combine the behavior we expect from the halt? function with the behavior that we expect from the G function.

halt?( G, G ) = true, when G( G ) = false, when F( G, G ) = false
halt?( G, G ) = false, when G( G ) = , when F( G, G ) = true

Now because F is actually halt?, let's replace the occurrences of F with halt?.

halt?( G, G ) = true, when G( G ) = false, when halt?( G, G ) = false
halt?( G, G ) = false, when G( G ) = , when halt?( G, G ) = true

And now we are left with the contradiction.  halt?( G, G ) is equal to true when G( G ) is equal to false, and that only happens when halt?( G, G ) is equal to false.  And vice versa, halt?( G, G ) is equal to false when G( G ) does not terminate, and that only happens when halt?( G, G ) is equal to true.

That might be a bit confusing, so let's reorganize the piecewise description to highlight the contradiction.

G( G ) = false, when halt?( G, G ) = false

Meaning that G( G ) is equal to false when the halt? function returns false which in turn means that G( G ) does halt when halt? says that G( G ) does not halt.

G( G ) , when halt?( G, G ) = true

Meaning that G( G ) does not halt when the halt? function says that it should halt.

So in other words.  The function G with input G halts when the halting function says that it doesn't halt and it doesn't halt when the halt? function says that it does halt.  Or …

halt?( G, G ) = false, when halt?( G, G ) = true
halt?( G, G ) = true, when halt?( G, G ) = false

Proof by contradiction works by assuming a certain thing exists.  Then it shows that as a result of that thing existing, something else that's impossible must also exist.  Finally, we conclude that the thing cannot exist because if it does then something that is definitely impossible must then also exist.

In this instance we assumed that there existed a function halt? that returned true when a program halted with a given input and false when a program does not halt with a given input.  From there we create a very real function G and explore its behavior when it is passed itself as a parameter.  Finally, we place the halt? function inside of the G function such that we receive a result that contradicts the very nature of the halt? function.  It's pretty obvious that halt?( G, G ) is equal to true only when it is also equal to false and vice versa is impossible.

Unfortunately, this doesn't really explain why the halting problem can't be solved.  It just shows that having a function that solves the halting problem is nonsensical.

Even though this seems like very esoteric material, it actually has important implications for everyone.  Just because you make a rule or a request that sounds like it makes sense doesn't mean that it actually does make sense.  After all, the halting problem sounds like it should be perfectly reasonable to exist.  And it's not quite obvious why it can't exist.  What is obvious is that if it did exist, then it wouldn't exist (it fails to work for G( G )).

Additionally, notice what happened when we created what we thought was a reasonable request.  Some very clever person showed up and created a very real function G.  G was able to make our reasonable request say 'yes' when it should have said 'no' and 'no' when it should have said 'yes'.

If we set up rules which seem reasonable, but in reality are nonsensical, we run the risk of encountering clever people who can subvert our rules and manipulate them to enforce the exact opposite of what we actually wanted to happen.