Code Analysis: Halting Problem

Let’s do a quick digression.  I wanted to talk about mutable state, but first I think we should consider the halting problem.

The halting problem goes something like this:

 Halt( program_source, program_input )  
{
      if ( <The program Halts with that input> ) 
          return true;
      else 
          return false;  
}   
// Now assume a hypothetical program  G 
G( f, v )
{
      if ( f( v, v ) == false ) 
          return false;      
      else
      {
          while( true ) { }; // Loop forever (ie do not halt)
      }  
}
//Now let's assume the following application  
Halt( SourceCode( G( F ), I ) )  
// The SourceCode method gets the source code of its input parameter.  
// The function F is a hypothetical function. I is hypothetical Input.  
// G is the function we defined above. When we provide G with only  
// one input (not two like it wants), then it returns a new G  
// function that has all instances of "f" in G replaced with  
// the "F" in the above line.  
// The behavior our our application is:  
// Halt( SourceCode( G( F ), I ) ) => false  
// When F( I, I ) => true  
// AND  
// Halt( SourceCode( G( F ), I ) ) => true  
// When F( I, I ) => false  
// This is because of the definition of G.  
// Now what happens when we do this:  Halt( SourceCode( G( Halt ) ), SourceCode( G( Halt ) ) )  
// IE what happens when G has Halt as its "f" and then we pass the  
// source code of exactly that input itself.  
// Well, we already know the behavior of  
// Halt( SourceCode( G( F ), I ) ) above, so let's just  
// plug in Halt for F and SourceCode( G( Halt ) ) for I.  
// Halt( SourceCode( G( Halt ) ), SourceCode( G( Halt ) ) ) => false  
// When Halt( SourceCode( G( Halt ) ), SourceCode( G( Halt ) ) ) => true  
// AND  
// Halt( SourceCode( G( Halt ) ), SourceCode( G( Halt ) ) ) => true  
// When Halt( SourceCode( G( Halt ) ), SourceCode( G( Halt ) ) ) => false  
// This is a contradiction, so the method Halt cannot be a valid function F.

Okay, so the point is that you can’t write an algorithm to determine whether or not a program is going to halt even when you know the source code of the program and the input that you are feeding into it.  You have to run the program to be sure.  But consider the following programs:

void First()  
{
      return;  
}
void Second()  
{
      while( true ) { };  
}

The First program obviously always halts and the Second program obviously never halts. But consider the next program:

void Collatz( BigDouble d )  
{
      if ( d == 1 ) return;
      if ( d % 2 == 0 )
          Collatz( d / 2 )
      else
          Collatz( (3 * d) + 1 )  
}

This is called the Collatz conjecture and right now nobody knows whether or not this function halts. So far it halts for every input that we’ve tried, but we don’t know if there’s some input that causes it to loop forever.

The halting problem doesn’t say that you can’t prove that any given program halts or doesn’t halt.  What it says is that you can’t write come up with a generic way of deciding the halting status for all programs.  For the simple First and Second programs above, it’s easy to prove that they halt.  For the Collatz program, it is so hard nobody knows if it ever fails to halt.

Arbitrary code can become arbitrarily difficult to work with.  You never know when you’re about to bump into a situation analogous to the Collatz conjecture that maybe no one on Earth knows how to deal with.

Okay.  Now let’s talk about mutable state.