Re: A modern view of the halting problem

Alex McDonald wrote:
Rod Pemberton wrote:
<randyhyde@xxxxxxxxxxxxx> wrote in message
news:1161530912.166161.254830@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

More importantly, you cannot write a program that
runs on a finite-resource machine (bounded memory, and program steps)
that determines if another program always halts and produces a correct

Before I ask the upcoming question, I'll simply state that I am not from a
CS background, and am _totally_ ignorant of the formal proofs of Church,
Turing, etc...

You've stated that it is impossible for one program to determine if another
program will halt. What I'd like to know is, is it possible to design a
language so that any program written in it will always halt properly,
whether or not that program is being reviewed by another program.
Basically, I'm asking why would one write a second program to check the
first program, if you know the first is correctly "halt-able" due to the
design of the language? I.e., is there some other proof, thereom, etc. that
says one can't design a provenly halt-able language...? At an assembly or C
level, it seems to me that you could halt every non-branching instruction,
and with correct design should be able to halt very branching instruction,
loop construct, or flow control code. I understand that I am missing
something to this discussion...

The halting problem is not about stopping at specific instructions;
it's about the impossibility of writing a program that can inspect
other programs and, in all cases, decide that they will halt or run
forever when executed.

I too am ignorant in this matter. But... I do recall a single example
that
seemed to make sense to me :-)

Lets take, the 4 color problem. Currently to my knowledge, it is
unsolved.

So lets ask a computer to find the first graph that contradicts the 4
color problem.

Now if the 4 color problem was solved, this would be easy to see if
the computer would halt or not.

Any algorithm that solved the halting problem would surely be
magnificent,
because it would obviously also solve any current math problem that
can be somehow expressed in a computer. (Including Riemann Hypothesis
and really, anything)

Or here is another actually, using Riemann Hypothesis instead.

Lets say algorithm A searches for a contradiction in the Riemann
Hypothesis.
(IIRC, there is a computer algorithm that really does that). Does A
halt?

Meh; this post doesn't "disprove" the halting problem nor does this
post "prove" it.
But it does at least show that the halting problem really is pretty
deep.

--Dragontamer

.

Relevant Pages

• Re: The Halting Problem is merely an erroneously formed question
... Since you are asserting that this machine must eventually halt, you are therefore asserting that this machine has entered an invalid run state, and you are breaking the implicit model of computation. ... This may be a mental fiction, but you can make these assumptions fully explicit in descriptions and talk about real world machines in the same manner. ... the halting problem itself is not the most useful problem to solve. ... word games that are harder to play in mathematical notation. ...
(comp.theory)
• Re: simple and beauty strategy
... the halting problem is a decision problem ... Alan Turing proved in 1936 that a general algorithm to solve the ... the program will eventually halt when run with that input. ... undecidability of a problem in the lambda calculus had already been ...
(rec.gambling.lottery)
• Re: Halting Problem Final Conclusion
... > was to detect programs that failed to halt, ... The primary benefit of a universal Halting Problem ... about programs that fail to halt. ... if this program would halt" analyzer may be as ...
(comp.theory)
• Re: Halting Problem Final Conclusion
... > was to detect programs that failed to halt, ... The primary benefit of a universal Halting Problem ... about programs that fail to halt. ... if this program would halt" analyzer may be as ...
(sci.logic)
• Re: The formal and informal proofs
... I am paid to formalize all day. ... > HALT(x,y) = List the TMs that halt. ... > possible, you have a formalization of the Halting Problem, the Every ...
(sci.logic)