Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

"Sometimes insanity is the only alternative" -- button at a Science Fiction convention.


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

<ndHtK.236184$70j.134397@fx16.iad>

  copy mid

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

  copy link   Newsgroups: comp.theory comp.ai.philosophy sci.logic sci.math
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer03.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>
<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>
<20220625162150.00002837@reddwarf.jmc>
<676dnb21wJs7sir_nZ2dnUU7_8zNnZ2d@giganews.com>
<20220625165919.0000287e@reddwarf.jmc>
<_K6dnVgtXJforyr_nZ2dnUU7_8xh4p2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <_K6dnVgtXJforyr_nZ2dnUU7_8xh4p2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 282
Message-ID: <ndHtK.236184$70j.134397@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 13:03:15 -0400
X-Received-Bytes: 15487
 by: Richard Damon - Sat, 25 Jun 2022 17:03 UTC

On 6/25/22 12:06 PM, olcott wrote:
> On 6/25/2022 10:59 AM, Mr Flibble wrote:
>> On Sat, 25 Jun 2022 10:54:13 -0500
>> olcott <NoOne@NoWhere.com> wrote:
>>
>>> On 6/25/2022 10:21 AM, Mr Flibble wrote:
>>>> On Sat, 25 Jun 2022 10:19:02 -0500
>>>> olcott <NoOne@NoWhere.com> 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.
>>>> Nope. Preventing a call to H is equivalent to H behaving differently
>>>> for same inputs. Aborting a simulation is a side effect: pure
>>>> functions do not have side effects.
>>>>
>>>> /Flibble
>>>
>>> In other words you are saying that a halt decider is simply not
>>> allowed to report when it correctly detects that it is being called
>>> in infinitely recursive simulation.
>>
>> I keep telling you this: the infinite recursion is NOT present when
>> using a valid halt decider: your H is NOT a valid halt
>> decider.
>>
>> Simulation is an erroneous approach as a simulating halt decider
>> can not answer in finite time for a non-halting input as there is no
>> proven general solution for detecting non-halting behaviour.
>>
>> /Flibble
>>
>
> IN OTHER WORDS THOROUGH LACK OF TECHNICAL COMPETANCE OR DISHONESTLY YOU
> DENY THIS VERIFIABLE FACT:
>
> 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.
>

SO?

H doesn't do a correct and complete x86 emulation of its input so the
statement doesn't apply.

H FALSELY ASSUMES that its copy will do this, so it is incorrect.

Either H is doing an INCORRECT emulation by that assumption, or H isn't
a pure function and behaving differently in different contexts.

Maybe we can't tell HOW H is wrong, becuase you don't give us enough
information, but it IS wrong, even by the nature of your definition.

Putting FALSE rules into you logic means you are working in a FALSE
logic system.

YOU FAIL.

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