OK, so Darren will know the answer to this one...

It's common knowledge that if you write an arbitrary program in a 
Turing-complete programming language, it is impossible to determine 
whether the program will ever halt.

This poses several interesting questions. For example:

- What is the "most powerful" language for which you *can* tell is an 
arbitrary program will halt?

- If you have an arbitrary program written in a Turing-complete 
language, which properties *can* you determine, and which ones *can't* 
you determine?

You can't determine whether the program halts after a finite or infinite 
number of steps. But you can trivially determine whether it halts after 
less than 1,000 steps. You can't determine if it's type-safe [only 
whether it is well-typed according to some more restrictive set of 
rules]. Can you determine whether a particular execution path is ever 
taken? Or whether a given variable will ever be read/written? You can't 
determine whether two programs do the same thing, but can you determine 
whether one algorithm is the inverse of another? And so on...

Post a reply to this message

Invisible <voi### [at] devnull> wrote:
> It's common knowledge that if you write an arbitrary program in a 
> Turing-complete programming language, it is impossible to determine 
> whether the program will ever halt.

  That's not stated correctly. It's impossible to create an algorithm which
would tell for all possible programs whether they terminate or not.

  It is, rather obviously, possible to create an algorithm which tells for
*some* programs whether they terminate or not.

  In other words, in the generic case the problem is unsolvable, but in
specific cases it can be solved.

> Can you determine whether a particular execution path is ever 
> taken? Or whether a given variable will ever be read/written?

  That's completely (and rather trivially) equivalent to the halting problem.

-- 
                                                          - Warp

Post a reply to this message

>> It's common knowledge that if you write an arbitrary program in a 
>> Turing-complete programming language, it is impossible to determine 
>> whether the program will ever halt.
> 
>   That's not stated correctly. It's impossible to create an algorithm which
> would tell for all possible programs whether they terminate or not.

Right. You can't solve the problem for all possible programs, only for 
some of them.

So what's the smallest limitation you could impose on the programs to 
make it possible to solve them all?

>> Can you determine whether a particular execution path is ever 
>> taken? Or whether a given variable will ever be read/written?
> 
>   That's completely (and rather trivially) equivalent to the halting problem.

I had a sinking feeling it might be...

Post a reply to this message

Invisible <voi### [at] devnull> wrote:
> So what's the smallest limitation you could impose on the programs to 
> make it possible to solve them all?

  I don't know, but I would bet that if you can't loop nor recurse, that's
a pretty safe bet.

-- 
                                                          - Warp

Post a reply to this message

Invisible wrote:
> - What is the "most powerful" language for which you *can* tell is an 
> arbitrary program will halt?

I forget what it's called, but basically anything with for loops instead of 
while loops does the trick. You have to rule out recursion also. 
Essentially, anything with indefinite loops is out, as far as I understand.

> Can you determine whether a particular execution path is ever 
> taken? 

No. That's called the "printing problem". Put a halt statement on that 
execution path.

> Or whether a given variable will ever be read/written?

Put a halt statement everywhere you read or write that variable.

> You can't 
> determine whether two programs do the same thing, but can you determine 
> whether one algorithm is the inverse of another? 

No, because then you could determine whether a third program does the same 
thing as the first, if they're both inverses of the same program.

See how it goes?

-- 
   Darren New, San Diego CA, USA (PST)
   "We'd like you to back-port all the changes in 2.0
    back to version 1.0."
   "We've done that already. We call it 2.0."

Post a reply to this message

>> - What is the "most powerful" language for which you *can* tell is an 
>> arbitrary program will halt?
> 
> I forget what it's called, but basically anything with for loops instead 
> of while loops does the trick. You have to rule out recursion also. 
> Essentially, anything with indefinite loops is out, as far as I understand.

So no GOTO then?

Basically, anything where flow control is data-dependent?

>> Can you determine whether a particular execution path is ever taken? 
> 
> No. That's called the "printing problem". Put a halt statement on that 
> execution path.

