Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

The goal of science is to build better mousetraps. The goal of nature is to build better mice.


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

<sq-dnVRwmaVtpCv_nZ2dnUU7_8zNnZ2d@giganews.com>

  copy mid

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

  copy link   Newsgroups: comp.theory comp.ai.philosophy sci.logic sci.math
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Fri, 24 Jun 2022 17:25:52 -0500
Date: Fri, 24 Jun 2022 17:25:51 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; 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>
<PtvsK.300027$5fVf.158200@fx09.iad>
<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>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <87fsjtwvut.fsf@bsb.me.uk>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <sq-dnVRwmaVtpCv_nZ2dnUU7_8zNnZ2d@giganews.com>
Lines: 178
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-H6lMMivyz5PRCSrBiOcc2vlwcw3N27eVwIcJA+EuBHkSHq/xjLDwmj8bRcIEAy/uwuVOvqcvsu46tVL!0iITgNbcTTJmxoVlSSGdI0nDhxiSbBO0Pbsg7xKbSyefCbznpUOvz+TAuKZH29wrMxbmS62cLmut
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 10594
 by: olcott - Fri, 24 Jun 2022 22:25 UTC

On 6/24/2022 5:16 PM, Ben Bacarisse wrote:
> Malcolm McLean <malcolm.arthur.mclean@gmail.com> writes:
>
>> On Friday, 24 June 2022 at 20:42:56 UTC+1, Ben Bacarisse wrote:
>>> Malcolm McLean <malcolm.ar...@gmail.com> writes:
>>>
>>>> On Thursday, 23 June 2022 at 23:44:12 UTC+1, Ben Bacarisse wrote:
>>>>> Malcolm McLean <malcolm.ar...@gmail.com> writes:
>>>>>
>>>>>> On Wednesday, 22 June 2022 at 16:50:31 UTC+1, Ben Bacarisse wrote:
>>>>>>> Malcolm McLean <malcolm.ar...@gmail.com> writes:
>>>>>>>
>>>>>>>> On Wednesday, 22 June 2022 at 13:16:36 UTC+1, olcott wrote:
>>>>>>>>> On 6/22/2022 2:55 AM, Malcolm McLean wrote:
>>>>>>>>>> On Wednesday, 22 June 2022 at 04:10:45 UTC+1, olcott wrote:
>>>>>>>>>>> On 6/21/2022 9:52 PM, Richard Damon wrote:
>>>>>>>>>>>>
>>>>>>>>>>>> Right, and P(P) reaches the ret instruction of H(P,P) returns 0, so H
>>>>>>>>>>>> was incorrect in its mapping, since the behavior of P(P) is the
>>>>>>>>>>>> DEFINITION of the behavior of H(P,P),
>>>>>>>>>>> Linz and others were aware that: 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.
>>>>>>>>>>> Linz and others made the false assumption that the actual behavior that
>>>>>>>>>>> is actually specified by the inputs to a simulating halt decider is not
>>>>>>>>>>> the same as the direct execution of these inputs. They were unaware of
>>>>>>>>>>> this because no one previously fully examined a simulating halt decider
>>>>>>>>>>> ever before.
>>>>>>>>>>>> especially if that is what P calls
>>>>>>>>>>>> and P is claimed to be built by the Linz template.
>>>>>>>>>>>>
>>>>>>>>>>>> So, either P isn't built right, or H isn't built fight, or H is wrong.
>>>>>>>>>>>
>>>>>>>>>> You've dry-run P(P) and it doesn't halt. Additionally the halt decider H
>>>>>>>>>> reports it as non-halting. So it's reasonable to assume that H is correct.
>>>>>>>>>>
>>>>>>>>>> However, when run, P(P) halts. So what are we to conclude? That "the
>>>>>>>>>> actual behaviour that is actually specified by the inputs to a simulating
>>>>>>>>>> halt decider is not the same as the direct execution of these inputs"?
>>>>>>>>>
>>>>>>>>> That is an actual immutable verified fact.
>>>>>>>>>
>>>>>>>> That's your conclusion from your observations and reasoning. You've
>>>>>>>> dry-run P(P), and it doesn't halt. You've run H on P(P), and it
>>>>>>>> reports "non-halting". You've run P(P), and it halts. So one
>>>>>>>> explanation is the one you've given but, as I said, that explanation
>>>>>>>> has rather far-reaching consequences.
>>>>>>> There is only one explanation. What you call the "dry-run" is not that
>>>>>>> same as the P(P). We've known this since the "line 15 commented out"
>>>>>>> days. There are two computations -- one that is not stopped and one
>>>>>>> that is, the "dry-run" and the run, the "simulation of the input to
>>>>>>> H(P,P)" and P(P). All PO is doing is trying to find words that hide
>>>>>>> what's going on.
>>>>>>>
>>>>>> I'm a scientists, not a mathematician.
>>>>>> The example I always use is that you are doing an energy budget for tigers.
>>>>>> You work how much they use on running about, lactating, maintaining their
>>>>>> body temperature, and so on.
>>>>>>
>>>>>> Now let's say that you find that all results are within a few percentage points
>>>>>> of a similar budget done for lions. You'd instantly accept this data.
>>>>>>
>>>>>> Now let's say that the results are wildly different from a previous budget done
>>>>>> for lions. You wouldn't just accept that data. You'd check. You'd want to
>>>>>> understand the reasons tigers spend far less energy on movement than lions.
>>>>>>
>>>>>> Now let's say that the result show that tigers use more energy than they
>>>>>> take in food. Would you instantly conclude that the law of conservation of
>>>>>> energy must be incorrect?
>>>>>>
>>>>>> The third is what PO is doing.
>>>>> I have no idea what parts of this analogy map to the current situation.
>>>>> PO has no contradictory results about anything. There's no conflict
>>>>> with any established facts in anything he is doing.
>>>>>
>>>> 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.
>>>>
>>>> So something odd is going on there that needs an explanation.
>>> Then I don't know what you mean by "dry-run" and what needs an
>>> explanation (for me) is your description of what he's doing. Nothing in
>>> what PO is doing needs to be explained as far as I can see.
>>>
>> "Dry run" means that a human programmer looks at the code, and determines
>> what it does, without actually executing it.
>
> OK. So what value does it have in this case? Do you think PO is
> competent to "dry run" any code at all?
>
> 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. Anyone who eyeballs some case and concludes that
> it does not do what it down when actually run has just made a mistake.
> Do you think it's interesting to find out what mistake PO has made when
> guessing what the code does? If so have fun trying to get the code from
> him...
>
> The more interesting (at least at one time) is fact that H is not
> correct since, by definition, H(X,Y) should report on the "halting" of
> the call X(Y).
>
>> It's a very important technique, because it's not always practical or even
>> possible to run a debugger. Even where a debugger is available, often
>> dry-running will reveal bugs in a fraction of the time.
>
> In this case, we have the undisputed fact that P(P) halts, so there's
> really no value in a "dry run" from a debugging perspective.
>
>> In this case, PO has dry run P(P).
>
> And, if that is indeed what he's done (and I don't think it is) he knows
> he's made some mistake in his "dry run".
>
>> That is, he has looked at the source, and
>> worked out what it will do.
>
> But, I hope you agree, he's made some mistake or he's been lying when re
> reports that P(P) halts.
>
>> Which is to run an infinite sequence of nested
>> emulations. So it won't halt.
>
> The execution of P(P) does not represent an infinite sequence of nested
> simulations. We know that because P(P) halts.
>
>> H(P,P) also reports "non-halting". So this is
>> powerful evidence that H is correct.
>
> Eh? How is some code eyeballing more compelling evidence than the 100%
> undisputed fact that P(P) halts? How is the opinion of someone who
> can't write a parity checking TM powerful evidence of anything?
>
>> However when he actually executes P(P) on hardware, it terminates.
>> Something isn't right.
>
> Yes.
>
>> PO's explanation is that P(P) has different correct behaviour when run and
>> when emulated by H.
>
> That can't be an explanation of anything because, according to you, he
> is wrong about the dry run of P(P) and an actual run of P(P). Both the
> dry run and the actual run must take account of the fact that H is
> (partially) emulating P(P).
>
>> I can think of an obvious alternative explanation which is much
>> simpler and much less far-reaching in its implications. However
>> despite a lot of coaxing, no-one else seems to have arrived at it.
>
> There is nothing here with any far-reaching implications and since I've
> never shared your explanation, I'm not going to look for an alternative.
>
> I don't think he's done a "dry run" at all. He knows P(P) halts so he's
> relying on sophistry. H "aborts" so P never reaches its "ret"
> instruction. That's why P(P) and "the simulation of the inputs to
> H(P,P)" are different. 18 years of work for what? An H that, on the
> basis of his own words, obviously gets the wrong answer.
>

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.

That your understanding of the semantics of the x86 language is
insufficient to directly confirm this is less than no rebuttal at all.

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

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