From: Tim Frink on
Hi,

it is known that the haling problem is not decidable in general.

When I understand it correctly, this is only true if the system where
the computation is performed is considered to be a turing machine (with
an infinite number of states and infinitely large variable values).

But what about real-life systems such as my Intel Linux box where I
run e.g., C programs? These computer systems can be modeled as finite
state machines where I could (at least in theory) test all possible
program executions, i.e., all possible initial states and all possible
inputs (of course in practice one runs into complexity problems). But
this would mean that the halting problem becomes decidable, right?

Regards,
Tim
From: Rick Decker on
On 5/13/10 11:20 AM, Tim Frink wrote:
> Hi,
>
> it is known that the haling problem is not decidable in general.
>
> When I understand it correctly, this is only true if the system where
> the computation is performed is considered to be a turing machine (with
> an infinite number of states and infinitely large variable values).
>
> But what about real-life systems such as my Intel Linux box where I
> run e.g., C programs? These computer systems can be modeled as finite
> state machines where I could (at least in theory) test all possible
> program executions, i.e., all possible initial states and all possible
> inputs (of course in practice one runs into complexity problems). But
> this would mean that the halting problem becomes decidable, right?
>
> Regards,
> Tim

Right. The Halting Problem for finite automata is decidable, though
a real-world computer has so many states that it might take *ahem*
a bit of time to decide.


Regards,

Rick
From: Ben Bacarisse on
Tim Frink <plfriko(a)yahoo.de> writes:

> it is known that the haling problem is not decidable in general.
>
> When I understand it correctly, this is only true if the system where
> the computation is performed is considered to be a turing machine (with
> an infinite number of states and infinitely large variable values).

That's a little confusing. Halting is not decidable for TMs with a
_finite_ number of states and unbounded tape. I think you are including
the state of the tape (or variables) in your "infinite number of
states". That's not exactly wrong, but it can obscure the fact the TM
have a finite number of states in the usual meaning of the term.

> But what about real-life systems such as my Intel Linux box where I
> run e.g., C programs? These computer systems can be modeled as finite
> state machines where I could (at least in theory) test all possible
> program executions, i.e., all possible initial states and all possible
> inputs (of course in practice one runs into complexity problems). But
> this would mean that the halting problem becomes decidable, right?

Right. The formal model for a machine with finite resources is a linear
bounded automaton: essentially a TM with end markers somewhere on the
tape.

--
Ben.
From: Tim Little on
On 2010-05-13, Tim Frink <plfriko(a)yahoo.de> wrote:
> But what about real-life systems such as my Intel Linux box where I
> run e.g., C programs? These computer systems can be modeled as
> finite state machines where I could (at least in theory) test all
> possible program executions, i.e., all possible initial states and
> all possible inputs (of course in practice one runs into complexity
> problems). But this would mean that the halting problem becomes
> decidable, right?

Some restricted subsets of the halting problem are decidable, yes.
The halting problem for finite machines is decidable by machines with
exponentially more resources than the ones being modelled.

Even then, if you bring practical considerations on the one side
(finite real-life system) you should bring practical considerations to
the other side, and the practical halting problem is still in practice
undecidable. Determining when a finite system with even a hundred
bits of state halts may require a machine with more bits than the
known universe has electrons.

A real-life system may have more than 10^15 bits, and consequently
more than 2^(10^15) states.


- Tim
From: Torben �gidius Mogensen on
Tim Little <tim(a)little-possums.net> writes:


> The halting problem for finite machines is decidable by machines with
> exponentially more resources than the ones being modelled.

Actually, twice as much memory is enough.

If a machine with N possible states terminates, it must do so after at
most N steps, otherwise it will have entered a loop. So to decide
termination, you just run a copy of the machine and count the number of
steps. If you terminate before N steps, you have proven termination.
If not, you have proven nontermiantion.

The counter will require the same space as the original machine. So you
need twice the space as the original machine.

Torben