I had a feeling it might be undecidable...

>> Or whether a given variable will ever be read/written?
> 
> Put a halt statement everywhere you read or write that variable.

This too.

>> You can't determine whether two programs do the same thing, but can 
>> you determine whether one algorithm is the inverse of another? 
> 
> No, because then you could determine whether a third program does the 
> same thing as the first, if they're both inverses of the same program.
> 
> See how it goes?

Seems to me that almost anything remotely useful to know is undecidable. 
How helpful...

Post a reply to this message

Invisible wrote:

> - If you have an arbitrary program written in a Turing-complete 
> language, which properties *can* you determine, and which ones *can't* 
> you determine?

This seems relevant:

http://en.wikipedia.org/wiki/Rice%27s_theorem

Now, if only it wasn't completely incomprehensible...

Post a reply to this message

Warp wrote:
> Invisible <voi### [at] devnull> wrote:
>> So what's the smallest limitation you could impose on the programs to 
>> make it possible to solve them all?
> 
>   I don't know, but I would bet that if you can't loop nor recurse, that's
> a pretty safe bet.

You can loop if you can prove a bound on the looping; i.e., a Pascal style 
for-loop, or any loop with a loop variant (in the technical sense of that term).

You can recurse as long as you always have an upper bound on the recursion.

You can also prove it if your language disallows dynamic allocation, 
including not having unboundedly-large integers.  Think of some of the 
original microcomputer BASIC interpreters, with 26 16-bit variables to work 
with. You could still loop forever, but if you run more than 26^2^16 steps, 
you're looping.

-- 
   Darren New, San Diego CA, USA (PST)
   "We'd like you to back-port all the changes in 2.0
    back to version 1.0."
   "We've done that already. We call it 2.0."

Post a reply to this message

Invisible wrote:
>>> - What is the "most powerful" language for which you *can* tell is an 
>>> arbitrary program will halt?
>>
>> I forget what it's called, but basically anything with for loops 
>> instead of while loops does the trick. You have to rule out recursion 
>> also. Essentially, anything with indefinite loops is out, as far as I 
>> understand.
> 
> So no GOTO then?

Forward goto, sure. :-)

> Basically, anything where flow control is data-dependent?

No. Well, yes, in a sense. You're trying to simplify something that's 
already trivially simple, and in so doing just raising questions about what 
you mean by your version of the words.  "Indefinite loops are out." A loop 
you can't look at and tell at compile time the maximum number of times it'll 
loop is an indefinite loop. While loops are not indefinite loops if you can 
tell at compile time how often they'll loop: See Eiffel's loops, for example.

Recursion is OK as long as you have an upper bound on how often you recurse, 
somehow.

> Seems to me that almost anything remotely useful to know is undecidable. 

Only on unbounded computers.

-- 
   Darren New, San Diego CA, USA (PST)
   "We'd like you to back-port all the changes in 2.0
    back to version 1.0."
   "We've done that already. We call it 2.0."

Post a reply to this message

Invisible wrote:
> Now, if only it wasn't completely incomprehensible...

What part do you not understand?

 > for any non-trivial property of partial functions,

A partial function is one that isn't defined for every input value. The way 
you model that in a computation is to have the function not return, i.e., 
get stuck in an infinite loop.

 > there is no general and effective method

"general and effective" means it works for all inputs and always returns. 
(An "effective" function always returns an answer when computed.)

 > Here, a property of partial functions is called trivial if it holds for 
all partial computable functions or for none,

So if some partial functions have that property but not all, it's a 
non-trivial property.  A "trivial" property might be that it executes at 
least one computation, for example.

 > and an effective decision method is called general if it decides 
correctly for every algorithm.

That pretty much sums it up.

Or were you saying the proof is too confusing?


-- 
   Darren New, San Diego CA, USA (PST)
   "We'd like you to back-port all the changes in 2.0
    back to version 1.0."
   "We've done that already. We call it 2.0."

Post a reply to this message