Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

To downgrade the human mind is bad theology. -- C. K. Chesterton


computers / comp.ai.philosophy / Re: Technically competent Software engineers can verify this halting problem proof refutation

Re: Technically competent Software engineers can verify this halting problem proof refutation

<zfCdnUrEbbibVij_nZ2dnUU7_83NnZ2d@giganews.com>

  copy mid

https://www.novabbs.com/computers/article-flat.php?id=9739&group=comp.ai.philosophy#9739

  copy link   Newsgroups: comp.theory comp.ai.philosophy sci.logic sci.math
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Fri, 24 Jun 2022 09:32:37 -0500
Date: Fri, 24 Jun 2022 09:32:36 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.10.0
Subject: Re: Technically competent Software engineers can verify this halting
problem proof refutation
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,sci.logic,sci.math
References: <EOydnaeszcdfHS__nZ2dnUU7_83NnZ2d@giganews.com>
<PtvsK.300027$5fVf.158200@fx09.iad>
<CaWdnZEntLawFS__nZ2dnUU7_83NnZ2d@giganews.com>
<ccb8af3c-e497-4d6e-8040-826a4e87a6e7n@googlegroups.com>
<g9qdnRjZj9uBlS7_nZ2dnUU7_8zNnZ2d@giganews.com>
<0f7ed34c-5aaa-4858-885e-66e16777f599n@googlegroups.com>
<87a6a44s02.fsf@bsb.me.uk>
<a9adde1d-ad2c-444c-9b14-88841f5e8783n@googlegroups.com>
<87sfnv2e6e.fsf@bsb.me.uk>
<3a337f21-4828-46c4-b5be-87c76cff9db4n@googlegroups.com>
<A-2dnVjBk9RiKyj_nZ2dnUU7_8zNnZ2d@giganews.com>
<ae991ec7-edb8-4a8f-8461-b87ba83cdf62n@googlegroups.com>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <ae991ec7-edb8-4a8f-8461-b87ba83cdf62n@googlegroups.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <zfCdnUrEbbibVij_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 226
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-SFC3zGbtgsDmeeQbmSU8k2c7WqqhWzUftP1q0XB/BE0iWckec5el6XClT9t8X+jwo2EmjjJG0oJBE9k!x05iX13efQeU66LR8XG/YYBACoZSX15UYbltt7FnmB95BwTtVRbmquGIG4rVQYL9/dCOavqSIiPN
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: 12615
X-Received-Bytes: 12708
 by: olcott - Fri, 24 Jun 2022 14:32 UTC

