Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

The moon is a planet just like the Earth, only it is even deader.


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

<frudnQE7VPOLCyv_nZ2dnUU7_83NnZ2d@giganews.com>

  copy mid

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

  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 23:59:02 -0500
Date: Fri, 24 Jun 2022 23:59:00 -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> <sq-dnVRwmaVtpCv_nZ2dnUU7_8zNnZ2d@giganews.com>
<d4d1011f-c7d4-4dba-b5f7-5747c5b01d10n@googlegroups.com>
<196dnYFoP-efziv_nZ2dnUU7_8zNnZ2d@giganews.com>
<fab45955-7bf3-48db-9b97-dc68eb3eb884n@googlegroups.com>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <fab45955-7bf3-48db-9b97-dc68eb3eb884n@googlegroups.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <frudnQE7VPOLCyv_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 218
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-JSSOscUTK8QmsRvQNmxEOX5EbrptxD+wde2rDnNc1M2nMqrZoyem1Ohzl60VTfOpPvn4QnjiPoDOo9r!tdD2IODI4G38VM8WWbSLNuggcgTGM3nUENqes/AHZPqbirlOmY1XBNZVeKlKBSu3tD5utj5FiV0F
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: 13287
 by: olcott - Sat, 25 Jun 2022 04:59 UTC

On 6/24/2022 11:50 PM, dklei...@gmail.com wrote:
> On Friday, June 24, 2022 at 5:12:57 PM UTC-7, olcott wrote:
>> On 6/24/2022 6:58 PM, dklei...@gmail.com wrote:
>>> On Friday, June 24, 2022 at 3:25:59 PM UTC-7, olcott wrote:
>>>> On 6/24/2022 5:16 PM, Ben Bacarisse wrote:
>>>>> Malcolm McLean <malcolm.ar...@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.
>>>
>>> I assume the semantics of C are defined by the 1989 Standard. The
>>> semantics of x86 assembly language are described (not actually
>>> authoritatively defined) in other documents. The mapping of C onto
>>> the assembly language is far from unique (every compiler could be
>>> different) PO appears to using a version of Microsoft's C# compiler.
>>>
>> The COFF object file generated by most any Microsoft C compiler.
>> I used Visual Studio 2017 Community Edition.
>>
>> x86 Instruction Set Reference: https://c9x.me/x86/
>>> Then we must define how a Turing machine is emulated by a C
>>> program. All that is needed of C is the struct concept and
>>> assignment. In that case using C seems unadvisable.
>>>
>> No we don't need this at all. We only need to know that a C function
>> that is a pure function of its inputs is Turing equivalent.
>>
>> https://en.wikipedia.org/wiki/Pure_function
>
> You are jumping too far in one step. What I am asking is equivalent to:
> Given a Turing Machine how do its steps map into C and thence into x86?
> No C functions are involved.
>

I have written this up several ways that boil down to C maps to a RASP
machine that maps to a TM.
https://en.wikipedia.org/wiki/Random-access_stored-program_machine

The bottom line is that when a C function is a pure function of its
inputs then it is TM equivalent computation.

>> By not using C my five page halt decider becomes hundreds of thousands
>> of indecipherable pages of TM description.
>
> That would depend on the answer to my question.

--
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