Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: olcott <polcott333@gmail.com>
Newsgroups: comp.theory,sci.logic
Subject: Re: Why does Olcott care about simulation, anyway? --- Mikes Review
Date: Mon, 3 Jun 2024 12:54:10 -0500
Organization: A noiseless patient Spider
Lines: 182
Message-ID: <v3l002$5d3$1@dont-email.me>
References: <v3j20v$3gm10$2@dont-email.me>
 <J_CdnTaA96jxpcD7nZ2dnZfqnPudnZ2d@brightview.co.uk>
 <v3jei1$3o3a7$1@dont-email.me>
 <0xqdnd8ktrnsc8D7nZ2dnZfqnPqdnZ2d@brightview.co.uk>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 03 Jun 2024 19:54:10 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="f629d257ac302b24ac32e99a4ff4b1b3";
	logging-data="5539"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/q2fGkByrGfT8DJwNP2iGJ"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:OrJOxH55AFi7/Urk3CmsjeC9mOc=
In-Reply-To: <0xqdnd8ktrnsc8D7nZ2dnZfqnPqdnZ2d@brightview.co.uk>
Content-Language: en-US
Bytes: 9492

On 6/3/2024 11:25 AM, Mike Terry wrote:
> 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.
> 

You said that the execution trace that I proved is correct is
incorrect because you didn't like the way that HH was written.
You said this without looking at my proof as you are doing
here again.

> 
>>
>> *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]
>>
========== REMAINDER OF ARTICLE TRUNCATED ==========