On 6/24/2022 8:34 AM, Malcolm McLean wrote:
> On Friday, 24 June 2022 at 14:07:19 UTC+1, olcott wrote:
>> On 6/24/2022 2:53 AM, Malcolm McLean wrote:
>>> On Thursday, 23 June 2022 at 23:44:12 UTC+1, Ben Bacarisse wrote:
>>>> Malcolm McLean <malcolm.ar...@gmail.com> writes:
>>>>
>>>>> On Wednesday, 22 June 2022 at 16:50:31 UTC+1, Ben Bacarisse wrote:
>>>>>> Malcolm McLean <malcolm.ar...@gmail.com> writes:
>>>>>>
>>>>>>> On Wednesday, 22 June 2022 at 13:16:36 UTC+1, olcott wrote:
>>>>>>>> On 6/22/2022 2:55 AM, Malcolm McLean wrote:
>>>>>>>>> On Wednesday, 22 June 2022 at 04:10:45 UTC+1, olcott wrote:
>>>>>>>>>> On 6/21/2022 9:52 PM, Richard Damon wrote:
>>>>>>>>>>>
>>>>>>>>>>> Right, and P(P) reaches the ret instruction of H(P,P) returns 0, so H
>>>>>>>>>>> was incorrect in its mapping, since the behavior of P(P) is the
>>>>>>>>>>> DEFINITION of the behavior of H(P,P),
>>>>>>>>>> Linz and others were aware that: A halt decider must compute the mapping
>>>>>>>>>> from its inputs to an accept or reject state on the basis of the actual
>>>>>>>>>> behavior that is actually specified by these inputs.
>>>>>>>>>> Linz and others made the false assumption that the actual behavior that
>>>>>>>>>> is actually specified by the inputs to a simulating halt decider is not
>>>>>>>>>> the same as the direct execution of these inputs. They were unaware of
>>>>>>>>>> this because no one previously fully examined a simulating halt decider
>>>>>>>>>> ever before.
>>>>>>>>>>> especially if that is what P calls
>>>>>>>>>>> and P is claimed to be built by the Linz template.
>>>>>>>>>>>
>>>>>>>>>>> So, either P isn't built right, or H isn't built fight, or H is wrong.
>>>>>>>>>>
>>>>>>>>> You've dry-run P(P) and it doesn't halt. Additionally the halt decider H
>>>>>>>>> reports it as non-halting. So it's reasonable to assume that H is correct.
>>>>>>>>>
>>>>>>>>> However, when run, P(P) halts. So what are we to conclude? That "the
>>>>>>>>> actual behaviour that is actually specified by the inputs to a simulating
>>>>>>>>> halt decider is not the same as the direct execution of these inputs"?
>>>>>>>>
>>>>>>>> That is an actual immutable verified fact.
>>>>>>>>
>>>>>>> That's your conclusion from your observations and reasoning. You've
>>>>>>> dry-run P(P), and it doesn't halt. You've run H on P(P), and it
>>>>>>> reports "non-halting". You've run P(P), and it halts. So one
>>>>>>> explanation is the one you've given but, as I said, that explanation
>>>>>>> has rather far-reaching consequences.
>>>>>> There is only one explanation. What you call the "dry-run" is not that
>>>>>> same as the P(P). We've known this since the "line 15 commented out"
>>>>>> days. There are two computations -- one that is not stopped and one
>>>>>> that is, the "dry-run" and the run, the "simulation of the input to
>>>>>> H(P,P)" and P(P). All PO is doing is trying to find words that hide
>>>>>> what's going on.
>>>>>>
>>>>> I'm a scientists, not a mathematician.
>>>>> The example I always use is that you are doing an energy budget for tigers.
>>>>> You work how much they use on running about, lactating, maintaining their
>>>>> body temperature, and so on.
>>>>>
>>>>> Now let's say that you find that all results are within a few percentage points
>>>>> of a similar budget done for lions. You'd instantly accept this data.
>>>>>
>>>>> Now let's say that the results are wildly different from a previous budget done
>>>>> for lions. You wouldn't just accept that data. You'd check. You'd want to
>>>>> understand the reasons tigers spend far less energy on movement than lions.
>>>>>
>>>>> Now let's say that the result show that tigers use more energy than they
>>>>> take in food. Would you instantly conclude that the law of conservation of
>>>>> energy must be incorrect?
>>>>>
>>>>> The third is what PO is doing.
>>>> I have no idea what parts of this analogy map to the current situation.
>>>> PO has no contradictory results about anything. There's no conflict
>>>> with any established facts in anything he is doing.
>>>>
>>> He's dry-run P(P) and established that it doesn't halt. He's invoked H on it
>>> and H reports that it doesn't halt. He's run P(P) and it halts.
>>>
>>> So something odd is going on there that needs an explanation.
>>
>> I already fully addressed that in my reply to you yesterday. P(P) has a
>> dependency relationship on the return value of H(P,P) that the correctly
>> emulated input to H(P,P) does not have. This changes their behavior
>> relative to each other.
>>
> I can see an alternative explanation. I was going to say "it is obvious" but
> no-one else has stepped in to point it out. Maybe because it's too obvious
> and they want to give other posters a chance.

The provably correct execution trace proves that the complete and
correct x86 emulation of the input to H(P,P) by H would never reach the
"ret" instruction (final state) of P, thus never halts. It is also
proven that H does determine this in a finite number of states.

The provably correct execution trace of P(P) proves that the it halts.

Because it is a fact that the actual input to H(P,P) has actual behavior
that never halts then H must report on this behavior and cannot report
on any other behavior.

If you need to verify that you have a white dog in your living room
checking for a black cat in you kitchen is the wrong criteria.

If you need to verify that an input to a halt decider reaches its final
state it must be the actual behavior of this actual input. P(P) is
provably not the actual behavior of the actual input on the basis of the
ordinary semantics of the x86 language as shown in the two provably
correct execution traces.

To fully understand this code a software engineer must be an expert in:
the C programming language, the x86 programming language, exactly how C
translates into x86 and the ability to recognize infinite recursion at
the x86 assembly language level. No knowledge of the halting problem is
required.

The ordinary semantics of standard C and the conventional x86 language
are the entire semantics required to conclusively prove that H(P,P) does
correctly determine that its correct and complete x86 emulation of its
input would never reach the "ret" instruction of P.

