Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Before Xerox, five carbons were the maximum extension of anybody's ego.


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

<20220625201230.00000c34@reddwarf.jmc>

  copy mid

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

  copy link   Newsgroups: comp.theory comp.ai.philosophy sci.logic sci.math
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!newsreader4.netcologne.de!news.netcologne.de!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer03.ams4!peer.am4.highwinds-media.com!news.highwinds-media.com!fx01.ams4.POSTED!not-for-mail
From: flib...@reddwarf.jmc (Mr Flibble)
Newsgroups: comp.theory,comp.ai.philosophy,sci.logic,sci.math
Subject: Re: Technically competent Software engineers can verify this
halting problem proof refutation
Message-ID: <20220625201230.00000c34@reddwarf.jmc>
References: <EOydnaeszcdfHS__nZ2dnUU7_83NnZ2d@giganews.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>
<20220625172518.00002fb8@reddwarf.jmc>
<S8udnWfpo60QpSr_nZ2dnUU7_8xh4p2d@giganews.com>
Organization: Jupiter Mining Corp
X-Newsreader: Claws Mail 3.17.8 (GTK+ 2.24.33; x86_64-w64-mingw32)
MIME-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Lines: 354
X-Complaints-To: abuse@eweka.nl
NNTP-Posting-Date: Sat, 25 Jun 2022 19:12:26 UTC
Date: Sat, 25 Jun 2022 20:12:30 +0100
X-Received-Bytes: 18023
 by: Mr Flibble - Sat, 25 Jun 2022 19:12 UTC

On Sat, 25 Jun 2022 11:32:12 -0500
olcott <NoOne@NoWhere.com> wrote:

> On 6/25/2022 11:25 AM, Mr Flibble wrote:
> > On Sat, 25 Jun 2022 11:06:12 -0500
> > olcott <NoOne@NoWhere.com> 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.
> >
> > For [Strachey 1965] (and the proofs based on it) H is NOT a
> > simulating halt decider so there is no infinite recursion as there
> > is no emulation.
> >
> > Valid halt deciders ANALYSE P, they do not EMULATE P.
> >
> > /Flibble
> >
>
> I provide a halt decider H that gets the right answer and your
> rebuttal is that H does not get the right answer because there is
> another different halt decider named H1 that gets the wrong answer.
Your H also gets the wrong answer:

void Px(u32 x)
{ H(x, x);
return;
}

int main()
{ Output("Input_Halts = ", H((u32)Px, (u32)Px));
}

....[000013e8][00102357][00000000] 83c408 add esp,+08
....[000013eb][00102353][00000000] 50 push eax
....[000013ec][0010234f][00000427] 6827040000 push 00000427
---[000013f1][0010234f][00000427] e880f0ffff call 00000476
Input_Halts = 0
....[000013f6][00102357][00000000] 83c408 add esp,+08
....[000013f9][00102357][00000000] 33c0 xor eax,eax
....[000013fb][0010235b][00100000] 5d pop ebp
....[000013fc][0010235f][00000004] c3 ret
Number of Instructions Executed(16120)

It gets the answer wrong, i.e. input has not been decided correctly.
QED.

/Flibble

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