King of Men 394 Report post Posted May 23, 2007 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? 0 Share this post Link to post Share on other sites
monstermunch 100 Report post Posted May 23, 2007 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_functionPrimitive 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= 0 Share this post Link to post Share on other sites
yadango 567 Report post Posted May 24, 2007 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. 0 Share this post Link to post Share on other sites
ROBERTREAD1 100 Report post Posted May 24, 2007 Now is it possible to saya) 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. 0 Share this post Link to post Share on other sites
CTar 1134 Report post Posted May 24, 2007 Quote:Original post by ROBERTREAD1Now is it possible to saya) 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 tellThat satifies your description of it, so without any other guarantees about what kind of halting it detects it would be useless. 0 Share this post Link to post Share on other sites
monstermunch 100 Report post Posted May 24, 2007 Quote:Original post by ROBERTREAD1Now is it possible to saya) 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 + 1If 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/ 0 Share this post Link to post Share on other sites
yadango 567 Report post Posted May 25, 2007 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... 0 Share this post Link to post Share on other sites
ROBERTREAD1 100 Report post Posted May 25, 2007 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? 0 Share this post Link to post Share on other sites
Daerax 1207 Report post Posted May 25, 2007 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? 0 Share this post Link to post Share on other sites
ToohrVyk 1596 Report post Posted May 25, 2007 Quote:Original post by DaeraxI 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. 0 Share this post Link to post Share on other sites
yadango 567 Report post Posted May 25, 2007 oh, he he he, i was relating GIT to the twin prime conjecture. we know it is true, but can't prove that it's true (at least not yet). in Sipser 6.2 you cover both. oh man... i remember my prof as he was doing the proof of GIT on the board:Prof: "La di da di da da..." writing proof on board...Prof: Stops and asks, "Do you understand?"Students: "No."Prof: "La di da di da da..." writing more proof on board...Prof: Stops and asks, "Do you understand?"Students: "No."Prof: "La di da di da da..." writing more proof on board...Prof: Stops and asks, "Do you understand?"Students: "No."Prof: "La di da di da da..." writing more proof on board...Prof: Stops and asks, "Do you understand?"Students: "Killlll meeeeeeeee....." 0 Share this post Link to post Share on other sites
Daerax 1207 Report post Posted May 25, 2007 Quote:Original post by ToohrVykQuote:Original post by DaeraxI 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.Would I be correct in guessing that a consequence of this means that a compiler for charity can never be written in Charity? What are other consequences of an inability to bootstrap? No reflection? This does not seem like much of a loss.Thanks.P.s. yadango, we do not know that the twin prime conjecture is true otherwise it would not be a conjecture :p. It is safer to say some mathematicians believe that that it should be true. 0 Share this post Link to post Share on other sites
ToohrVyk 1596 Report post Posted May 25, 2007 Quote:Original post by DaeraxWould I be correct in guessing that a consequence of this means that a compiler for charity can never be written in Charity?It's not certain: the compiler could output code in a turing-complete language (for instance, a language which is a syntactical superset of Charity, through an identity function). The resulting code could not be interpreted in Charity, however. 0 Share this post Link to post Share on other sites
Daerax 1207 Report post Posted May 25, 2007 Quote:Original post by ToohrVykQuote:Original post by DaeraxWould I be correct in guessing that a consequence of this means that a compiler for charity can never be written in Charity?It's not certain: the compiler could output code in a turing-complete language (for instance, a language which is a syntactical superset of Charity, through an identity function). The resulting code could not be interpreted in Charity, however.Should it not be inclusion rather than identity? Anyways thanks for the clarification =). I guess I just dont understand why everyone is so hung up on turing completeness.[Edited by - Daerax on May 25, 2007 9:29:17 AM] 0 Share this post Link to post Share on other sites
monstermunch 100 Report post Posted May 25, 2007 Quote:Original post by DaeraxQuote:Original post by ToohrVykQuote:Original post by DaeraxWould I be correct in guessing that a consequence of this means that a compiler for charity can never be written in Charity?It's not certain: the compiler could output code in a turing-complete language (for instance, a language which is a syntactical superset of Charity, through an identity function). The resulting code could not be interpreted in Charity, however.Should it not be inclusion rather than identity? Anyways thanks for the clarification =). I guess I just dont understand why everyone is so hung up on turing completeness.Me either. I don't claim to be an expect on this, but to me, Halting is more a theoretical barrier than a practical one. The question "can we prove all programs halt?" is interesting, but not as important as "can we prove all programs that have some practical use halt?". When you write computer programs, you normally think along the lines of "this loops until this becomes true, and this becomes true when this number gets so big etc. so it should eventually stop" e.g. I'm sure you know why your 3D engine doesn't loop forever. We don't just throw constructs together to make a random program and then puzzle about whether it terminates or not.http://en.wikipedia.org/wiki/Church-Turing_thesis"The thesis can be stated as:"Every 'function which would naturally be regarded as computable' can be computed by a Turing machine.""This doesn't say anything about whether we would actually want to compute all computable things. 0 Share this post Link to post Share on other sites
ToohrVyk 1596 Report post Posted May 25, 2007 Identity: you just output the input file as is.As for Turing-completeness, it's primarily a business reason: you don't want to be caught trying to develop a program which (you discover later on) cannot be developed using your language, but can't be done in another.Besides, the halting problem is not important in real life. People don't care if programs halt. And anyway, by page 30 or 40 in any C++ book, you will have written a correct and wanted program which doesn't halt:char q = '\0';while (std::cin >> q && q != 'q') std::cout << "Press 'q' to quit" << std::endl;A more important metric is postcondition verification: does my function truly sort this array? A secondary one, although less important, is runtime error detection: does my code overflow any buffers?And, while these are also undecidable, people are getting damn close to getting a correct and useful answer in most practical situations. 0 Share this post Link to post Share on other sites
monstermunch 100 Report post Posted May 25, 2007 Quote:Original post by ToohrVykAs for Turing-completeness, it's primarily a business reason: you don't want to be caught trying to develop a program which (you discover later on) cannot be developed using your language, but can't be done in another.Church-Turing is still a thesis though. It might turn out (though unlikely) that there's someone we would want to compute something that a Turing machine cannot. You can have your cake and eat it; use a language which always terminates and then when it's not powerful enough, use a language that allows non-terminating functions.Quote:Besides, the halting problem is not important in real life. People don't care if programs halt. And anyway, by page 30 or 40 in any C++ book, you will have written a correct and wanted program which doesn't halt:People do care! :-) Nobody wants infinite loops if they can be avoided. Programmers are just conditioned into thinking its a problem that no help can be offered for.[quote]Quote:char q = '\0';while (std::cin >> q && q != 'q') std::cout << "Press 'q' to quit" << std::endl;I would say represent this in your non-terminating language (e.g. C++) and use it to call your terminating one in the loop. You then prove termination of e.g. sorting, in the latter language.Quote:A more important metric is postcondition verification: does my function truly sort this array? A secondary one, although less important, is runtime error detection: does my code overflow any buffers?You can still do all these things and optionally verify termination; it's not like you have to choose between them. Depending on the application, termination can be very important e.g. hardware drivers.Quote:And, while these are also undecidable, people are getting damn close to getting a correct and useful answer in most practical situations.This is the same as the Halting problem though, isn't it? Godel tells us that proving buffers will not overflow is undecidable. Halting says proving termination is undecidable. As long as we can prove termination for practical programs and prove non-overflowing buffers for practical programs, then this should not be an issue. Defining practical is a problem though.I'm not an expert on this, but imagine I had a computer program and my advanced verifier system says "using all my most powerful techniques, I cannot prove that this terminates or if it has a buffer overflow or not". Surely this is a pretty good indication the program is wrong because then surely the programmer themselves would have no clue if it terminates or not? 0 Share this post Link to post Share on other sites
Daerax 1207 Report post Posted May 25, 2007 Again thanks, ToohrVyk. Im satisfied with that response. Turing completeness is basically a just in case safeguard and whether or not a program will halt rarely enters into practical considerations. Not much of a problem then huh. hehe.Although, in terms of verification whether or not a program halts is a big deal. One can leverage the Curry Howard Isomorphism to show that a formal proof written in a language such as Coq or Charity must be correct if its execution halts. Quote:Original post by ToohrVykIdentity: you just output the input file as is.I specified inclusion because the domain and codomain on the inclusion function seems more appropriate based on what you stated. Suppose C was our Turing incomplete language and C_S was our complete version. If it is identity then it must either be id : C_S -> C_S or id: C -> C. The second function is obviously not the case but the domain of the first seems too large. With inclusion i, one gets i:C -> C_S. i(x) = x. Hence my feeling inclusion is more appropriate. 0 Share this post Link to post Share on other sites
Sharlin 864 Report post Posted May 25, 2007 Halting problem is mostly important in that there are many more interesting problems that can be proven to be unsolvable by reducing them to the Halting problem. 0 Share this post Link to post Share on other sites
Timkin 864 Report post Posted May 25, 2007 Quote:Original post by DaeraxAs 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. Actually, I believe that Chaitin has shown that they are equivalent. If, for any program you ask what is the probability that it halts, and then ask the subsequent question, "If I know the values of the first N bits of this probability, what is the value of the N+1'th bit?", you find that you cannot answer the question. From recollection, it turns out that Godel's Theorem, Heisenberg's Principle and the Halting Problem are all expressions of the same fundamental problem. 0 Share this post Link to post Share on other sites
Monder 993 Report post Posted May 26, 2007 Quote:that can be proven to be unsolvable by reducing them to the Halting problem.Actually in order to prove something uncomputable you'd need to reduce the halting problem to it (as that means if you have a solution to that problem you'd have a solution to the halting problem). For a simple example of something computable that could be reduced to the halting problem take the decision problem of deciding whether something is the smallest element of the list. You'd construct a program that takes a list and an element of the list, it loops through the list and if it finds no element smaller than the element you give, it halts otherwise it loops forever. Then the problem of whether the element you give is the smallest member of the list becomes, given this program (detailed above) and this list and an element as input, does the program halt? Thus we have reduced the problem to the halting problem, though the original problem is clearly computable. 0 Share this post Link to post Share on other sites
kSquared 1356 Report post Posted May 26, 2007 Quote:Original post by MonderActually in order to prove something uncomputable you'd need to reduce the halting problem to it (as that means if you have a solution to that problem you'd have a solution to the halting problem).Actually, you're saying the same thing either way. "X reduces to Y" means "X is Y"; the precise nature of "is" here depends on the problem you're solving. Whether we say "X reduces to Y" or "Y reduces to X" just depends on which expression is perceived to be more complicated.Because it's generally easier to reduce things to simpler forms, proofs generally show how a more complicated solution is like a previously solved, simpler form. For example, consider the statement "(m^2 - n^2)/(m - n) == m + n". We can prove this either by:(1) Try to gradually make changes to "m + n" until you arrive at "(m^2 - n^2)/(m - n)".(2) Try to gradually make changes to "(m^2 - n^2)/(m - n)" until you arrive at "m + n".If you're successful either way, you've shown that X is Y.Quote:Original post by MonderFor a simple example of something computable that could be reduced to the halting problem take the decision problem of deciding whether something is the smallest element of the list.[...]Thus we have reduced the problem to the halting problem, though the original problem is clearly computable.The halting problem doesn't ask whether a specific program will terminate. It asks whether it's possible, in general, to decide if any given program will terminate.In other words, the halting problem asks whether it's possible to write a function H(p) that takes a program p as input, and that returns "true" if the program terminates and "false" if it doesn't. Your program is simply one example of a possible p (any program is, of course), but it's not an H. An H that only works for one particular p is also not an H, so either way, this example does not reduce to the halting problem.Here's another example: imagine that, instead of H, I ask you to write S(n), the successor function. This simply takes any integer n as input and adds one to it. Would you be satisfied that this was really the successor function if it only worked with an input of 271?Your program is trivial enough that you can show that it will, in fact, always halt. You can actually do even better, since you can say how the expected running time of the program is (number of list elements multiplied by the time cost to make a comparison). As long as the list is finite and there is a finite upper bound on how long it takes to determine if a particular element is the smallest thus far, it will terminate. 0 Share this post Link to post Share on other sites
ToohrVyk 1596 Report post Posted May 26, 2007 Quote:Original post by kSquaredIn other words, the halting problem asks whether it's possible to write a function H(p) that takes a program p as input, and that returns "true" if the program terminates and "false" if it doesn't. Your program is simply one example of a possible p (any program is, of course), but it's not an H. An H that only works for one particular p is also not an H, so either way, this example does not reduce to the halting problem.Here's another example: a program M(x,a) which determines if x is the minimal element of array a. We build the program:program P is: for i = 1 to a.size do while x > a[i] do () done doneThen, x is the minimal element of a if and only if H(P) returns true (where H is a program solving the halting problem). We have effectively reduced our "is minimal element" problem to the halting problem: if a solution to the halting problem exists, then a solution to the minimal element problem exists. In general, in computability theory, reduction is a complex relationship, which depends on the way in which the reduction is done (time and space complexity, for instance) and is generally not symmetrical. The typical intuition is that X is A-reductible to Y if there exist two processes with property A so that a problem in X can be transformed into a problem in Y, and a solution in Y can be transformed into a solution in X. This implies that being able to solve problems in Y lets you solve problems in X, but not necessarily the reverse. 0 Share this post Link to post Share on other sites
Monder 993 Report post Posted May 26, 2007 Quote:Actually, you're saying the same thing either way. "X reduces to Y" means "X is Y"; the precise nature of "is" here depends on the problem you're solving. Whether we say "X reduces to Y" or "Y reduces to X" just depends on which expression is perceived to be more complicated.Depends upon how you define reduction, here I'm defining it as in complexity theory where a reduction is a function that given two languages L1 and L2 which are decidable by turing machines T1 and T2 will take a member of L1 and transform it into a member of L2. Futhermore anything that isn't in L1 will be transformed into something that isn't in L2. There is no requirement for this function to be injective, or surjective, thus you can define a reduction that will only work one way. This is generally used in proofs of NP-Completeness you take a language known to be NP hard and define a reduction that can reduce it to another language you wish to prove NP hard in polynomial time (and of course the other part is proving the language you wish to prove NP complete is indeed in NP).Now about my reducing to the halting problem example, here it is again but slightly more formally so it's clearer what I actually mean.Here when I say halting problem, I mean given a encoding of some computable function P and an input to that function x, can you build a turing machine that given P and x as inputs halts in either an accepting state if P(x) halts or halts in a rejecting state is P(x) does not halt? Thus the language of the halting problem (lets call it H) is a set of pairs (P, x) where if (P, x) is in H then P(x) halts, otherwise if (P, x) is not in H then P(x) does not halt (Another way to phrase that halting problem would be can you build a turning machine that decides membership of H?).Now take my smallest element of list decision problem. Here the language (lets call it SMALL) is again a set of parts (L, x) where L is a finite list and x is an element from that list. A pair (L, x) is in SMALL if and only if x is a member of L and it is the smallest member of L.We then define a reduction from SMALL to H as follows: Given (L, x) in SMALL construct a turing machine that iterates through L and takes x as the initial contents of the tape. If at any point it finds an element of L that is smaller than x it loops forever, if it reaches the end of the list and x has not been found (i.e. x is not in L) then it loops forever, otherwise it halts. Clearly the machine will halt if and only if x is in L and it is the smallest element of L, otherwise it will not halt. Thus we can reduce SMALL to H and if we can decide membership of H (i.e. we can solve the halting problem) we can decide membership of SMALL.Now SMALL is clearly a decidable language, while H is not, hence we can reduce things that are decidable to things that are not (actually if you allow L to be infinite, then you can probably manage to reduce H to SMALL, though I won't attempt that here). 0 Share this post Link to post Share on other sites
kSquared 1356 Report post Posted May 26, 2007 Quote:Original post by ToohrVykThen, x is the minimal element of a if and only if H(P) returns true (where H is a program solving the halting problem). We have effectively reduced our "is minimal element" problem to the halting problem: if a solution to the halting problem exists, then a solution to the minimal element problem exists. I agree with that, I just don't agree with the other relationship: that merely because you had a P that was easy to H-solve, that your P is an H, which is what the other post seemed to be saying.Quote:In general, in computability theory, reduction is a complex relationship, which depends on the way in which the reduction is done (time and space complexity, for instance) and is generally not symmetrical.Well, there are two types of reduction: Turing (which is symmetrical) and many-one (which isn't). The former is more powerful, because it says that a solution to either is a solution to both. But the latter is more useful in the pragmatic sense, because we don't generally get lucky enough to find Turing reductions (in fact, finding any TR for most "hard" problems amounts to determining that P is NP). 0 Share this post Link to post Share on other sites