In computer science terminology this means that complete and correct
emulation P by H would never reach its final state and halt.

The dependency relationship that P(P) has on H(P,P) causes its behavior
to be quite different than the complete and correct x86 emulation of the
input to H(P,P) that has no such dependency relationship.

As shown below because P(P) depends on the return value of H(P,P) it has
different behavior than the correctly emulated input to H(P,P).

The correctly emulated input to H(P,P) remains stuck in recursive
emulation that never gets to the point of receiving a return value from
H, thus lacks the dependency of the executed P(P).

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

int main()
{ P(P);
}

_P()
[000011f0](01) 55 push ebp
[000011f1](02) 8bec mov ebp,esp
[000011f3](03) 8b4508 mov eax,[ebp+08]
[000011f6](01) 50 push eax
[000011f7](03) 8b4d08 mov ecx,[ebp+08]
[000011fa](01) 51 push ecx
[000011fb](05) e820feffff call 00001020
[00001200](03) 83c408 add esp,+08
[00001203](02) 85c0 test eax,eax
[00001205](02) 7402 jz 00001209
[00001207](02) ebfe jmp 00001207
[00001209](01) 5d pop ebp
[0000120a](01) c3 ret
Size in bytes:(0027) [0000120a]

_main()
[00001210](01) 55 push ebp
[00001211](02) 8bec mov ebp,esp
[00001213](05) 68f0110000 push 000011f0
[00001218](05) e8d3ffffff call 000011f0
[0000121d](03) 83c404 add esp,+04
[00001220](02) 33c0 xor eax,eax
[00001222](01) 5d pop ebp
[00001223](01) c3 ret
Size in bytes:(0020) [00001223]

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
[00001210][00101fba][00000000] 55 push ebp
[00001211][00101fba][00000000] 8bec mov ebp,esp
[00001213][00101fb6][000011f0] 68f0110000 push 000011f0 // push P
[00001218][00101fb2][0000121d] e8d3ffffff call 000011f0 // call P
[000011f0][00101fae][00101fba] 55 push ebp // enter executed P
[000011f1][00101fae][00101fba] 8bec mov ebp,esp
[000011f3][00101fae][00101fba] 8b4508 mov eax,[ebp+08]
[000011f6][00101faa][000011f0] 50 push eax // push P
[000011f7][00101faa][000011f0] 8b4d08 mov ecx,[ebp+08]
[000011fa][00101fa6][000011f0] 51 push ecx // push P
[000011fb][00101fa2][00001200] e820feffff call 00001020 // call H

Begin Simulation Execution Trace Stored at:21206e
Address_of_H:1020
[000011f0][0021205a][0021205e] 55 push ebp // enter emulated P
[000011f1][0021205a][0021205e] 8bec mov ebp,esp
[000011f3][0021205a][0021205e] 8b4508 mov eax,[ebp+08]
[000011f6][00212056][000011f0] 50 push eax // push P
[000011f7][00212056][000011f0] 8b4d08 mov ecx,[ebp+08]
[000011fa][00212052][000011f0] 51 push ecx // push P
[000011fb][0021204e][00001200] e820feffff call 00001020 // call emulated H
Infinitely Recursive Simulation Detected Simulation Stopped

H knows its own machine address and on this basis it can easily
examine its stored execution_trace of P (see above) to determine:
(a) P is calling H with the same arguments that H was called with.
(b) No instructions in P could possibly escape this otherwise infinitely
recursive emulation.
(c) H aborts its emulation of P before its call to H is emulated.

[00001200][00101fae][00101fba] 83c408 add esp,+08 // return to
executed P
[00001203][00101fae][00101fba] 85c0 test eax,eax
[00001205][00101fae][00101fba] 7402 jz 00001209
[00001209][00101fb2][0000121d] 5d pop ebp
[0000120a][00101fb6][000011f0] c3 ret // return from
executed P
[0000121d][00101fba][00000000] 83c404 add esp,+04
[00001220][00101fba][00000000] 33c0 xor eax,eax
[00001222][00101fbe][00100000] 5d pop ebp
[00001223][00101fc2][00000000] c3 ret // ret from main
Number of Instructions Executed(878) / 67 = 13 pages

--
Copyright 2022 Pete Olcott

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

SubjectRepliesAuthor
o Technically competent Software engineers can verify this halting

By: olcott on Wed, 22 Jun 2022

158olcott
server_pubkey.txt

rocksolid light 0.9.81
clearnet tor