Jump to content
  • Advertisement
Sign in to follow this  
King of Men

Question about the Halting Problem

This topic is 4048 days old which is more than the 365 day threshold we allow for new replies. Please post a new topic.

If you intended to correct an error in the post then please contact us.

Recommended Posts

I'm a bit fuzzy on formal computer science. I seem to recall that the Halting Problem shows that it is not possible to compute using a Turing machine whether a general, non-trivial program will stop execution. If I have a particular program, though, even a non-trivial one, can I say anything about its halting properties for arbitrary input?

Share this post


Link to post
Share on other sites
Advertisement
Yes, you can prove termination of non-trivial programs; Halting just says you cannot do this for all possible programs. In terms of proving termination for practical programs you would want to write though, it's feasible to do but requires more effort for harder algorithms.

For example, many functions can be defined using primitive recursion which is very easy to check: http://en.wikipedia.org/wiki/Primitive_recursive_function

Primitive recursion really says "when defining f, you can only call f recursively if the arguments you call f with are simpler each time". This ensures that eventually some kind of base case is met and the function terminations. Examples of these kinds of function are list operations like reverse, insert, remove, filter, append, map, drop etc. These terminate on an empty list and the recursive call makes the list smaller each time.

For more general recursion, you can prove termination by providing a "termination measure". This is some value of some kind that you prove gets smaller on each recursive call. An example of this is a binary search, where the reducing termination measure is the distance between the two search markers. Termination proofs usually involving thinking about how you yourself know that the program terminates and then justifying this logically.

There are plenty of systems that support automated and assisted termination proofs. Have a browse on google for decades worth of work into this problem:
http://www.google.com/search?num=100&hl=en&q=termination+proof+automatic&btnG=Search&meta=

Share this post


Link to post
Share on other sites
regurgitates what the above poster said in first sentence. ha ha ha taking a course in computation and intractability huh? man, now that was a fun class.

Share this post


Link to post
Share on other sites
Now is it possible to say

a) it does halt.
b) it doesn't halt.
c) I can't tell if it will or not.
d) I can't tell if it will or not and here's the reason.

it would very handy for a post compiler check.

Predicate maths helped me tidy up my code immensely. I found it really useful, finally I could say WHY I coded things in particular ways I had discovered by trial and error.

Share this post


Link to post
Share on other sites
Quote:
Original post by ROBERTREAD1
Now is it possible to say

a) it does halt.
b) it doesn't halt.
c) I can't tell if it will or not.
d) I can't tell if it will or not and here's the reason.

it would very handy for a post compiler check.

Predicate maths helped me tidy up my code immensely. I found it really useful, finally I could say WHY I coded things in particular ways I had discovered by trial and error.


Yes and I can even give you the pseudo-code:
function Halt?
return can't tell

That satifies your description of it, so without any other guarantees about what kind of halting it detects it would be useless.

Share this post


Link to post
Share on other sites
Quote:
Original post by ROBERTREAD1
Now is it possible to say

a) it does halt.
b) it doesn't halt.
c) I can't tell if it will or not.
d) I can't tell if it will or not and here's the reason.

it would very handy for a post compiler check.

Predicate maths helped me tidy up my code immensely. I found it really useful, finally I could say WHY I coded things in particular ways I had discovered by trial and error.


The Halting problem is undecidable which means there does not exist a yes/no procedure that can tell you what will happen always. Your compiler could have:

a) it halts (e.g. it doesn't use recursion for trivially halts; it is defined by primitive recursion; it has a valid terminating measure)
b) it doesn't halt (e.g. I can prove the input to the recursive call always grows)
c) I do not know if it halts (it might be have, say, a terminating measure or a proof that it loops forever but the system just isn't smart enough to find it)

An example of c from http://en.wikipedia.org/wiki/Halting_Problem (worth a read, it's well written) is:

function findTwinPrimeAbove(int N)
int p = N
loop
if p is prime and p + 2 is prime then
return
else
p = p + 1

If you can find if this halts, you have an answer to the unsolved twin prime conjecture (i.e. a really hard long standing math problem). The conjecture could be true or it could be false, so until we prove/disprove it we won't know if this function halts or not.

There are compilers/system that exist today that can check for termination. See here for an annual competition on termination checking:
http://www.lri.fr/~marche/termination-competition/2006/

Share this post


Link to post
Share on other sites
speaking of that twin prime thingy oh i bet the OP just can't wait till they cover goedel's incompleteness theorem ha ha ha. oh, that was fun too lol. oh the things that lurk in a computation class...

Share this post


Link to post
Share on other sites
Is Gödel's incompleteness theory and the halting problem related?

Maybe Gödel's unprovable axioms are equivalent to a set of assumed functions that always halt?

Share this post


Link to post
Share on other sites
The First Incompleteness Theorem and the Halting Problem (also the Church Turing Belief/Argument, whose truth or not places constraints on the universe because of the first two theorems) are all related. I have seen a proof of Godels Theorem in terms of the Halting theorem.

As well, both the incompleteness theorem and halting hinge on a method quite similar to Russell's Paradox to express their thesis and so will have similar structures. But no, they are not equivalent I do not think. I think Godel's might be more general.

I have a question that I hope someone may answer. I know of a language - Charity - that does not suffer from the Halting Problem, all programs on it terminate. That is, it is not turing complete. What are the consequences of this on the scope and applicability or strength of the language?

Share this post


Link to post
Share on other sites
Quote:
Original post by Daerax
I have a question that I hope someone may answer. I know of a language - Charity - that does not suffer from the Halting Problem, all programs on it terminate. That is, it is not turing complete. What are the consequences of this on the scope and applicability or strength of the language?


The most important is the inability to bootstrap: you cannot emulate a program of that language in that language. Because if you could, non-termination would be simple.

Share this post


Link to post
Share on other sites
Sign in to follow this  

  • Advertisement
×

Important Information

By using GameDev.net, you agree to our community Guidelines, Terms of Use, and Privacy Policy.

Participate in the game development conversation and more when you create an account on GameDev.net!

Sign me up!