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....."
Question about the Halting Problem
Quote:Original post by ToohrVykQuote: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.
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.
Quote:Original post by Daerax
Would 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.
Quote:Original post by ToohrVykQuote:Original post by Daerax
Would 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]
Quote:Original post by DaeraxQuote:Original post by ToohrVykQuote:Original post by Daerax
Would 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.
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:
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.
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.
Quote:Original post by ToohrVyk
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.
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: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?
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.
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.
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 ToohrVyk
Identity: 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.
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.
Quote:Original post by Daerax
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.
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.
This topic is closed to new replies.
Advertisement
Popular Topics
Advertisement
