Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

grep me no patterns and I'll tell you no lines.


computers / comp.ai.philosophy / Complete proof that H(P,P)==0 is correct for every simulating halt decider H

SubjectAuthor
* Complete proof that H(P,P)==0 is correct for every simulating haltolcott
`- Re: Complete proof that H(P,P)==0 is correct for every simulatingolcott

1
Subject: Complete proof that H(P,P)==0 is correct for every simulating halt decider H
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, sci.logic, sci.math
Date: Wed, 3 Nov 2021 23:14 UTC
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 03 Nov 2021 18:15:00 -0500
Date: Wed, 3 Nov 2021 18:14:59 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.2.1
Newsgroups: comp.theory,comp.ai.philosophy,sci.logic,sci.math
Content-Language: en-US
From: NoO...@NoWhere.com (olcott)
Subject: Complete proof that H(P,P)==0 is correct for every simulating halt
decider H
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <s7KdnUYxN6Npih78nZ2dnUU7-a_NnZ2d@giganews.com>
Lines: 71
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-oipOZUTtGxwXb29szqRpPPXv6fNjxHUaHZzmvh9jMFxUVDDp441/2SnAhN17ghDjEj0Ob4RKqkaLVy7!Z/7zVKS61nuUEXoLr8jn/8FwLA7TgfdlgGJihjkGasfhqGoNukIBi0VQId06QGypGmjB8YXbVCLn!Lw==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
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
X-Original-Bytes: 4126
View all headers
// Simplified Linz Ĥ (Linz:1990:319)
// Strachey(1965) CPL translated to C
void P(u32 x)
{
   if (H(x, x))
     HERE: goto HERE;
}

_P()
[00000c36](01)  55          push ebp
[00000c37](02)  8bec        mov ebp,esp
[00000c39](03)  8b4508      mov eax,[ebp+08] // 2nd Param
[00000c3c](01)  50          push eax
[00000c3d](03)  8b4d08      mov ecx,[ebp+08] // 1st Param
[00000c40](01)  51          push ecx
[00000c41](05)  e820fdffff  call 00000966    // call H
[00000c46](03)  83c408      add esp,+08
[00000c49](02)  85c0        test eax,eax
[00000c4b](02)  7402        jz 00000c4f
[00000c4d](02)  ebfe        jmp 00000c4d
[00000c4f](01)  5d          pop ebp
[00000c50](01)  c3          ret
Size in bytes:(0027) [00000c50]

Begin Local Halt Decider Simulation at Machine Address:c36

  machine   stack     stack     machine    assembly
  address   address   data      code       language
  ========  ========  ========  =========  =============
[00000c36][002117ca][002117ce] 55          push ebp
[00000c37][002117ca][002117ce] 8bec        mov ebp,esp
[00000c39][002117ca][002117ce] 8b4508      mov eax,[ebp+08]
[00000c3c][002117c6][00000c36] 50          push eax       // push P
[00000c3d][002117c6][00000c36] 8b4d08      mov ecx,[ebp+08]
[00000c40][002117c2][00000c36] 51          push ecx       // push P
[00000c41][002117be][00000c46] e820fdffff  call 00000966  // call H(P,P)

[00000c36][0025c1f2][0025c1f6] 55          push ebp
[00000c37][0025c1f2][0025c1f6] 8bec        mov ebp,esp
[00000c39][0025c1f2][0025c1f6] 8b4508      mov eax,[ebp+08]
[00000c3c][0025c1ee][00000c36] 50          push eax       // push P
[00000c3d][0025c1ee][00000c36] 8b4d08      mov ecx,[ebp+08]
[00000c40][0025c1ea][00000c36] 51          push ecx       // push P
[00000c41][0025c1e6][00000c46] e820fdffff  call 00000966  // call H(P,P)
Local Halt Decider: Infinite Recursion Detected Simulation Stopped

We can perfectly know that H(P,P) does precisely simulate the first seven instructions of P when it simulates the first seven instructions of P.

We can also know that when it perfectly repeats this sequence again that it has acted as a pure simulator for the execution of these two sequences.

That it is a pure simulator up to this point conclusively proves that
it is a pure simulator up to this point and conclusively proves that
a pure simulation would never halt.

2021-11-03 Update to Halt Decider Criteria
It is impossible for any halt decider to be incorrect when the correct pure simulation of its input never halts and it reports not halting.

Halting problem undecidability and infinitely nested simulation
May 2021 PL Olcott  (above is from pages 4 and 5)

https://www.researchgate.net/publication/351947980_Halting_problem_undecidability_and_infinitely_nested_simulation --
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: Complete proof that H(P,P)==0 is correct for every simulating halt decider H [ conclusive proof ]
From: olcott
Newsgroups: comp.theory, sci.logic, comp.ai.philosophy
Date: Thu, 4 Nov 2021 15:19 UTC
References: 1 2 3 4
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 04 Nov 2021 10:19:49 -0500
Date: Thu, 4 Nov 2021 10:19:48 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.2.1
Subject: Re: Complete proof that H(P,P)==0 is correct for every simulating
halt decider H [ conclusive proof ]
Content-Language: en-US
Newsgroups: comp.theory,sci.logic,comp.ai.philosophy
References: <s7KdnUYxN6Npih78nZ2dnUU7-a_NnZ2d@giganews.com>
<875yt8g6zv.fsf@bsb.me.uk> <dfOdnW5sOr8H-x78nZ2dnUU7-XfNnZ2d@giganews.com>
<72PgJ.13861$6a3.12306@fx41.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <72PgJ.13861$6a3.12306@fx41.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <v_GdnYjv-KiIZx78nZ2dnUU7-QvNnZ2d@giganews.com>
Lines: 84
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-p43WIu+xIFGW04di3+xXhsILi+hesAFwBvdfxxihGNx3Esy6vU46O2bteXMPkX6mFi6CANQwgmOK3KJ!FnQhkkVf2FeudESpm0b7GK19uZWsnB8Si24JZbIXmJoz8X0OFdZLLXgApHHuSorcVzq5Aut7zloL!Vg==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
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
X-Original-Bytes: 4834
View all headers
On 11/4/2021 5:59 AM, Richard Damon wrote:
On 11/4/21 12:50 AM, olcott wrote:
On 11/3/2021 6:21 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

void P(u32 x)
{
   if (H(x, x))
     HERE: goto HERE;
}

But H(P,P) == 0 is not correct if P(P) halts and you have told us that
both are the case (for the specific H you are touting).  That false is
the wrong return for inputs that represent halting computations comes
from the definition of the problem you claim to be addressing.


I provided all of the details to prove that I am correct and you simply ignored and erased them. This is apparently because you realized that my proof is irrefutable thus realize any attempt at rebuttal could only seem foolish. Alternatively you are clueless about the x86 language.


Except that you 'proof' is totally baseless since it is built on false assumptions.

_P()
[00000c36](01)  55          push ebp
[00000c37](02)  8bec        mov ebp,esp
[00000c39](03)  8b4508      mov eax,[ebp+08] // 2nd Param
[00000c3c](01)  50          push eax
[00000c3d](03)  8b4d08      mov ecx,[ebp+08] // 1st Param
[00000c40](01)  51          push ecx
[00000c41](05)  e820fdffff  call 00000966    // call H
[00000c46](03)  83c408      add esp,+08
[00000c49](02)  85c0        test eax,eax
[00000c4b](02)  7402        jz 00000c4f
[00000c4d](02)  ebfe        jmp 00000c4d
[00000c4f](01)  5d          pop ebp
[00000c50](01)  c3          ret
Size in bytes:(0027) [00000c50]

Begin Local Halt Decider Simulation at Machine Address:c36

  machine   stack     stack     machine    assembly
  address   address   data      code       language
  ========  ========  ========  =========  =============
[00000c36][002117ca][002117ce] 55          push ebp
[00000c37][002117ca][002117ce] 8bec        mov ebp,esp
[00000c39][002117ca][002117ce] 8b4508      mov eax,[ebp+08]
[00000c3c][002117c6][00000c36] 50          push eax       // push P
[00000c3d][002117c6][00000c36] 8b4d08      mov ecx,[ebp+08]
[00000c40][002117c2][00000c36] 51          push ecx       // push P
[00000c41][002117be][00000c46] e820fdffff  call 00000966  // call H(P,P)

[00000c36][0025c1f2][0025c1f6] 55          push ebp
[00000c37][0025c1f2][0025c1f6] 8bec        mov ebp,esp
[00000c39][0025c1f2][0025c1f6] 8b4508      mov eax,[ebp+08]
[00000c3c][0025c1ee][00000c36] 50          push eax       // push P
[00000c3d][0025c1ee][00000c36] 8b4d08      mov ecx,[ebp+08]
[00000c40][0025c1ea][00000c36] 51          push ecx       // push P
[00000c41][0025c1e6][00000c46] e820fdffff  call 00000966  // call H(P,P)

Verified facts:
(1) The above 14 simulated lines are a correct pure simulation of P(P) for every possible encoding of simulating halt decider H.

(2) The above 14 simulated lines conclusively prove that the pure simulation of the input to H(P,P) would never reach its final state of c50 for every possible encoding of simulating halt decider H.

(1) and (2) conclusively prove that H(P,P) meets this criteria:

2021-11-03 Halt Deciding Criteria
It is impossible for any halt decider to be incorrect when the correct pure simulation of its input never halts and it reports not halting.


--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


1
rocksolid light 0.7.2
clearneti2ptor