Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

From Sharp minds come... pointed heads. -- Bryan Sparrowhawk


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

<20220626204304.00006847@reddwarf.jmc>

  copy mid

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

  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!peer02.ams4!peer.am4.highwinds-media.com!news.highwinds-media.com!fx04.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: <20220626204304.00006847@reddwarf.jmc>
References: <EOydnaeszcdfHS__nZ2dnUU7_83NnZ2d@giganews.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>
<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>
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: 296
X-Complaints-To: abuse@eweka.nl
NNTP-Posting-Date: Sun, 26 Jun 2022 19:43:01 UTC
Date: Sun, 26 Jun 2022 20:43:04 +0100
X-Received-Bytes: 14659
 by: Mr Flibble - Sun, 26 Jun 2022 19:43 UTC

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

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