[racket] Checking infinite loops

On Oct 3, 2010, at 7:19 PM, Marco Morazan wrote:

> What year of study are you in?
> 
> I will assume you are a beginner. It can't be done in Racket or any
> other programming language. Most Automata Theory books have a proof of
> that The Halting Problem is unsolvable.

More precisely, you can write a program that will say "yes, there's an infinite loop" whenever there's an infinite loop, but sometimes mistakenly says "yes, there's an infinite loop" when there isn't.  Or you can write a program that will say "no, there's no infinite loop" whenever there isn't one, but sometimes mistakenly says "no, there's no infinite loop" when there is.  Or you can write a program that never makes a mistake on this question, but sometimes goes infinite itself.  But there is NO program, in ANY language, that takes in another program and always tells correctly (in finite time) whether that other program contains an infinite loop.

The proof is simple: suppose there were such a program; call it "inf-loop?".  Then I would write a program "diag" as follows:

(define (diag)
   (if (inf-loop? diag)
       "bye now"
       (diag)))

Now, either "diag" goes infinite or it doesn't.  If it does, (inf-loop? diag) will return true (because that's what inf-loop? does), so the "if" will return "bye now", thus NOT going into an infinite loop.  On the other hand, if "diag" doesn't go infinite, (inf-loop? diag) will return false (because that's its job), so the "if" will call "diag", thus going into an infinite loop.  In short, if "diag" goes infinite, then it doesn't, and if it doesn't, then it does.  Both situations are impossible, so our assumption that "inf-loop?" exists must have been incorrect.  We conclude that "inf-loop?" doesn't exist (or isn't always correct, or sometimes goes infinite itself, or something).


Stephen Bloch
sbloch at adelphi.edu