Path: ...!2.eu.feeder.erje.net!feeder.erje.net!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 20:46:42 -0500
Organization: A noiseless patient Spider
Lines: 164
Message-ID: <v3lrm2$4h2j$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>
 <v3l002$5d3$1@dont-email.me>
 <lZadnYLpbtuB7cP7nZ2dnZfqn_udnZ2d@brightview.co.uk>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 04 Jun 2024 03:46:43 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="e82f76cbf70c4c740fdbf97a3b1eefca";
	logging-data="148563"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/vjK51ei/aqoAGmT1niJLo"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:TBNQvEogxRNPf4SMLQciNbb7x1Q=
In-Reply-To: <lZadnYLpbtuB7cP7nZ2dnZfqn_udnZ2d@brightview.co.uk>
Content-Language: en-US
Bytes: 9352

On 6/3/2024 8:38 PM, Mike Terry wrote:
> On 03/06/2024 18:54, olcott wrote:
>> 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.
> 
> An execution trace that is produced by a program that is incorrect 
> /proves/ nothing whatsoever.  I don't need to look at your proof, as I 
> was commenting on the value of your program output AS PROOF.
> 

I provided the execution trace that HH derives
*AND THE X86 SOURCE-CODE OF DD THAT PROVES THIS TRACE IS CORRECT*
*AND THE X86 SOURCE-CODE OF DD THAT PROVES THIS TRACE IS CORRECT*
*AND THE X86 SOURCE-CODE OF DD THAT PROVES THIS TRACE IS CORRECT*

http://al.howardknight.net/?STYPE=msgid&MSGI=%3CS8CcnRadHexfe8X7nZ2dnZfqnPqdnZ2d%40brightview.co.uk%3E+
Message-ID: <S8CcnRadHexfe8X7nZ2dnZfqnPqdnZ2d@brightview.co.uk>

AND YOU SAID
   "It shows that the simulation is "rubbish" and any trace
    produced by it can just be ignored."

-- 
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer