Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Ignorance is bliss. -- Thomas Gray Fortune updates the great quotes, #42: BLISS is ignorance.


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

<N9HtK.236183$70j.16465@fx16.iad>

  copy mid

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

  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!fx16.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; 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>
<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>
<878rplyhj6.fsf@bsb.me.uk>
<b6163094-01b0-4bb4-a3b1-4e48457527a0n@googlegroups.com>
<87fsjtwvut.fsf@bsb.me.uk>
<b2699d2d-40be-4e9b-9612-efb7121d5a8bn@googlegroups.com>
<t9637e$53p$1@dont-email.me>
<20edb990-f33e-4f3b-bc59-6cebf9f9def8n@googlegroups.com>
<wtidnY0ehdBiBiv_nZ2dnUU7_83NnZ2d@giganews.com>
<8328cb40-6b3c-4f89-a2ad-4054a6b466a6n@googlegroups.com>
<Jq2dnbDrVr_lhir_nZ2dnUU7_83NnZ2d@giganews.com>
<Jo2dnaO4cb0rvir_nZ2dnUU7_83NnZ2d@giganews.com>
<20220625160945.00006e9b@reddwarf.jmc>
<2umdnWsMdJX6uir_nZ2dnUU7_83NnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <2umdnWsMdJX6uir_nZ2dnUU7_83NnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 244
Message-ID: <N9HtK.236183$70j.16465@fx16.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Sat, 25 Jun 2022 12:59:25 -0400
X-Received-Bytes: 13032
 by: Richard Damon - Sat, 25 Jun 2022 16:59 UTC

On 6/25/22 11:19 AM, olcott wrote:
> On 6/25/2022 10:09 AM, Mr Flibble wrote:
>> On Sat, 25 Jun 2022 10:03:17 -0500
>> olcott <NoOne@NoWhere.com> wrote:
>>
>>> On 6/25/2022 9:28 AM, olcott wrote:
>>>> On 6/25/2022 2:32 AM, Malcolm McLean wrote:
>>>>> On Saturday, 25 June 2022 at 06:24:23 UTC+1, olcott wrote:
>>>>>> On 6/25/2022 12:09 AM, Malcolm McLean wrote:
>>>>>>> On Saturday, 25 June 2022 at 05:33:53 UTC+1, olcott wrote:
>>>>>>>> On 6/24/2022 11:01 PM, Malcolm McLean wrote:
>>>>>>>>> On Friday, 24 June 2022 at 23:16:30 UTC+1, Ben Bacarisse
>>>>>>>>> wrote:
>>>>>>>>>> Malcolm McLean <malcolm.ar...@gmail.com> writes:
>>>>>>>>>>> "Dry run" means that a human programmer looks at the code,
>>>>>>>>>>> and determines
>>>>>>>>>>> what it does, without actually executing it.
>>>>>>>>>>
>>>>>>>>>> Going back, now, to what you think needs to be resolved:
>>>>>>>>>> | 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.
>>>>>>>>>> The obvious conclusion is that PO's dry run (if he has indeed
>>>>>>>>>> done such
>>>>>>>>>> a thing) is incorrect.
>>>>>>>>> Exactly.
>>>>>>>>> We do our little energy budget on tigers, and find that tigers
>>>>>>>>> spend more energy
>>>>>>>>> than they take in. Well potentially this is dynamite. One
>>>>>>>>> explanation is that the
>>>>>>>>> law of conservation of energy is wrong.
>>>>>>>>> Except, before we countenance that explanation, we need to
>>>>>>>>> rule out a much
>>>>>>>>> simpler explanation. Which is that our measurements are wrong.
>>>>>>>>>
>>>>>>>>> Similarly, PO has worked out what he thinks P(P) should be
>>>>>>>>> doing, by dry-running
>>>>>>>>> it, and then actually run P(P) and obtained a different
>>>>>>>>> result. He also found that H
>>>>>>>>> agreed with the dry run. It's hard to paraphrase his
>>>>>>>>> conclusion, but it is extensive
>>>>>>>>> and far-reaching in its implications. The behaviour of code
>>>>>>>>> when run is different
>>>>>>>>> from the correct behaviour of the code when simulated. If
>>>>>>>>> that's true, then it has
>>>>>>>>> similar implications for computer science that disproving the
>>>>>>>>> conservation law
>>>>>>>>> has for physics.
>>>>>>>>>
>>>>>>>>> But the obvious explanation is that the dry-run was incorrect.
>>>>>>>>> Lots of people have
>>>>>>>>> suggested why it is incorrect. But they can't actually see the
>>>>>>>>> code. PO needs to
>>>>>>>>> understand that no-one will accept the complicated,
>>>>>>>>> far-reaching explanation,
>>>>>>>>> until the simple explanation has been ruled out.
>>>>>>>>
>>>>>>>> I already proved that the dry run is correct.
>>>>>>> Someone reports that tigers use more energy than they take in,
>>>>>>> and concludes that
>>>>>>> the energy conservation law is incorrect.
>>>>>>> Naturally, everyone is going to say "There must be some mistake.
>>>>>>> How were your
>>>>>>> measurements taken? Show us your calculations, maybe you've got
>>>>>>> your sums wrong."
>>>>>>>
>>>>>>> Now if they are also uncooperative about sharing the details of
>>>>>>> the investigation,
>>>>>>> those reservations will be magnified. There can be legitimate
>>>>>>> reasons. Tigers are
>>>>>>> rare and need to be conserved, you can't let anyone who wants
>>>>>>> have access to the
>>>>>>> tigers to try to repeat the measurements. But there's also a
>>>>>>> common illegitimate
>>>>>>> reason put forwards by people who make extraordinary claims. If
>>>>>>> the claims were
>>>>>>> unexceptional, such as that tigers have a similar energy budget
>>>>>>> to lions, then no-one
>>>>>>> would be saying "Show me your notebooks. How do you know that
>>>>>>> calorimeter was
>>>>>>> calibrated accurately? What's the name of the person who took
>>>>>>> that measurement
>>>>>>> and can I interview them?" Extraordinary claims are put through
>>>>>>> the wringer in a way
>>>>>>> that ordinary ones are not. I've seen complaints about this from
>>>>>>> parapsychologists.
>>>>>>> But if you're going to claim to have discovered a new physical
>>>>>>> principle, you need
>>>>>>> to present rock solid evidence.
>>>>>>>
>>>>>>> In this case, we can't see H. We can only suggest explanations
>>>>>>> for its behaviour.
>>>>>> It seems that you simply lack the technical competence.
>>>>>> Go back and look at my proof again.
>>>>> Sorry no. I've been programming since I was a boy and I have a PhD
>>>>> in a computational-
>>>>> related subject. I'm confident of my technical abilities. What I
>>>>> can't do of course
>>>>> is tell you exactly what is going on in code I cannot see. I've
>>>>> got a pretty good idea,
>>>>> but I can only reconstruct on the basis of what you tell me. Ben
>>>>> thinks that I've
>>>>> got it wrong and in fact there are no nested emulations at all.
>>>>> I've no way of actually
>>>>> disproving that idea without seeing H.
>>>>
>>>> To fully understand this a software engineer must be an expert in:
>>>> (a) The C programming language,
>>>> (b) The x86 programming language,
>>>> (c) Exactly how C translates into x86 and,
>>>> (d) The ability to recognize infinite recursion at the x86 assembly
>>>> language level.
>>>>
>>>> Anyone having the above credentials can validate my work, if you
>>>> cannot validate my work then you do not sufficiently have the above
>>>> credentials.
>>>>
>>>> Exactly how C translates into x86 is mandatory. If you don't know
>>>> how the C calling conventions are implemented in x86 you cannot
>>>> validate my work.
>>>>
>>>>   From a purely software engineering perspective H(P,P) is required
>>>> to to correctly determine that its correct and complete x86
>>>> emulation of its input would never reach the "ret" instruction of
>>>> this input and H must do this in a finite number of steps.
>>>>
>>>> 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
>>>> (final state) of this input thus never halts.
>>>>
>>>> The correct and complete x86 emulation of its input by H(P,P) would
>>>> never reach the "ret" instruction of P because both H and P would
>>>> remain stuck in infinitely nested emulation.
>>>>
>>>> void P(u32 x)
>>>> {
>>>>     if (H(x, x))
>>>>       HERE: goto HERE;
>>>>     return;
>>>> }
>>>>
>>>> int main()
>>>> {
>>>>     Output("Input_Halts = ", H((u32)P, (u32)P));
>>>> }
>>>>
>>>> _P()
>>>> [00001202](01)  55              push ebp
>>>> [00001203](02)  8bec            mov ebp,esp
>>>> [00001205](03)  8b4508          mov eax,[ebp+08]
>>>> [00001208](01)  50              push eax
>>>> [00001209](03)  8b4d08          mov ecx,[ebp+08]
>>>> [0000120c](01)  51              push ecx
>>>> [0000120d](05)  e820feffff      call 00001032
>>>> [00001212](03)  83c408          add esp,+08
>>>> [00001215](02)  85c0            test eax,eax
>>>> [00001217](02)  7402            jz 0000121b
>>>> [00001219](02)  ebfe            jmp 00001219
>>>> [0000121b](01)  5d              pop ebp
>>>> [0000121c](01)  c3              ret
>>>> Size in bytes:(0027) [0000121c]
>>>>
>>>> _main()
>>>> [00001222](01)  55              push ebp
>>>> [00001223](02)  8bec            mov ebp,esp
>>>> [00001225](05)  6802120000      push 00001202
>>>> [0000122a](05)  6802120000      push 00001202
>>>> [0000122f](05)  e8fefdffff      call 00001032
>>>> [00001234](03)  83c408          add esp,+08
>>>> [00001237](01)  50              push eax
>>>> [00001238](05)  68b3030000      push 000003b3
>>>> [0000123d](05)  e8c0f1ffff      call 00000402
>>>> [00001242](03)  83c408          add esp,+08
>>>> [00001245](02)  33c0            xor eax,eax
>>>> [00001247](01)  5d              pop ebp
>>>> [00001248](01)  c3              ret
>>>> Size in bytes:(0039) [00001248]
>>>>
>>>>    machine   stack     stack     machine    assembly
>>>>    address   address   data      code       language
>>>>    ========  ========  ========  =========  =============
>>>> [00001222][0010200f][00000000] 55         push ebp
>>>> [00001223][0010200f][00000000] 8bec       mov ebp,esp
>>>> [00001225][0010200b][00001202] 6802120000 push 00001202 // push P
>>>> [0000122a][00102007][00001202] 6802120000 push 00001202 // push P
>>>> [0000122f][00102003][00001234] e8fefdffff call 00001032 // call
>>>> executed H
>>>>
>>>> Begin Simulation   Execution Trace Stored at:2120c3
>>>> Address_of_H:1032
>>>> [00001202][002120af][002120b3] 55         push ebp
>>>> [00001203][002120af][002120b3] 8bec       mov ebp,esp
>>>> [00001205][002120af][002120b3] 8b4508     mov eax,[ebp+08]
>>>> [00001208][002120ab][00001202] 50         push eax      // push P
>>>> [00001209][002120ab][00001202] 8b4d08     mov ecx,[ebp+08]
>>>> [0000120c][002120a7][00001202] 51         push ecx      // push P
>>>> [0000120d][002120a3][00001212] e820feffff call 00001032 // 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.
>>>
>>> When you know that H simply implements the above algorithm there is
>>> no need to see its source code. I am reserving the publication of the
>>> 5 pages of the source code of the halt decider for journal
>>> publication.
>>
>> Your H is not a pure function as it behaves differently depending on
>> what is invoking it (it returns a decision answer to main() but not
>> to P()) and it has side effects (aborting a simulation).
>>
>> /Flibble
>>
>
> Finally a critique that has a reasonable basis.
>
> When I transformed H into a pure function of its inputs it always has
> the same behavior no matter how it is invoked.
>
> The x86 emulation of P is aborted before P invokes H.
>

Teny why doesn't it return the answer to P when P(P) is emulated?

Proof you LIE.

One H(P,P) return 0

One H(P,P) doesn't return.

DIFFERENT BEHAVIOR, BY DEFINITION not a pure function, or the emulation
isn't correct.

We need the code of H to tell you in which way your H is wrong.

Without it, all we can do is show you it is wrong.

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