A Possible "solution" to the Halting Problem
in [Theory]
|
From: Peter Olcott on 22 Oct 2006 09:58 "Patricia Shanahan" <pats(a)acm.org> wrote in message news:QtK_g.13324$Y24.9698(a)newsread4.news.pas.earthlink.net... > Peter Olcott wrote: >> "Patricia Shanahan" <pats(a)acm.org> wrote in message >> news:4dx_g.17125$UG4.12313(a)newsread2.news.pas.earthlink.net... >>> Peter Olcott wrote: >>>> "Patricia Shanahan" <pats(a)acm.org> wrote in message >>>> news:yWw_g.10604$Lv3.9258(a)newsread1.news.pas.earthlink.net... >>>>> Peter Olcott wrote: >>>>> ... >>>>>> 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?" >>>>> Do you think your "Ill formed statement" condition is computable? >>>>> >>>>> Patricia >>>> If we make the usual assumptions that are made in the HP, then yes. If we >>>> assume that an algorithm is capable of correctly determining whether or not >>>> another program halts, at least in each and every case where this is >>>> possible, then this same algorithm would by definition already know the >>>> ill-formed cases. The ill-formed cases would be any case where it can >>>> neither conclude HALTS, nor conclude NOT_HALTS. >>> I do NOT "assume that an algorithm is capable of correctly determining >>> whether or not another program halts", whether or not qualified by "at >>> least in every case in which this is possible". >>> >>> It is certainly not an assumption that is usually made in discussing the >>> halting problem, other than in the sense that some versions of the proof >>> use a proof by contradiction form, in which the prover temporarily >>> assumes something exists, demonstrates a contradiction, and concludes it >>> does not exist. >> >> I am not taking on the burden of proving that solving the HP is possible. The >> most burden that I am taking on is showing that there might have been some >> errors with some of the prior proofs that solving the HP is impossible. >> Within the context of the above mentioned assumptions, if I can merely show >> that the conclusions drawn from these assumptions and proofs might not >> logically follow from the logic of these proofs, I have met the minimum >> degree of my original goals. > > The problem with this is that I believe you need a Turing machine > halting problem decider to decide the MSR condition: > > 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. > > As a Turing machine simulator, it does not allow for exceptions. It > 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. > > In order to decide whether to throw the exception or not, at least > according to your current definition, you need to know whether Turing > returns or not. That can be determined only by a general, no exceptions, > Turing machine halting problem decider. > > someTM may involve code equivalent to your HaltTest implementation, with > the exception treated as a form of halting. Regardless of that, you need > to know whether it halts. > > A lot of questions about dynamic properties of programs, such as "does > it ever reach this statement", turn out to be halting problem > equivalent. I will be surprised if you can find a specification for the > MSR condition that is decidable. > > Patricia 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. If in each and every specific attempt to provide a valid counter-example that Halting is undecidable I can show that this specific attempt has failed, I will have met my maximum burden of proof. In other words I would be able to show (at least for the moment) that whether or not Halting is decidable, is currently undecided.
From: Markus Triska on 22 Oct 2006 10:29 "Peter Olcott" <NoSpam(a)SeeScreen.com> writes: > In other words I would be able to show (at least for the moment) > that whether or not Halting is decidable, is currently undecided. It's easy to show that HP isn't decidable (you can lead the assumption that it's decidable to a contradiction). Better use a different terminology to avoid confusion. Best wishes! Markus Triska
From: Peter Olcott on 22 Oct 2006 10:45 "Markus Triska" <triska(a)gmx.at> wrote in message news:873b9g77bi.fsf(a)gmx.at... > "Peter Olcott" <NoSpam(a)SeeScreen.com> writes: > >> In other words I would be able to show (at least for the moment) >> that whether or not Halting is decidable, is currently undecided. > > It's easy to show that HP isn't decidable (you can lead the assumption > that it's decidable to a contradiction). Better use a different > terminology to avoid confusion. > > Best wishes! > Markus Triska My recent posting on a thread entitled "Is the Halting Problem merely an ill-formed question?" attempts to show that the conclusion of a formed contradiction may be incorrect.
From: Patricia Shanahan on 22 Oct 2006 11:09 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
From: Peter Olcott on 22 Oct 2006 11:38
"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. |