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]
> 
>