Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

APL hackers do it in the quad.


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

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

<20220626211525.0000424c@reddwarf.jmc>

  copy mid

https://www.novabbs.com/computers/article-flat.php?id=34974&group=comp.theory#34974

  copy link   Newsgroups: comp.theory comp.ai.philosophy sci.logic sci.math
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!news.szaf.org!news.uzoreto.com!peer03.ams4!peer.am4.highwinds-media.com!news.highwinds-media.com!fx05.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: <20220626211525.0000424c@reddwarf.jmc>
References: <EOydnaeszcdfHS__nZ2dnUU7_83NnZ2d@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>
<87k094uwkw.fsf@bsb.me.uk>
<SbudnW2JfoTdICr_nZ2dnUU7_83NnZ2d@giganews.com>
<20220626030328.00007922@reddwarf.jmc>
<R8WdnXqc7LIHqCX_nZ2dnUU7_83NnZ2d@giganews.com>
<20220626121534.00007e30@reddwarf.jmc>
<xridnT9kGf5GFSX_nZ2dnUU7_83NnZ2d@giganews.com>
<20220626200003.00005a2f@reddwarf.jmc>
<g66dneEaUuTaMiX_nZ2dnUU7_83NnZ2d@giganews.com>
<20220626202610.000048d3@reddwarf.jmc>
<3cOdnZP4Ka8cKCX_nZ2dnUU7_83NnZ2d@giganews.com>
<20220626204304.00006847@reddwarf.jmc>
<qsadnZNWDrXtJCX_nZ2dnUU7_8zNnZ2d@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: 335
X-Complaints-To: abuse@eweka.nl
NNTP-Posting-Date: Sun, 26 Jun 2022 20:15:22 UTC
Date: Sun, 26 Jun 2022 21:15:25 +0100
X-Received-Bytes: 16279
 by: Mr Flibble - Sun, 26 Jun 2022 20:15 UTC

On Sun, 26 Jun 2022 14:54:22 -0500
olcott <NoOne@NoWhere.com> wrote:

> On 6/26/2022 2:43 PM, Mr Flibble wrote:
> > On Sun, 26 Jun 2022 14:37:36 -0500
> > olcott <NoOne@NoWhere.com> wrote:
> >
> >> On 6/26/2022 2:26 PM, Mr Flibble wrote:
> >>> On Sun, 26 Jun 2022 14:11:02 -0500
> >>> olcott <NoOne@NoWhere.com> wrote:
> >>>
> >>>> On 6/26/2022 2:00 PM, Mr Flibble wrote:
> >>>>> On Sun, 26 Jun 2022 11:27:06 -0500
> >>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>
> >>>>>> On 6/26/2022 6:15 AM, Mr Flibble wrote:
> >>>>>>> On Sun, 26 Jun 2022 05:31:53 -0500
> >>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>
> >>>>>>>> On 6/25/2022 9:03 PM, Mr Flibble wrote:
> >>>>>>>>> On Sat, 25 Jun 2022 20:58:23 -0500
> >>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>
> >>>>>>>>>> On 6/25/2022 6:55 PM, Ben Bacarisse wrote:
> >>>>>>>>>>> Malcolm McLean <malcolm.arthur.mclean@gmail.com> writes:
> >>>>>>>>>>>
> >>>>>>>>>>>> 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.
> >>>>>>>>>>>
> >>>>>>>>>>> Obviously.
> >>>>>>>>>>>
> >>>>>>>>>>>> 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.
> >>>>>>>>>>>
> >>>>>>>>>>> He is just waffling. There is no conclusion, just a
> >>>>>>>>>>> constant twisting and turning to find some why to persuade
> >>>>>>>>>>> people that the wrong answer is the right one. He's being
> >>>>>>>>>>> doing this for years with various degrees of obfuscation.
> >>>>>>>>>>>
> >>>>>>>>>>> H does not report the correct result for P(P) and PO is
> >>>>>>>>>>> putting up anything he can think of to keep the discussion
> >>>>>>>>>>> going. It should simply have stopped once he'd been clear
> >>>>>>>>>>> that H(P,P) == 0 is correct "even though P(P) halts" but
> >>>>>>>>>>> the traces and the verbiage is keeping people keen.
> >>>>>>>>>>>> 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.
> >>>>>>>>>>>
> >>>>>>>>>>> When a student comes to me and says that her program to
> >>>>>>>>>>> add 5 and 6 gives 12, I don't, even for a moment, imagine
> >>>>>>>>>>> that the laws of logic and mathematics are in doubt.
> >>>>>>>>>>>
> >>>>>>>>>>>> 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.
> >>>>>>>>>>>
> >>>>>>>>>>> For what it's worth, I don't think there is any "dry run"
> >>>>>>>>>>> going on here at all. PO decide years ago that H(H_Hat,
> >>>>>>>>>>> H_Hat) would be 0 because he knew (correctly) that H could
> >>>>>>>>>>> spot what would happen if H did not "intervene".
> >>>>>>>>>>> Everything since then -- the "it only halt because...",
> >>>>>>>>>>> the "it wouldn't halt if line 15 were commented out" and
> >>>>>>>>>>> the rather less explicitly stated "H_Hat does not get to
> >>>>>>>>>>> its ret instruction because a non top-level H aborts" are
> >>>>>>>>>>> just the various attempt at after-the-fact justification.
> >>>>>>>>>>>
> >>>>>>>>>>> I agree it's never quite so simple because PO is usually
> >>>>>>>>>>> fractally wrong, so he's not correct about almost
> >>>>>>>>>>> everything he says at almost every level. For example,
> >>>>>>>>>>> at one level he now admits that a halt decider is
> >>>>>>>>>>> impossible because H(X,Y) must report "on its input" and
> >>>>>>>>>>> the call X(Y) is not an input! He did this to explain why
> >>>>>>>>>>> H(P,P) is permitted to return 0 "even though P(P) halts",
> >>>>>>>>>>> but it also makes it clear that what he one thought was
> >>>>>>>>>>> that halting problem is not solvable.
> >>>>>>>>>>
> >>>>>>>>>> YOU KNOW THAT THIS IS TRUE
> >>>>>>>>>> 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.
> >>>>>>>>>>
> >>>>>>>>>> BECAUSE THIS IS PROVABLY TRUE
> >>>>>>>>>> P(P) is provably not the actual behavior of the actual
> >>>>>>>>>> input.
> >>>>>>>>>>
> >>>>>>>>>> YOU ARE THE ONE FUDGING WITH THE TRUTH
> >>>>>>>>>
> >>>>>>>>> The issue is what constitutes a pathological input: the
> >>>>>>>>> pathological input at issue here are YOUR PATHOLOGICAL LIES,
> >>>>>>>>> Olcott.
> >>>>>>>>>
> >>>>>>>>> /Flibble
> >>>>>>>>>
> >>>>>>>>
> >>>>>>>> Computable functions are the basic objects of
> >>>>>>>> study in computability theory.
> >>>>>>>> Computable functions are the formalized analogue of
> >>>>>>>> the intuitive notion of
> >>>>>>>> algorithms, in the sense that a function is
> >>>>>>>> computable if there exists an algorithm
> >>>>>>>> that can do the job of the function, i.e. given an
> >>>>>>>> input of the function domain it
> >>>>>>>> can return the corresponding output.
> >>>>>>>> https://en.wikipedia.org/wiki/Computable_function
> >>>>>>>>
> >>>>>>>> void P(u32 x)
> >>>>>>>> {
> >>>>>>>> if (H(x, x))
> >>>>>>>> HERE: goto HERE;
> >>>>>>>> return;
> >>>>>>>> }
> >>>>>>>>
> >>>>>>>> int main()
> >>>>>>>> {
> >>>>>>>> Output("Input_Halts = ", H((u32)P, (u32)P));
> >>>>>>>> }
> >>>>>>>>
> >>>>>>>> That you reject that the above proves that H and P have a
> >>>>>>>> pathological relationship to each other seem to be your lack
> >>>>>>>> of technical competence rather than dishonesty.
> >>>>>>>
> >>>>>>> There is nothing wrong with my technical competence however
> >>>>>>> yours *is* suspect.
> >>>>>>>
> >>>>>>> Nobody is denying that P is pathological input as its comes
> >>>>>>> from [Strachey, 1965]'s "Impossible Program";
> >>>>>>
> >>>>>> // rec routine P
> >>>>>> // §L :if T[P] go to L
> >>>>>> // Return §
> >>>>>> // https://academic.oup.com/comjnl/article/7/4/313/354243
> >>>>>> void Strachey_P()
> >>>>>> {
> >>>>>> L:if (T(Strachey_P))
> >>>>>> goto L;
> >>>>>> return;
> >>>>>> }
> >>>>>>
> >>>>>> int main()
> >>>>>> {
> >>>>>> Output("Input_Halts = ", T(Strachey_P));
> >>>>>> }
> >>>>>>
> >>>>>> _Strachey_P()
> >>>>>> [000015b2](01) 55 push ebp
> >>>>>> [000015b3](02) 8bec mov ebp,esp
> >>>>>> [000015b5](05) 68b2150000 push 000015b2 // push
> >>>>>> Strachey_P [000015ba](05) e813fdffff call 000012d2 //
> >>>>>> call T [000015bf](03) 83c404 add esp,+04
> >>>>>> [000015c2](02) 85c0 test eax,eax
> >>>>>> [000015c4](02) 7402 jz 000015c8
> >>>>>> [000015c6](02) ebed jmp 000015b5
> >>>>>> [000015c8](01) 5d pop ebp
> >>>>>> [000015c9](01) c3 ret
> >>>>>> Size in bytes:(0024) [000015c9]
> >>>>>>
> >>>>>> _main()
> >>>>>> [000015d2](01) 55 push ebp
> >>>>>> [000015d3](02) 8bec mov ebp,esp
> >>>>>> [000015d5](05) 68b2150000 push 000015b2 // push
> >>>>>> Strachey_P [000015da](05) e8f3fcffff call 000012d2 //
> >>>>>> call T [000015df](03) 83c404 add esp,+04
> >>>>>> [000015e2](01) 50 push eax
> >>>>>> [000015e3](05) 6833040000 push 00000433
> >>>>>> [000015e8](05) e895eeffff call 00000482
> >>>>>> [000015ed](03) 83c408 add esp,+08
> >>>>>> [000015f0](02) 33c0 xor eax,eax
> >>>>>> [000015f2](01) 5d pop ebp
> >>>>>> [000015f3](01) c3 ret
> >>>>>> Size in bytes:(0034) [000015f3]
> >>>>>>
> >>>>>> machine stack stack machine assembly
> >>>>>> address address data code language
> >>>>>> ======== ======== ======== ========= ============> >>>>>> [000015d2][001025c6][00000000] 55 push ebp
> >>>>>> [000015d3][001025c6][00000000] 8bec mov ebp,esp
> >>>>>> [000015d5][001025c2][000015b2] 68b2150000 push 000015b2 // push
> >>>>>> Strachey_P [000015da][001025be][000015df] e8f3fcffff call
> >>>>>> 000012d2 // call T
> >>>>>>
> >>>>>> Begin Simulation Execution Trace Stored at:21267a
> >>>>>> Address_of_T:12d2
> >>>>>> [000015b2][0021266a][0021266e] 55 push ebp
> >>>>>> [000015b3][0021266a][0021266e] 8bec mov ebp,esp
> >>>>>> [000015b5][00212666][000015b2] 68b2150000 push 000015b2 // push
> >>>>>> Strachey_P [000015ba][00212662][000015bf] e813fdffff call
> >>>>>> 000012d2 // call T Infinitely Recursive Simulation Detected
> >>>>>> Simulation Stopped
> >>>>>>
> >>>>>> T knows its own machine address and on this basis it can easily
> >>>>>> examine its stored execution_trace of Strachey_P (see above) to
> >>>>>> determine: (a) Strachey_P is calling T with the same arguments
> >>>>>> that T was called with. (b) No instructions in Strachey_P could
> >>>>>> possibly escape this otherwise infinitely recursive emulation.
> >>>>>>
> >>>>>
> >>>>> There is no recursion in [Strachey, 1965] or the proofs based on
> >>>>> it that you are attempting to refute. Fail.
> >>>>>
> >>>>> /Flibble
> >>>>>
> >>>>
> >>>> In other words you are saying that because a non-simulating halt
> >>>> decider (that has no recursive emulation) cannot correctly
> >>>> determine the halt status of its input that a simulating halt
> >>>> decider (that has recursive emulation) cannot correctly determine
> >>>> the halt status of its input.
> >>>
> >>> We have already established that your simulating halt decider gets
> >>> the answer wrong if P calls H but isn't pathological.
> >>>
> >>
> >> We have not established that at all.
> >
> > Yes we have:
> >
> > 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)
> >
> > As can be seen above Olcott's H decides that Px does not halt but
> > it is obvious that Px should always halt if H is a valid halt
> > decider that always returns a decision to its caller (Px).
> > Olcott's H does not return a decision to its caller (Px) and is
> > thus invalid.
> >> H1(P,P)==1 is the non-pathological instance.
> >
> > See above.
> >
> >>
> >>>>
> >>>> In other words if there are no black dogs in the kitchen this
> >>>> proves that there are no white cats in the living room.
> >>>
> >>> You are the one trying to redefine H to be something else.
> >>>
> >>> /Flibble
> >>>
> >>
> >> Not something else at all.
> >>
> >> It is merely the case that no one besides me every bothered to
> >> fully investigate the effects of applying a simulating halt
> >> decider to the wide open (any pure function of its inputs will do)
> >> specification of the halting problem proofs.
> >
> > A simulating halt decider is invalid as it cannot return an answer
> > of non-halting in finite time for all non-halting inputs as there
> > is no proven algorithm that can detect non-halting behaviour for
> > the general case.
> >
> > /Flibble
> >
> >
>
> We are back to your lack of sufficient software engineering skill.
> You still don't understand that everything after P's function call to
> H(P,P) is unreachable by P from:
>
> int main()
> {
> Output("Input_Halts = ", H1((u32)P, (u32)P));
> }
>
> This means that erasing the infinite loop can have no effect.
> Here is the actual non-pathological input to H1(P,P):
>
> void P(u32 x)
> {
> if (H(x, x))
> HERE: goto HERE;
> return;
> }
>
> int main()
> {
> Output("Input_Halts = ", H1((u32)P, (u32)P));
> }
>
> H1(P,P)==1.
The only reason erasing the infinite loop has no effect is because your
H aborts the simulation which is an invalid thing to do.

/Flibble

SubjectRepliesAuthor
o Technically competent Software engineers can verify this halting

By: olcott on Wed, 22 Jun 2022

211olcott
server_pubkey.txt

rocksolid light 0.9.8
clearnet tor