From: Patricia Shanahan on 18 Oct 2006 11:43 The Ghost In The Machine wrote: > In sci.logic, Peter Olcott > <NoSpam(a)SeeScreen.com> > wrote > on Tue, 17 Oct 2006 11:32:53 -0500 > <UA7Zg.8314$eZ4.3841(a)dukeread06>: >> "Charlie-Boo" <shymathguy(a)gmail.com> wrote in message >> news:1161101671.273314.18520(a)h48g2000cwc.googlegroups.com... >>> Peter Olcott wrote: >>>> The Halt program throws an "Invalid Input" exception. >>>> This would be analogous to the hardware exception of an attempt to divide by >>>> zero. >>> Are you aware of the fact that the Clay Institute offers a $1 million >>> reward for anyone who solves the Halting Problem? Alan Turing wasn't >>> able to and nobody has ever solved it since (except when using a >>> Computationally Based Logic). >>> >>> (I think Chaitin came closest by using a special number that vaporizes >>> as soon as you so much as think about it. Bit # N = whether or not I >>> will prove that I am not thinking about Chaitin at point in time N in >>> the future. (I hope I get all zeros.)) >>> >>> C-B >>> >>> -HALT(I,J)* The Halting Problem is Unsolvable >>> 1. NO(x,x) Known >>> 2. HALT(I,J)* PREMISE >>> 3. HALT(I,I)* SUB 2 >>> 4. ~HALT(I,I)* NOT 3 >>> 5. ~HALT(X,X) TRUE (THM) Peano 4 >>> 6. NO(X,X)v~HALT(X,X) UNION 1,5 >>> 7. ~YES(X,X) LIne 6 given CONS >>> qed >>> >>> -~YES(x,x) is the Incompleteness Axiom - more generally -~P/P where >>> general CBL is M # P / Q and the Theory of Computation is - X / YES : >>> output all non-r.e. sets. Also X / YES : Output all r.e. sets. >>> >>> -~YES(x,x) The set of programs that don't halt yes on themselves is >>> not r.e. >>> 1. ~YES(x,x) Premise >>> 2. M # ~YES(x,x) There must be a program that enumerates the set. >>> 3. YES(M,a) , ~YES(a,a) A1 expr => DEF (syntax) >>> 4. YES(M,M) , ~YES(M,M) SUB 3 >>> 5. P , ~P SUB 4 >>> qed >>> >>> -P,~P is a basic axiom. >>> >> Here is my closest approximation so far. >> >> // >> // To make the problem more clear we are assuming: >> // (a) a purely interpreted language >> // (b) function call syntax results in inline expansion, >> // thus specifying the name of a function specifies >> // the text body of the function. >> // >> >> >> void LoopIfHalts(string SourceCode) { >> if ( WillHalt(SourceCode, SourceCode) == TRUE ) >> while (TRUE) // loop forever >> ; >> else >> return; >> } >> >> >> int WillHalt(string SourceCode, string InputData) { >> if (NotValid(SourceCode, InputData)) >> throw(INVALID_INPUT); >> if ( TheProgramWillHalt(SourceCode, InputData) ) >> return TRUE; >> else >> return FALSE; >> } >> >> >> LoopIfHalts(LoopIfHalts); >> >> The INVALID_INPUT exception indicates that WillHalt() has detected a case of >> malignant self-reference where the result of its analysis is fed back into the >> analysis to change the result. This does not indicate that WillHalt() is unable >> to correctly derive the halt status of the universal set of programs. It only >> means that there exists at least one malignant case of self-reference where it >> can not provide the results of its correct and complete analysis as a return >> value. >> > > OK. And what's to prevent LoopIfHalts from using a nearly exact *copy* of > TheProgramWillHalt() in its implementation? There's an indefinite > number of modifications to a program that can be contemplated -- if > nothing else, one can assign an arbitrary number to an unused local > variable. > > But there are a fair number of other modification methods: loop > unrolling, variable name changes, using an int where a boolean > would be sufficient, exchanging leftshift and * or rightshift and /, > bitflipping > > v2 = v XOR 2^n > > versus > > if(floor(v / 2^n) mod 2 == 0) then v2 = v + 2^n; else v2 = v - 2^n; > > etc. > I was thinking of going a little further. Suppose the implementation language for LoopIfHalts is language X. Pick any TM-equivalent language Y. Write a language Y interpreter in X, and an X to Y compiler. LoopIfHalts gets fed as SourceCode the interpreter, bundled with the compiled version of LoopIfHalts as the interpreted program. Language Y could be designed after WillHalt has been written. The only information WillHalt gets about language Y is the language X implementation of a Y interpreter. Perhaps we should just stick to Turing machines? WillHalt has to able to deal with analyzing a TM program, because Turing machine is a possible language Y. Patricia
From: Paul E. Black on 18 Oct 2006 12:21 On Tuesday 17 October 2006 14:36, Peter Olcott wrote: > My primary point is based on the subtle distinction between your precise > statement of the conclusions that can be drawn from the HP, and the actual > correct conclusions that can actually be drawn. ... > > The HP does not show any limitation what-so-ever to the capability to > determine the halting status of any program. All that the HP shows ... In my personal experience I find that the unsolvability of the Halting Problem is a real limit (not just a problem in, say, definition) and that the theorem is useful. From time to time we would have trouble "writing" some powerful routines. We would think we had a solution, only to find we overlooked something, and we'd try to generalize to solve the *real* problem. Not infrequently after the second or third attempt, we'd ponder and realize that the problem was equivalent to solving the Halting Problem. With that we were satisfied with heuristics. Because of these experiences and the proofs I've seen, I am skeptical of purported solutions to the Halting Problem. True, the Halting Problem may be redefined such that there is a solution, but I've never found the redefined problem applicable in the real world. Sincerely, -paul- -- Paul E. Black (p.black(a)acm.org)
From: Dr A. N. Walker on 18 Oct 2006 12:24 In article <Jo9Zg.9173$eZ4.2688(a)dukeread06>, Peter Olcott <NoSpam(a)SeeScreen.com> wrote: >I thought that the "problem" part of the term "Halting Problem" was directly >referring to the existence of this case of malignant self-reference such that it >appears to defeat attempts to determine whether or not any program in the set of >all programs, halts. What you are calling "malignant self-reference" is nothing at all to do with the HP itself, nor with whether it is solvable, nor with the fact that it isn't. Rather, it arises in one specific proof that the HP is unsolvable. There are other ways to show the basic result, including a simple one based on the "busy beaver" idea. There is also no need for the HP to refer to programs *at all*; there is a simple equivalent formulation entirely in terms of data [eg as supplied to a UTM]. >The HP does not show any limitation what-so-ever to the capability to determine >the halting status of any program. The HP is merely a problem; as such it doesn't show anything at all. However, the proof that it is unsolvable does show a limitation; viz that there is no program that solves it. This is quite different from, for example, the syntax analysis problem, for it is quite usual for people to write syntax checkers, or the convex-hull-of-a-set-of- points-in-N-dimensions problem, or the search-data-for-a-specified-string problem, or many other potentially interesting problems. [But it is similar to many other interesting but, sadly, unsolvable problems.] > All that the HP shows is that there exists >some cases of malignant self-reference where this determination can not be >provided as a return value to a caller. No, it doesn't show that. No matter how MSR your program may be, there are programs out there that will show whether or not your program with its data will halt. But this is a game of "you show me yours and I'll show you mine". Given your program/data, I have a tester that will investigate it; but given my tester, you can write a program/data that busts it. It's important who is made to show his hand first. -- Andy Walker, School of MathSci., Univ. of Nott'm, UK. anw(a)maths.nott.ac.uk
From: MoeBlee on 18 Oct 2006 12:58 Peter Olcott wrote: > > Define 'self-referential', 'malignantly self-referential', > > 'self-modifying', and 'functioning correctly' as mathematical > > predicates in the theory (or a theory) of which the unsolvability of > > the halting probelm is a theorem. > > Let's start with just one, that will (hopefully) get us on the same page more > quickly: > [functioning correctly] would mean that a software function consistently > produces the results that it was designed to achieve. Yes, "software function consistencly produces the results that it was designed to achieve," is surely a rigorous mathematical definition. Reading that, I now realize I was entirely mistaken to doubt your complete expertise and profound grasp of the mathematics of this subject. MoeBlee
From: Chris Menzel on 18 Oct 2006 13:10
On Wed, 18 Oct 2006 12:21:08 -0400, Paul E. Black <p.black(a)acm.org> said: > > Because of these experiences and the proofs I've seen, I am skeptical > of purported solutions to the Halting Problem. It's definitely a good thing to be skeptical of purported solutions to provably unsolvable problems! > True, the Halting Problem may be redefined such that there is a > solution, You can't redefine the Halting Problem; it is what it is. The most you can do is decide to use the words "the Halting Problem" to mean some- thing other than what everyone else means by them. Many unsolvable problems have been "solved" in this manner in this newsgroup. :-) |