Re: A modern view of the halting problem



This is so wrong, I don't even know where to begin...


Charles A. Crayne wrote:
In 1936, Alan Turing presented a proof that it is possible to write a
program such that it is not possible by analysis alone (i.e. without
actually running the program) to determine if the program will eventually
halt. At the time, this proof created quite a stir among his colleagues,
however after 70 years of rapid development in computer science, it is now
clear that his proof, albeit valid, is more of a parlor trick, than any
real insight into computing theory, and, although it does apply to
computers, it has no special connection with them.


Well, Turing did basically introduce turning machines as a formal way
to describe the notion of an algorithm, and then proved that the
halting problem cannot be solved. This was not very interesting. What
*was* interesting was that Turing was able to prove that Hilbert's
Entscheidungsproblem could be recast as the halting problem, thus
answering a major outstanding question in (first order) predicate
calculus. Note that Church actually proved the same thing slightly
earlier than Turing, but Turing's method is considerably more
interesting.

And of course the results have no special relationship to computers.
Computers are dull little engineering artifacts, of darn little
interest to propositions of logic or algorithms. Although they are, on
occasion, quite handy places to run those algorithms.

Also, the "without running the program" comment is true, but only
trivially. If the recast problem is to determine if an program
actually halts, running the program until it stops is obviously
impossible if the program can run for an unbounded amount of time (and
if it can't the questing is silly in the first place). You might as
well complain that someone asked "how fast can a man run," and then had
the audacity to exclude the use of an automobile.


To demonstrate that
these two points are true, it is necessary only to restate Turing's proof
without reference to computers.

Let us postulate that the "The Great Melvini" claims to be able to predict
which of two checkers (one red, one black) a volunteer will choose in any
given trial. To lend credibility to this test, "The Amazing Randi"
volunteers to be the one who chooses the checker.

The fairness of such a test clearly depends upon the time sequence in which
the predictions and the choices are made and revealed. If, for example, the
rules allow Randi to know Melvini's prediction before making his own
choice, then Randi is in complete control of the results, and can make
Melvini look either very good, or very bad, as Randi may wish. As this
situation should be obvious to the casual observer, it is unlikely to draw
much of a crowd. And yet, this unlikely set of rules is exactly what
Turing choose for his famous proof.

In other words, by proposing a program which consults an oracle, and then
does the opposite of whatever the oracle predicts, Turing has not so much
proven anything about computers, as he has drawn on the well known fact
that predicting the future is fraught with difficulties.

However, since Turing did choose to focus on computers, let me offer a
couple of observations on the consequences of his proof:

To begin with, since the generalized proof applies to both humans and
computers, any proof which is derived from his proof also applies to both
humans and computers. There is no "wiggle room" for a human to "step
outside the box" and decide what a computer can not decide. So long as the
argument derives from Turing's proof, then anything which is undecidable
by a computer, is also undecidable by a human.

Next, the proof is not limited to halting, nor even to two alternatives.
The essence of the proof is the attempt to predict a future event which is
under some other entity's control. In the real world, this situation
rarely arises, if for no better reason that we know better than to try. In
the real world, one does not write programs which use infinite loops as a
function's return code. Nor, except as a joke, programs which accept a
user's input command, and then do something entirely different.


This analogy is just silly.

Turing required no Oracle. He used the common mathematical approach of
reductio ad absurdum. He assumed that the problem *could* be solved,
and then demonstrated that such an assumption leads to an absurd
result. IOW, if you actually had a program that could solve the
halting problem, you can trivially construct a program about which you
*cannot* decide the halting problem, which contradicts the notion that
you have a program that *can* solve the halting problem in the first
place. Hence, by the law of the excluded middle, such a program cannot
exist.

Compare the similar approach we all used in high school to prove the
existence of irrational numbers. Assume that sqrt(2) is rational, and
thus may be represented as a fraction of two natural numbers p/q where
p and q share no common factors (basically the definition of a rational
number). The trivial "proof" shows that both p and q have to then
be even numbers, hence both must have a factor of two. Which, of
course, is absurd since they share no common factors, and hence,
sqrt(2) cannot be rational.

In fact, the halting problem is something of a triviality (just like
the fact that the square root of two is irrational is rather trivial).
It was used only to prove that a large class of problems do not, in
fact, have solutions. That was the interesting result, namely the
answer to the Entscheidungsproblem (or that irrational numbers exist in
the other example).

Frankly one almost never actually cares. What is important is that we
acknowledge that many problems cannot be solved. For example, a
compiler trying to generally decide if two pieces of code are
equivalent, or if a point in a program will ever actually be reached.
By knowing that certain problems don't have a solution, I can avoid
wasting my time trying to solve them. You won't catch me trying to
square a circle with a compass and straightedge either.


And finally, in the real world, one does not demand 100% precision. The
fatal flaw in Turing's proof is that it is qualitative, and not
quantitative. If one wishes to write a program which analyzes programs
submitted by students, and reject those which are likely to loop forever,
one doesn't care that it may not be possible to catch them all, but rather
what percentage of such programs can be caught. And for such questions,
Turing's proof has no answer.


This at least is true. Unfortunately it's completely trivial. The
notion that one can often usefully use an approximation, or a limited
solution, when an exact result is too expensive or impossible to
obtain, is trivially obvious.

.



Relevant Pages

  • Re: Alan Turings Halting Problem is Incorrect (FINAL PART)
    ... the Halting Problem applies to "real" computers as much as Turing ... on what they can compute is obviously inherited by real machines. ...
    (sci.logic)
  • Re: What is the Result from Invoking this Halt Function?
    ... > machines are weaker than current computers. ... > 'halting problem' has not yet been analysed to determine whether it ... number of quantifiers in a certain logical formula that Turing ...
    (sci.logic)
  • Re: What is the Result from Invoking this Halt Function?
    ... > machines are weaker than current computers. ... > 'halting problem' has not yet been analysed to determine whether it ... number of quantifiers in a certain logical formula that Turing ...
    (comp.theory)
  • Re: misconceptions on computer science
    ... The essential thing about the Turing test ... Turing held that computers would in time be programmed to acquire ... In Alan Turing: the Enigma, I discussed Turing's paper in the light ...
    (comp.object)
  • Re: Alan Turings Halting Problem is Incorrect (FINAL PART)
    ... unsolvability of the Halting Problem for a real programming language. ... The Halting Problem isn't really about computers, at least not directly, ... > computers* that does not contrive a logic paradox to make the proof? ... A paradox is an argument in which a contradiction follows from ...
    (sci.logic)

Loading