[racket] Checking infinite loops

From: Edmund Dengler (edmundd at esentire.com)
Date: Mon Oct 4 10:56:52 EDT 2010

Yep, but the state space is a wee bit large to record :-).

(All computers are equivalent to finite automata in theory, but definitely
not in practice!)

Ed

On Mon, Oct 04, 2010 at 10:31:36AM -0400, Patrick Li wrote:
>    I know of the halting problem but can't figure out this dilemma.
>    Imagine you load a program into a virtual machine. 
>    This virtual machine has no registers. All operations are done through the
>    memory.
>    That is, the entire state of the virtual machine is captured by whatever
>    is in memory.
>    In that case, because machines are deterministic, the next operation that
>    the machine takes is completely determined by the current state it is in.
>    Therefore, can't the virtual machine detect whether a program will run
>    forever by simply checking whether it's returned to a previously visited
>    state?
>      -Patrick
>    On Mon, Oct 4, 2010 at 10:02 AM, Stephen Bloch <[1]sbloch at adelphi.edu>
>    wrote:
> 
>      On Oct 4, 2010, at 8:37 AM, Eric Tanter <[2]etanter at dcc.uchile.cl>
>      wrote:
> 
>      > Just for the sake of precision:
>      >
>      > On Oct 3, 2010, at 11:48 PM, Stephen Bloch wrote:
>      >> 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 "in ANY language" is too much: This is true of any _Turing
>      complete_ language.
> 
>      Even more precisely, this is true if the language of the program being
>      analyzed is Turing complete.  The language in which you write the
>      alleged analyzer doesn't matter, as long as it can be called from a
>      Turing-complete language.
>      Stephen Bloch
>      [3]sbloch at adelphi.edu
>      _________________________________________________
>       For list-related administrative tasks:
>       [4]http://lists.racket-lang.org/listinfo/users
> 
> References
> 
>    Visible links
>    1. mailto:sbloch at adelphi.edu
>    2. mailto:etanter at dcc.uchile.cl
>    3. mailto:sbloch at adelphi.edu
>    4. http://lists.racket-lang.org/listinfo/users

> _________________________________________________
>   For list-related administrative tasks:
>   http://lists.racket-lang.org/listinfo/users


Posted on the users mailing list.