From: Peter Olcott on 22 Oct 2006 15:28 "Jens Auer" <jens.auer-news(a)betaversion.net> wrote in message news:453bc0e2(a)news.ish.de... > Peter Olcott wrote: >> "Jens Auer" <jens.auer-news(a)betaversion.net> wrote in message >> news:453bbc0e(a)news.ish.de... >>> Peter Olcott wrote: >>>> My purpose is not to solve the Halting Problem. My purpose (at most) is to >>>> show that the conclusion of the HP is incorrect. Within this context I have >>>> determined three possible halt decision outcomes: >>>> (1) The Halt() function can determine that the program subject to test will >>>> halt, and can return this value. >>>> (2) The Halt() function can determine that the program subject to test will >>>> halt, yet can not return this value. >>>> (3) The Halt() function can determine that the program subject to test is >>>> constructed such that it can not be determined whether or not the program >>>> under test will halt because the question regarding the halting status of >>>> the program under test is ill-formed. Ill-formed is taken to mean that no >>>> correct solutions exist within the required solution set. >>>> >>>> If you can provide a concrete example of a HP proof that does not fall into >>>> one of these categories, please do. Try to do it in the form of WillHalt() >>>> / LoopIfHalts() if you can. >>> I first assume that your Halt function, implementing the three conditions >>> exists. Now, take your usual example source code (the one with the famous >>> analytical comment), together with a function WillHalt' (in the sense of >>> source code function) that behaves equivalent to WillHalt, but has a >>> different source code. Now form a new function LoopIfHalts2 by replacing the >>> call the WillHalt with WillHalt'. >>> For this function, Halt cannot determine that LoopIfHalts2 is constructed to >>> fool itself (unless you solve program equivalence), so only condition 1 and >>> 2 can hold. But for these conditions, we formed the usual contradiction, so >>> this Halt function cannot exist. >> >> I can't see what you mean, can you make this concrete by changing to >> functions below to reflect exactly what you are saying? >> >> void LoopIfHalts(string SourceCode) { >> if ( WillHalt(SourceCode, SourceCode) == TRUE ) >> while (TRUE) // loop forever >> ; >> else >> return; >> } >> >> int WillHalt(string SourceCode, string InputData) { >> if (MalignantSelfReference(SourceCode, InputData)) >> return MALIGNANT_SELF_REFERENCE; >> if ( TheProgramWillHalt(SourceCode, InputData) ) >> return TRUE; >> else >> return FALSE; >> } >> >> LoopIfHalts(LoopIfHalts); > I first assume that WillHalt exists and works. > I derive a new function WillHalt' from WillHalt. This function behaves exactly > like WillHalt, but has different source code, e.g. > int WillHalt'(string SourceCode, string InputData) { > int i = 1; > if (MalignantSelfReference(SourceCode, InputData)) > return MALIGNANT_SELF_REFERENCE; > if ( TheProgramWillHalt(SourceCode, InputData) ) > return TRUE; > else > return FALSE; > } > Actually, the real implementation doesn't matter. There are infinitely many of > them, and some don't even look similar. > I now construct LoopIfHalts2: > void LoopIfHalts2(string SourceCode) { > if (WillHalt'(SourceCode, SourceCode) == TRUE) > while (TRUE); > else return; > } > > If I feed this function LoopIfHalts2 to your WillHalt function, it results in > a contradiction: > 1) MalignantSelfReference fails because there is no reference to WillHalt in > LoopIfHalts2. Nice try, no cigar. You went through all the trouble of specifying WillHalt'() and LoopIfHalts2() to merely point out that LoopIfHalts2() does not form MalignantSelfReference() with WillHalt(). The problem is that it is still completely obvious (more obvious for some than others, apparently) that LoopIfHalts2() still forms MALIGNANT_SELF_REFERENCE with WillHalt'(). In this case WillHalt'() must indicate MALIGNANT_SELF_REFERENCE, whereas WillHalt() is free to return TRUE. > Of course, WillHalt and WillHalt' compute equivalent functions, but his is > undecidable in general (Check out Rice's theorem). > 2) If WillHalt decides that LoopIfHalt2 halt, than it goes directly into the > endless loop => contradiction > 3) If WillHalt decides that LoopIfHalt2 does not halt, it immediately returns > => contradiction > So, our assumption that WillHalt exists has lead us to contradictions, so they > must be false.
From: Jens Auer on 22 Oct 2006 15:43 Peter Olcott wrote: > Nice try, no cigar. You went through all the trouble of specifying WillHalt'() > and LoopIfHalts2() to merely point out that LoopIfHalts2() does not form > MalignantSelfReference() with WillHalt(). The problem is that it is still > completely obvious (more obvious for some than others, apparently) that > LoopIfHalts2() still forms MALIGNANT_SELF_REFERENCE with WillHalt'(). In this > case WillHalt'() must indicate MALIGNANT_SELF_REFERENCE, whereas WillHalt() is > free to return TRUE. So, if I feed LoopHalt2 into WillHalt, it finds the "MALIGNANT_SELF_REFERENCE"? This would be nice because it has to know that WillHalt and WillHalt' are equivalent. Congratulations, you solved the undecidable program equivalence problem. What exactly does MALIGNANT_SELF_REFERENCE do than? Does it search the source code for a function equivalent to WillHalt and check if it is used in some special way?
From: Patricia Shanahan on 22 Oct 2006 15:56 Jens Auer wrote: > Peter Olcott wrote: >> Nice try, no cigar. You went through all the trouble of specifying >> WillHalt'() and LoopIfHalts2() to merely point out that LoopIfHalts2() >> does not form MalignantSelfReference() with WillHalt(). The problem is >> that it is still completely obvious (more obvious for some than >> others, apparently) that LoopIfHalts2() still forms >> MALIGNANT_SELF_REFERENCE with WillHalt'(). In this case WillHalt'() >> must indicate MALIGNANT_SELF_REFERENCE, whereas WillHalt() is free to >> return TRUE. > So, if I feed LoopHalt2 into WillHalt, it finds the > "MALIGNANT_SELF_REFERENCE"? This would be nice because it has to know > that WillHalt and WillHalt' are equivalent. Congratulations, you solved > the undecidable program equivalence problem. The proofs I've seen of Rice's theorem use reduction from the halting problem. I don't know what WillHalt does if it equivalence decider throws an MSR. I'm being a bit more direct, by forcing WillHalt to decide, in the usual theory of computation sense, the Turing machine halting problem in order to know whether to throw the MSR. Patricia
From: Peter Olcott on 22 Oct 2006 16:12 "Jens Auer" <jens.auer-news(a)betaversion.net> wrote in message news:453bc9d5(a)news.ish.de... > Peter Olcott wrote: >> Nice try, no cigar. You went through all the trouble of specifying >> WillHalt'() and LoopIfHalts2() to merely point out that LoopIfHalts2() does >> not form MalignantSelfReference() with WillHalt(). The problem is that it is >> still completely obvious (more obvious for some than others, apparently) that >> LoopIfHalts2() still forms MALIGNANT_SELF_REFERENCE with WillHalt'(). In this >> case WillHalt'() must indicate MALIGNANT_SELF_REFERENCE, whereas WillHalt() >> is free to return TRUE. > So, if I feed LoopHalt2 into WillHalt, it finds the > "MALIGNANT_SELF_REFERENCE"? This would be nice because it has to know that > WillHalt and WillHalt' are equivalent. Congratulations, you solved the > undecidable program equivalence problem. No this is not what I said. If you feed LoopIfHalts2() to WillHalt(), then WillHalt'() sees the MALIGNANT_SELF_REFERENCE to itself. > > What exactly does MALIGNANT_SELF_REFERENCE do than? Does it search the source > code for a function equivalent to WillHalt and check if it is used in some > special way?
From: Jens Auer on 22 Oct 2006 16:18
Peter Olcott wrote: > No this is not what I said. If you feed LoopIfHalts2() to WillHalt(), then > WillHalt'() sees the MALIGNANT_SELF_REFERENCE to itself. So, there is not a single MALIGNANT_SELF_REFERENCE function, but one for each function? I have to ask you again, define either the set of MSR functions or give a definition of MSR, in terms of pseudo-code, Turing machine program or some equivalent statement. |