Deutsch English Français Italiano |
<0xqdnd8ktrnsc8D7nZ2dnZfqnPqdnZ2d@brightview.co.uk> View for Bookmarking (what is this?) Look up another Usenet article |
Path: ...!Xl.tags.giganews.com!local-2.nntp.ord.giganews.com!nntp.brightview.co.uk!news.brightview.co.uk.POSTED!not-for-mail NNTP-Posting-Date: Mon, 03 Jun 2024 16:25:21 +0000 Subject: Re: Why does Olcott care about simulation, anyway? --- Mikes Review Newsgroups: comp.theory,sci.logic References: <v3j20v$3gm10$2@dont-email.me> <J_CdnTaA96jxpcD7nZ2dnZfqnPudnZ2d@brightview.co.uk> <v3jei1$3o3a7$1@dont-email.me> From: Mike Terry <news.dead.person.stones@darjeeling.plus.com> Date: Mon, 3 Jun 2024 17:25:21 +0100 User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Firefox/91.0 SeaMonkey/2.53.17 MIME-Version: 1.0 In-Reply-To: <v3jei1$3o3a7$1@dont-email.me> Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 8bit Message-ID: <0xqdnd8ktrnsc8D7nZ2dnZfqnPqdnZ2d@brightview.co.uk> Lines: 148 X-Usenet-Provider: http://www.giganews.com X-Trace: sv3-1v3GD99FTgon1hlwCMn7Zthzq17P5vbDIUhOT9irFnDsxLzQVG02BOYvz4Q7B5trnQVdanBjehJI9r1!vmQK1vTk4jG2Z0d33XQN0IVBBXGIf6g+EN5ArXBFGXPWH0MAaBYPAvLAE3G+VQYfCr0DW30Xj6+z!VwVZETQwXTi3kdYAnnr4vcIvkd2X X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.3.40 Bytes: 8711 On 03/06/2024 04:50, olcott wrote: > On 6/2/2024 10:28 PM, Mike Terry wrote: >> On 03/06/2024 01:16, immibis wrote: >>> The halting problem says you can't find a Turing machine that tells whether executing each other >>> Turing machine will halt. Simulation has nothing to do with the question. >> >> Background: >> >> PO claims to have refuted the common HP proof, e.g. as covered in the Linz book "An Introduction >> to Formal Languages and Automata". PO occasionally posts a link to a PDF containing an extract of >> the 5 or so pages of the book containing the proof, but I expect you have access to this or >> equivalent. >> >> In a nutshell, the proof goes: >> - Suppose H is a TM Halt decider that decides for any input <P><I> whether >> TM P run with input I on its input tape halts. >> [<P> is the string representation of the actual TM P, and >> <I> is the string representation of input tape I] >> - Construct from H a new TM H^ using the mechanical process described in the proof. >> If H exists, then its corresponding H^ also exists. >> - Show that the construction of H^ ensures that: >> - if H decides input <H^><H^> (representing H^ running with input <H^>) halts, >> then that implies that H^ running with input <H^> never halts >> - if H decides input <H^><H^> never halts, >> then that implies H^ running with input <H^> halts >> I.e. either way, H decides the specific input <H^><H^> incorrectly, contradicting >> the initial assumption that H is a halt decider. >> - So no halt decider exists. (Every proposed halt decider decides at least one input case >> incorrectly, viz input <H^><H^>.) >> >> PO basically claimed he had a fully coded TM H, which CORRECTLY decides its "nemesis" input >> <H^><H^>, contradicting the logic of the Linz proof [without pointing out any actual mistake in >> the Linz proof]. Given most people here understand the Linz proof well enough to see it is >> basically sound, people were sceptical! >> >> It turned out PO was lying about the fully coded TM, and in fact what he actually had was the idea >> behind a C program which would "prove" his idea. A couple of years(?) later he actually completed >> his C program and his x86utm.exe which would simulate the x86 code of his H and H^ to "prove" his >> claim. His equivalent of Linz H is his C function H or HH, and his equivalent of Linz H^ is his D >> or DD respectively. (They run under x86utm.exe and are not Windows/Unix executables.) >> >> H/HH use PARTIAL simulation of their input to decide halting/non-halting, returning >> 0 or 1 to communicate their decision. As you correctly point out, to the HP proof simulation is >> quite irrelevant, being just one kind of data manipulation that H may perform on its input string >> <P><I> before it decides the halting status. So the Linz HP proof covers such H, no problem. >> [I put PARTIAL in caps, just because there seems to be some confusion in recent threads as to what >> PO means by "simulation". He doesn't say it explicitly, despite suggestions to this effect, but >> he always means what might be called /partial/ simulation.] >> >> PO believes that by (partially) simulating the computation corresponding to the input <P><I> [i.e. >> calculating the successive x86 instruction steps of the computation P(I)] and monitoring the >> progress of virtual x86 state changes (like instruction address and op-code and so on) H could >> spot some pattern that reveals whether computation P(I) halts or not. At this point in the >> partial simulation, his H would stop simulating (aka "abort" the simulation) and return the >> appropriate halt status for input <P><I>. >> >> Nothing remarkable so far! Clearly a tight-loop in P /can/ be detected in this fashion, so /some/ >> <P><I> inputs /can/ be correctly determined like this. The PO claim however is that the specific >> input <H^><H^> is correctly decided by his H. In C terms those correspond to H(D,D) correctly >> returning the halt status of computation D(D). [PO would probably dispute this, because he >> doesn't properly understand halting or the HP generally, or in fact pretty much /any abstract >> concept/ ] >> > > Introduction to the Theory of Computation, by Michael Sipser > https://www.amazon.com/Introduction-Theory-Computation-Michael-Sipser/dp/113318779X/ > > On 10/13/2022 11:29:23 AM > MIT Professor Michael Sipser agreed this verbatim paragraph is correct > (He has neither reviewed nor agreed to anything else in this paper) > > <Professor Sipser agreed> > If simulating halt decider H correctly simulates its input D until H > correctly determines that its simulated D would never stop running > unless aborted then > > H can abort its simulation of D and correctly report that D specifies a > non-halting sequence of configurations. > </Professor Sipser agreed> > > I have started working on what seem to be some computability issues > that you pointed out with my HH. I found that they are isolated to > one single element of HH. Essentially the details of how the master > UTM directly executed HH passes a portion of its tape to its slaves. > > Nothing else seems to have any computability issues by the measure > that I am using. > > Message-ID: <rLmcnQQ3-N_tvH_4nZ2dnZfqnPGdnZ2d@brightview.co.uk> > On 3/1/2024 12:41 PM, Mike Terry wrote: > > > > Obviously a simulator has access to the internal state > > (tape contents etc.) of the simulated machine. No problem there. > > Because of your above comment it seems that correcting this > tiny computability issue with HH is my best path forward. > > > > > You have given the following a blatantly false review when I > said the same thing another way: I have no idea what you're talking about. I did not write any of what follows below. Also I don't believe I said anything "blatantly false". You're incapable of judging what other people say or are thinking - you're often telling people that they'er lying to you and denying "previously verified facts" etc. but its all rubbish - you're in no position to make such judgements. Mike. > > *We can see that the following DD cannot possibly halt when* > *correctly simulated by every HH that can possibly exist* > > typedef int (*ptr)(); // ptr is pointer to int function in C > 00 int HH(ptr p, ptr i); > 01 int DD(ptr p) > 02 { > 03 int Halt_Status = HH(p, p); > 04 if (Halt_Status) > 05 HERE: goto HERE; > 06 return Halt_Status; > 07 } > > _DD() > [00001c22] 55 push ebp > [00001c23] 8bec mov ebp,esp > [00001c25] 51 push ecx > [00001c26] 8b4508 mov eax,[ebp+08] > [00001c29] 50 push eax ; push DD 1c22 > [00001c2a] 8b4d08 mov ecx,[ebp+08] > [00001c2d] 51 push ecx ; push DD 1c22 > [00001c2e] e80ff7ffff call 00001342 ; call HH > [00001c33] 83c408 add esp,+08 > [00001c36] 8945fc mov [ebp-04],eax > [00001c39] 837dfc00 cmp dword [ebp-04],+00 > [00001c3d] 7402 jz 00001c41 > [00001c3f] ebfe jmp 00001c3f > [00001c41] 8b45fc mov eax,[ebp-04] > [00001c44] 8be5 mov esp,ebp > [00001c46] 5d pop ebp > [00001c47] c3 ret > Size in bytes:(0038) [00001c47] > >