Path: ...!feed.opticnetworks.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: Re: Proof that DD correctly simulated by HH has different behavior than DD(DD) STEP(1)
Date: Tue, 11 Jun 2024 11:02:48 +0300
Organization: -
Lines: 88
Message-ID: <v490b8$v2i4$1@dont-email.me>
References: <v428vv$2no74$2@dont-email.me> <v43ib7$38hnd$1@dont-email.me> <v44da3$3i5jo$1@dont-email.me> <v46b4u$99o6$1@dont-email.me> <v474uv$ggn5$8@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 11 Jun 2024 10:02:49 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="6354b1c58f689f5eeabcf22981df2d90";
	logging-data="1018436"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+WoPBknmNUb3M89KSlu+9f"
User-Agent: Unison/2.2
Cancel-Lock: sha1:3be+vGreu5gRXmUejfLrB1c1poQ=
Bytes: 4279

On 2024-06-10 15:09:19 +0000, olcott said:

> On 6/10/2024 2:48 AM, Mikko wrote:
>> On 2024-06-09 14:13:23 +0000, olcott said:
>> 
>>> On 6/9/2024 1:33 AM, Fred. Zwarts wrote:
>>>> Op 08.jun.2024 om 20:47 schreef olcott:
>>>>> Before we can get to the behavior of the directly executed
>>>>> DD(DD) we must first see that the Sipser approved criteria
>>>>> have been met:
>>>>> 
>>>>> <MIT Professor Sipser agreed to ONLY these verbatim words 10/13/2022>
>>>>> 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.
>>>>> </MIT Professor Sipser agreed to ONLY these verbatim words10/13/2022>
>>>>> 
>>>>> On 10/14/2022 7:44 PM, Ben Bacarisse wrote:
>>>>>  > I don't think that is the shell game. PO really /has/ an H
>>>>>  > (it's trivial to do for this one case) that correctly determines
>>>>>  > that P(P) *would* never stop running *unless* aborted.
>>>>> 
>>>>> Try to show how this DD correctly simulated by any HH ever
>>>>> stops running without having its simulation aborted by HH.
>>>> 
>>>> Stopping at your first error. So, we can focus on it. Your are asking a 
>>>> question that contradicts itself.
>>>> A correct simulation of HH that aborts itself, should simulate up to 
>>>> the point where the simulated HH aborts. That is logically impossible. 
>>>> So, either it is a correct simulation and then we see that the 
>>>> simulated HH aborts and returns, or the simulation is incorrect, 
>>>> because it assumes incorrectly that things that happen (abort) do not 
>>>> happen.
>>>> A premature conclusion.
>>>> 
>>>> 
>>> 
>>> I have a clearer explanation now that I have gone through
>>> all of Mikko's posts: (you must know C to understand this)
>>> 
>>> typedef void (*ptr)(); // pointer to void function
>>> 
>>> void HHH(ptr P, ptr I)
>>> {
>>>    P(I);
>>>    return;
>>> }
>>> 
>>> void DDD(int (*x)())
>>> {
>>>    HHH(x, x);
>>>    return;
>>> }
>>> 
>>> int main()
>>> {
>>>    HHH(DDD,DDD);
>>> }
>>> 
>>> In the above Neither DDD nor HHH ever reach their own return
>>> statement thus never halt.
>>> 
>>> When HHH is a simulating halt decider then HHH sees that
>> 
>> As the code above shows, HHH is not a simulating halt decider:
>> (a) HHH does not simulate, (b) HHH does not decide.
>> Consequently, you are talking about nothing.
>> 
> 
> Yes that is correct. I begin with ordinary infinite recursion.
> If my reviewer does not understand that then they lack sufficient
> technical competence to review my work.
> 
> After they first understand infinite recursion then I show how
> infinite recursion is isomorphic to nested simulation.

To proove an isomorphism required much more effort that proving merely
what you need to prove. It is easier to prove a claim about recursive
calls and then transform that proof to a proof about nested simulation.
Other aspects of an isomorphism are not relevant so hardly worth of a
proof.

-- 
Mikko