A Possible "solution" to the Halting Problem
in [Theory]
|
From: Patricia Shanahan on 22 Oct 2006 12:25 Peter Olcott wrote: > "Patricia Shanahan" <pats(a)acm.org> wrote in message > news:RQL_g.14948$o71.5933(a)newsread3.news.pas.earthlink.net... >> Peter Olcott wrote: >> ... >>> I don't need to show that MSR is decidable to completely prove my point. All >>> that my maximum burden of proof requires is that I show that prior proofs >>> that Halting is undecidable are incorrect. >> To do that, I think you need a definition of MSR that is at least not >> provably undecidable. The current definition fails that test. >> >> Patricia >> > > Okay, then show how it is provably un-decidable. This will require only a single > example. Try to do it as a variation of the LoopIfHalts() / WillHalt() form that > I have presented. > > In general, I disagree saying, in effect, "Prove your claim, but only using proof methods I choose". When I'm proving something, I get to pick any logically valid proof approach. However, the example I just posted is indeed a variation on the LoopIfHalts example, with small changes to make the MSR decision non-trivial. ====================================================================== int HaltTest(HaltTestSource){ if(WillHalt(HaltTestSource,HaltTestSource){ Turing(someTM, someInput); }else{ return; } } Suppose HaltTestSource is the source code for HaltTest, including the strings specifying someTM and someInput. Turing is a Turing machine simulator that runs someTM with someInput as initial tape contents. Turing returns if, and only if, someTM reaches a terminal state when run with initial tape contents someInput. If someTM(someInput) halts, then this program halts regardless of the result of WillHalt. WillHalt can, and should, return TRUE. If someTM(someInput) does not halt, then WillHalt should throw an MSR exception. ====================================================================== If the Turing call does not return HaltTest, called with its own source code, is exactly equivalent to your LoopIfHalts. If the Turing call does return, this example is equivalent to a call to WillHalt followed by an unconditional return. This example proves that MSR decidability, as MSR is currently defined, would imply full decidability, in the original sense rather than your modified form, of the Turing machine halting problem. Patricia
From: Peter Olcott on 22 Oct 2006 12:58 "Patricia Shanahan" <pats(a)acm.org> wrote in message news:3YM_g.14968$o71.5033(a)newsread3.news.pas.earthlink.net... > Peter Olcott wrote: >> "Patricia Shanahan" <pats(a)acm.org> wrote in message >> news:RQL_g.14948$o71.5933(a)newsread3.news.pas.earthlink.net... >>> Peter Olcott wrote: >>> ... >>>> I don't need to show that MSR is decidable to completely prove my point. >>>> All that my maximum burden of proof requires is that I show that prior >>>> proofs that Halting is undecidable are incorrect. >>> To do that, I think you need a definition of MSR that is at least not >>> provably undecidable. The current definition fails that test. >>> >>> Patricia >>> >> >> Okay, then show how it is provably un-decidable. This will require only a >> single example. Try to do it as a variation of the LoopIfHalts() / WillHalt() >> form that I have presented. > > In general, I disagree saying, in effect, "Prove your claim, but only > using proof methods I choose". When I'm proving something, I get to pick > any logically valid proof approach. > > However, the example I just posted is indeed a variation on the > LoopIfHalts example, with small changes to make the MSR decision > non-trivial. It would seem that from the conclusions that you are making about your own proof, that this proof does not meets its original burden of proof. The specification requires providing at least one example of a definition of a MSR that is [provably undecidable]. Providing an example of a [MSR decision non-trivial] does not meet the burden of proof of an example of MSR that is [provably undecidable]. None-the-less, I will print out your example and carefully study it. > > ====================================================================== > > int HaltTest(HaltTestSource){ > if(WillHalt(HaltTestSource,HaltTestSource){ > Turing(someTM, someInput); > }else{ > return; > } > } > > Suppose HaltTestSource is the source code for HaltTest, including the > strings specifying someTM and someInput. > > Turing is a Turing machine simulator that runs someTM with someInput as > initial tape contents. > > Turing returns if, and only if, someTM reaches a terminal state when run > with initial tape contents someInput. > > If someTM(someInput) halts, then this program halts regardless of the > result of WillHalt. WillHalt can, and should, return TRUE. > > If someTM(someInput) does not halt, then WillHalt should throw an MSR > exception. > > ====================================================================== > > If the Turing call does not return HaltTest, called with its own source > code, is exactly equivalent to your LoopIfHalts. If the Turing call does > return, this example is equivalent to a call to WillHalt followed by an > unconditional return. > > This example proves that MSR decidability, as MSR is currently defined, > would imply full decidability, in the original sense rather than your > modified form, of the Turing machine halting problem. > > Patricia
From: sillybanter on 22 Oct 2006 13:22 In comp.theory Patricia Shanahan <pats(a)acm.org> wrote: > sillybanter(a)gmail.com wrote: > > In comp.theory Patricia Shanahan <pats(a)acm.org> wrote: > > > >> If you take the existence of a decision algorithm for the Halting > >> problem as an axiom, while retaining the normal axioms that ultimately > >> underly theory of computation, you end up with an inconsistent system of > >> axioms. Even then, it is the set of axioms that is broken, not the > >> fundamental concept of truth. > > > > Not to confuse the mainline discussion going on in this thread, but I > > wanted to point out that if you're careful about how you do this then > > you don't get an inconsistent system. For example, you can add an > > "oracle" the the TM model where the oracle can decide the halting > > problem. > > I can see that you could reason about Turing computation plus a halting > oracle, but I would not call a halting oracle "a decision algorithm". I > suppose it depends on your attitude to the Church-Turing thesis - can > something be an "algorithm" if no Turing machine computes it? I suppose that's a terminology difference, but I'd certainly call this an algorithm... An algorithm is just a description of steps that solves a problem - the model of computation for this algorithm is a separate issue, so I can certainly have algorithms that are designed for an oracle machine, even if no such machine could ever be built. -- Steve Stringer sillybanter(a)gmail.com
From: Patricia Shanahan on 22 Oct 2006 13:24 Peter Olcott wrote: > "Patricia Shanahan" <pats(a)acm.org> wrote in message > news:3YM_g.14968$o71.5033(a)newsread3.news.pas.earthlink.net... >> Peter Olcott wrote: >>> "Patricia Shanahan" <pats(a)acm.org> wrote in message >>> news:RQL_g.14948$o71.5933(a)newsread3.news.pas.earthlink.net... >>>> Peter Olcott wrote: >>>> ... >>>>> I don't need to show that MSR is decidable to completely prove my point. >>>>> All that my maximum burden of proof requires is that I show that prior >>>>> proofs that Halting is undecidable are incorrect. >>>> To do that, I think you need a definition of MSR that is at least not >>>> provably undecidable. The current definition fails that test. >>>> >>>> Patricia >>>> >>> Okay, then show how it is provably un-decidable. This will require only a >>> single example. Try to do it as a variation of the LoopIfHalts() / WillHalt() >>> form that I have presented. >> In general, I disagree saying, in effect, "Prove your claim, but only >> using proof methods I choose". When I'm proving something, I get to pick >> any logically valid proof approach. >> >> However, the example I just posted is indeed a variation on the >> LoopIfHalts example, with small changes to make the MSR decision >> non-trivial. > > It would seem that from the conclusions that you are making about your own > proof, that this proof does not meets its original burden of proof. > > The specification requires providing at least one example of a definition of a > MSR that is [provably undecidable]. I was using the definition of MSR you gave earlier. It is a fine example of a definition of MSR that is provably undecidable. =================================================================== I was going to go through several different concrete examples, but, what it boils down to is simply this: There are cases where WillHalt() can correctly determine whether or not LoopIfHalts() will halt or not, and return this value, and there are cases where WillHalt() can correctly determine whether or not LoopIfHalts() will halt or not, and is unable to return this value, and there are cases where the only reason that WillHalt() can not determine whether or not LoppIfHalts() halts, is because the question itself is ill-formed. We can precisely define what is meant by an ill-formed question by saying that an ill-formed question is any question that has no possible correct answer from the required solution set. The variation of the HP that your example refers to has no correct YES or NO answer, thus derives an ill-formed question equivalent to the question: "How tall are you red or blue?" =================================================================== Patricia
From: sillybanter on 22 Oct 2006 13:36
In comp.theory Peter Olcott <NoSpam(a)seescreen.com> wrote: > <sillybanter(a)gmail.com> wrote in message news:obw_g.1640$hK.1002(a)trnddc02... > > In comp.theory Peter Olcott <NoSpam(a)seescreen.com> wrote: > >> > >> <sillybanter(a)gmail.com> wrote in message news:Tsr_g.8573$A27.1777(a)trnddc08... > >> > In comp.theory Peter Olcott <NoSpam(a)seescreen.com> wrote: > >> >> <sillybanter(a)gmail.com> wrote in message news:oF5_g.21$A27.19(a)trnddc08... > >> >> > In comp.theory Peter Olcott <NoSpam(a)seescreen.com> wrote: > >> >> >> <sillybanter(a)gmail.com> wrote in message > >> >> >> news:TDYZg.3794$4T6.1422(a)trnddc02... > >> >> >> > In comp.theory Peter Olcott <NoSpam(a)seescreen.com> wrote: > >> >> >> >> > >> >> >> >> <sillybanter(a)gmail.com> wrote in message > >> >> >> >> news:bnLZg.5347$NK5.1822(a)trnddc08... > >> >> >> >> > In comp.theory Peter Olcott <NoSpam(a)seescreen.com> wrote: > >> >> >> >> > > >> >> >> >> >> So the equivalent of the return value of the Halt() function from > >> >> >> >> >> the TM is the integer value that the TM's ReadWrite head rests on > >> >> >> >> >> when the TM halts. In this case DOES_NOT_HALT=0 HALTS=1 > >> >> >> >> >> MALIGNANT_SELF_REFERENCE=2. This scenario breaks out of the > >> >> >> >> >> infinite > >> >> >> >> >> recursion of the original specification of the problem, and > >> >> >> >> >> provides > >> >> >> >> >> the only possible correct answer. > >> >> >> >> > > >> >> >> >> > In the standard presentation of the halting problem, there is no > >> >> >> >> > recursion, infinite or otherwise. Don't be confused by the fact > >> >> >> >> > that > >> >> >> >> > the same name of a function is used in the analyzed program and in > >> >> >> >> > the > >> >> >> >> > analyzer - it's not the same thing, and these two instances of > >> >> >> >> > "Halt" are completely separate. > >> >> >> >> > >> >> >> >> See the ANALYTICAL COMMENTARY of this example mentioned below to > >> >> >> >> see > >> >> >> >> my > >> >> >> >> current > >> >> >> >> point. > >> >> >> > > >> >> >> >> ... > >> >> >> > > >> >> >> >> // ANALYTICAL COMMENTARY > >> >> >> >> WillHalt() is provided with the source code of LoopIfHalts(), as > >> >> >> >> input, so WillHalt() can see exactly how the return value of the > >> >> >> >> invocation of itself under test will be used to toggle the result > >> >> >> >> of the analysis of the invocation of itself under test. WillHalt() > >> >> >> >> can see that LoopIfHalts() is toggling the result of the invocation > >> >> >> >> of itself under test to invalidate the analysis of the invocation > >> >> >> >> of itself under test. > >> >> >> >> > >> >> >> >> Therefore WillHalt() can determine that the question: > >> >> >> >> "Does LoopIfHalts(LoopIfHalts) halt?" has no correct YES or NO > >> >> >> >> answer, and is thus erroneously formed because it is asking a > >> >> >> >> YES or NO question that has no correct YES or NO answer. > >> >> >> > > >> >> >> > Except that it, of course, DOES have a correct YES or NO answer. > >> >> > > >> >> >> So which of the correct YES or NO answers can WillHalt() provide > >> >> >> such that it has provided the correct YES or NO answer? If you are > >> >> >> correct, then you MUST be able to correctly select one of these, > >> >> >> otherwise YOU ARE INCORRECT!!! THERE EXISTS NO CORRECT YES OR NO > >> >> >> ANSWER THAT WillHalt() CAN POSSIBLY PROVIDE, THUS THIS HALTING > >> >> >> PROBLEM IS MERELY THE CASE OF THE INABILITY TO CORRECTLY ANSWER AN > >> >> >> ILL-FORMED QUESTION ENTIRELY DUE TO THE FACT THAT THE QUESTION > >> >> >> ITSELF IS ILL-FORMED!!! > >> >> > > >> >> > If you really think about what you yourself just wrote there, you > >> >> > would see that you've exactly described the contradiction that is the > >> >> > heart of the halting problem proof, and hence you have proved that the > >> >> > halting problem is undecidable. > >> > > >> >> Right there is the error. This reasoning has not shown that the HP > >> >> is undecidable. There is a subtle but crucial distinction between > >> >> deciding the correct answer to a question, and providing a correct > >> >> answer to a question. It is very possible to provide a correct > >> >> answer without knowing it (guessing is possible), and it is also > >> >> possible to know the correct answer without providing it. > >> > > >> > Then it hasn't "decided" the answer in the C.S. sense of the term. In > >> > this area, "decided" means that you have provided the correct answer. > >> > They are completely synonymous. To use your definition of "decided" > >> > you'd have to impart some notion of consciousness on the deciding TM > >> > so that it could say "I *know* the answer, but I'm not telling you." > > > >> Not really, all that is required is a Boolean memory variable that > >> is not used as a function call return value. > > > > Whether you "return" it or store it in a Boolean variable in memory > > and then don't return it is completely irrelevant to the halting > > problem. > > Not within the context of the single isolated example of > LoopIfHalts() and WillHalt() that I provided. Within this context > this example of a HP clearly shows that it is the specific > requirement of a Boolean return value that causes the whole > "problem". I think that this might be able to be generalized to the > UTM version of the HP, but, this generalization will have to wait > until the current point is conceded one way or the other. That's only a problem with the way that this proof constructs a specific input instance on which WillHalt fails. The deeper logic of the proof (beyond the superficial characteristic of which input) doesn't depend on a "return value" at all. > >> > And I can guarantee you that if you defined that notion (deciding but > >> > not telling) in a rigourous and unambiguous way that the halting > >> > problem would *still* be undecidable (by your new notion of > >> > decidability). > >> > >> The decision is simply stored in a local Boolean memory value, that > >> is not used as a function call return value. > > > > Let me be very specific - and *think* about this before you respond, > > because you have a habit of ignoring what people are telling you. > > > > Let's say you have a function PetersHaltDecision() that does what you > > say - stores the decision in a boolean variable and doesn't return it. > > I'll take your function and make StevesHaltDecision( |