The halting problem revisited

[Roedy Green]

The proof that the halting problem is insoluble has discouraged any
sort work on static analysing what computer programs will do.

What if the problem were reformulated like this:

The input to the detector is a Java program, syntactically valid. The
output is :

1. definitely halts
2. definitely does not halt
3. can't tell

Obviously such a program CAN be written. The question is how high
quality is such a detector?

What counts is the percentage of real-life programs that fall in
category 1 or 2.

It does not really matter how it fairs with pathological constructions
favoured of mathematicians.

There is some research in this area, going on in the name of code
optimisation, where you do analysis on a fairly local basis.

You might imagine a compiler warning you of parts of your program
where you have created an endless loop or endless recursion under some
unusual run time conditions. It would not necessarily catch
everything, but it might catch something.

 

[Lawrence D'Oliveiro]

The proof that the halting problem is insoluble has discouraged any
sort work on static analysing what computer programs will do.

If that were true, we wouldn’t have optimizing compilers.

What if the problem were reformulated like this:

The input to the detector is a Java program, syntactically valid. The
output is :

1. definitely halts
2. definitely does not halt
3. can't tell

Obviously such a program CAN be written.

Trivially always answer 3.

The question is how high quality is such a detector?

Can’t tell.

 

[Alex Mentis]

Can’t tell.

hehe

 

[Lew]

The proof that the halting problem is insoluble has discouraged any
sort work on static analysing what computer programs will do.

"I'm ... well ... ummm ..., just not - er - sure how I ... um, ... feel about
Turing," Tom said haltingly.

 

[Joshua Cranmer]

The proof that the halting problem is insoluble has discouraged any
sort work on static analysing what computer programs will do.

No it hasn't. Static analysis is a very hot topic of research in
compilers, despite the fact that is provably impossible. In fact, I
would wager that computer science is the only field where we try to
solve problems we already know to be impossible (well, there's also
government, but that doesn't count).

What if the problem were reformulated like this:

The input to the detector is a Java program, syntactically valid. The
output is :

1. definitely halts
2. definitely does not halt
3. can't tell

Obviously such a program CAN be written. The question is how high
quality is such a detector?

No, the question is how useful is the definite yes/no compared to the
amount of time it takes to run. Also, it turns out that the halting
problem is actually rather boring for static analysis; perhaps the most
important question in general would either be the equivalency question
(are these two expressions equivalent) or pointer aliasing (can these
pointers point to the same value). Or, if you are looking at
machine/assembly code, the most important question is code/data separation.

You might imagine a compiler warning you of parts of your program
where you have created an endless loop or endless recursion under some
unusual run time conditions. It would not necessarily catch
everything, but it might catch something.

Sometimes, though, you want an infinite loop. Think of the event loop in
a GUI toolkit.

 

[Lew]

The input to the detector is a Java program, syntactically valid. The
output is :

1. definitely halts
2. definitely does not halt
3. can't tell

Obviously such a program CAN be written. The question is how high
quality is such a detector?

That is very far from obvious. You assume that the decider will halt.

Now if #3 were "can't tell within period /x/", that'd be different.

No it hasn't. Static analysis is a very hot topic of research in compilers,
despite the fact that is provably impossible. In fact, I would wager that
computer science is the only field where we try to solve problems we already
know to be impossible (well, there's also government, but that doesn't count).

False analysis. The government doesn't try to solve problems, irrespective of
whether they are possible.

Seriously, though, just because a problem isn't ultimately solvable doesn't
mean that research into heuristics or more efficient approaches or bounding
problems or probabilistic approaches won't be fruitful.

For example, suppose you could prove that a decider has a 99.5% probability of
proving haltability or the impossibility thereof within /x/ seconds. You can
prove that the decider will halt by adding the constraint that it must end
after /x/ seconds. You then call the answer "can't tell" with an epsilon
probability of being wrong.

I should think the impossibility of the theoretical would in no wise
discourage the search for the profitable.

 

[Joshua Cranmer]

That is very far from obvious. You assume that the decider will halt.

Program A:
Always returns "can't tell" for any input.

Program B:
Looks for a for/while/do-while loop in the code. If one is present,
output "can't tell". Otherwise, check a method callgraph for the
presence of a cycle. If one is present, output "can't tell", otherwise,
output "definitely does not halt"

Program A clearly satisfies the requirements of the detector, in that it
is never wrong. Obviously, it always terminates, so there is an obvious
program (at least to me) that satisfies the requirements.

Program B is a program which is moderately more useful but still
satisfies the requirements.

So it seems quite obvious that it exists, at least to me.

 

[Lew]

Program A:
Always returns "can't tell" for any input.

Program B:
Looks for a for/while/do-while loop in the code. If one is present, output
"can't tell". Otherwise, check a method callgraph for the presence of a cycle.
If one is present, output "can't tell", otherwise, output "definitely does not
halt"

Program A clearly satisfies the requirements of the detector, in that it is
never wrong. Obviously, it always terminates, so there is an obvious program
(at least to me) that satisfies the requirements.

Program B is a program which is moderately more useful but still satisfies the
requirements.

So it seems quite obvious that it exists, at least to me.

Silly me. I assumed we wanted it to produce a *correct* answer based on an
actual effort to determine the answer.

Now that I look again, I see that attempts at correct results were not
explicitly specified. What was I /thinking/?

Will program B always succeed? Now that I hear your answer it's no longer not
obvious.

 

[Dirk Bruere at NeoPax]

If that were true, we wouldn’t have optimizing compilers.


Trivially always answer 3.

No.
What cannot be done is to create an algorithm that will tell in all
cases whether a program will halt.

It is trivial to detect whether most small programs will do in a finite
time. Otherwise nobody could ever read somebody else's code and spot
halting/loop bugs. The Human brain is also subject to the Turing
limitation (as far as is known)

 

[Joshua Cranmer]

Will program B always succeed? Now that I hear your answer it's no
longer not obvious.

If you make the modification that I had (I mixed up "definitely halts"
with "definitely does not halt"), yes, with the added caveat that if you
cannot construct the callgraph, you print out "can't tell." The reasons
for such might include native methods, effects of reflection, violation
of the closed world assumption, or multithreaded pitfalls (viewing the
callgraph at an actual instruction level, so context switches become
extra edges--I'm viewing this as its correlation to a Turing machine).

 

[Screamin Lord Byron]

The Human brain is also subject to the Turing
limitation (as far as is known)

If what you're saying is true, then how can the human brain prove things
like, say, Fermat's last theorem?

 

[Screamin Lord Byron]

How would you deduce inability to prove Fermat's last theorem from the
Turing limitation?

There can not be an algorithmic proof of Fermat's last theorem because
of the halting problem. And yet, humans can produce the proof.
Therefore, human brain is not subject to Turing limitation.

 

[Screamin Lord Byron]

Why does the halting problem imply anything at all about the existence
or otherwise of a proof for Fermat's last theorem?
Can you give a proof, or point to one I can read?

Yes. Sir Roger Penrose's book "Emperor's New Mind". I have a copy which
is translated to my language, so I can't give you exact page numbers
where he talks about that specifically (should be within first 100
pages), but the book is absolutely worth a read in its entirety.

 

[Screamin Lord Byron]

Yes. Sir Roger Penrose's book "Emperor's New Mind". I have a copy which
is translated to my language, so I can't give you exact page numbers
where he talks about that specifically (should be within first 100
pages), but the book is absolutely worth a read in its entirety.

Just to be clear, in the time of writing of that book Fermat's last
theorem wasn't yet proven nor Penrose provides the proof. That was done
later of course.
http://en.wikipedia.org/wiki/Wiles'_proof_of_Fermat's_Last_Theorem

In his book, Penrose argues that such problems cannot be solved
algorithmically.

 

[Screamin Lord Byron]

I don't have a copy, so that is not currently one I can read. Perhaps
you can restate the proof in your own words, or give an on-line reference?

In fact I have. I didn't have much hope to find it online, but I got
lucky I guess.

http://bit.ly/gCPoot

Long link:
<http://books.google.hr/books?id=oI0...&resnum=1&ved=0CBgQ6AEwAA#v=onepage&q&f=false>

 

[Lew]

It is trivial to detect whether most small programs will do in a finite time.
Otherwise nobody could ever read somebody else's code and spot halting/loop
bugs. The Human brain is also subject to the Turing limitation (as far as is
known)

Fortunately the human mind is not limited to the limitations of the human brain.

 

[John B. Matthews]

I don't have a copy, so that is not currently one I can read. Perhaps
you can restate the proof in your own words, or give an on-line
reference?

Several related arguments, including Penrose's, are summarized here:

<http://en.wikipedia.org/wiki/Mechanism_(philosophy)#G.C3.B6delian_arguments>

 

[javax.swing.JSnarker]

Fortunately the human mind is not limited to the limitations of the
human brain.

Non sequitur. In fact, self-contradicting. The human mind is implemented
on the human brain*. Your statement is analogous to saying that some
computer program you ran on your dual-core x86-64 machine was not
limited to the limitations of your dual-core x86-64 machine, or that if
you put a fancy enough GPS unit in your Chevy Tahoe you could drive it
from New York to Sydney, Australia in under two hours, regardless of the
Tahoe's engine speed, and without having to drive it onto a plane or a ship.

Obvious nonsense.

* And to forestall the inevitable objections from dualists, every single
faculty of the human mind has been found to be able to be specifically
impaired by particular brain injuries, including memory, face
recognition, conscious awareness, language (and particular subskills of
language), and more. If the brain was just the antenna by which some
external mind-stuff connected to pilot the body, it seems unlikely that
this would be the case. Indeed, other than specific low-level sensory or
motor impairments, and perhaps epilepsy, any sensible dualist theory
would predict a near-total absence of mental disorders resulting from
identifiable physical trauma or chemical states of the brain, or
correctable by same. But instead it's possible to get whacked upside the
head and become unable to *think certain thoughts* anymore.

Read "The Man Who Mistook His Wife For A Hat" and try to reconcile *any*
of it with *any* flavor of dualism. On the other hand, the broad
spectrum of often very quirky bug reports in there are pretty much
exactly what you'd expect if the mind was complex software that ran as
specialized daemons distributed over a complex computer-network inside
the skull, and then various parts of that network became "host unreachable".

I'll add that they've mostly already reverse engineered auditory
perception, have made big strides in reverse engineering visual
perception, and will probably have decompiled and begun to analyze the
very algorithms underpinning conscious awareness itself in another
decade or three. MP3 encoding is a lossy compression whose lossiness was
optimized partly based on understanding the algorithms used in the human
brain to process incoming sound data. With every passing year, that much
less of what goes on in there remains unexplained in terms of simple
mechanics, electrochemistry, and various algorithms, and there's no
reason to believe that process will stop short of explaining *all* of it
in such terms.

 

[Mike Schilling]

Thanks. I happen to agree with the view that human reasoning is not
always consistent. It has evolved to produce decisions as needed, even
if there is limited data, which puts completeness ahead of consistency.

In particular, I think, the human mind sees patterns everywhere, and is
ready to reason from them without knowing for sure whether they're real or
spurious. Ramanujan was well-known for deriving amazing results from this
kind of reasoning by analogy which other, sometimes lesser, mathematicians
would later prove rigorously.

 

[Lawrence D'Oliveiro]

In particular, I think, the human mind sees patterns everywhere, and is
ready to reason from them without knowing for sure whether they're real or
spurious.

And the part of the mind that believes in these patterns is different from
the part that finds out whether they’re spurious.

And so you have the odd situation of scientists who continue to believe in
religion, for example. Or Johnny Carson’s famed debunking of Uri Geller, the
effect of which on his popularity was ... zero.