Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald Knuth


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

<9FotK.137484$ntj.95074@fx15.iad>

  copy mid

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

  copy link   Newsgroups: comp.theory comp.ai.philosophy sci.logic sci.math
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx15.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; 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>
<A-2dnVjBk9RiKyj_nZ2dnUU7_8zNnZ2d@giganews.com>
<ae991ec7-edb8-4a8f-8461-b87ba83cdf62n@googlegroups.com>
<t94mff$8jv$1@dont-email.me>
<bab8ec9f-5d54-4399-bd07-58fdc239d783n@googlegroups.com>
<ePednUX7feSMeij_nZ2dnUU7_83NnZ2d@giganews.com>
<nfKdncxZra16dij_nZ2dnUU7_83NnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <nfKdncxZra16dij_nZ2dnUU7_83NnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 225
Message-ID: <9FotK.137484$ntj.95074@fx15.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Fri, 24 Jun 2022 15:55:48 -0400
X-Received-Bytes: 12314
 by: Richard Damon - Fri, 24 Jun 2022 19:55 UTC

On 6/24/22 12:52 PM, olcott wrote:
> On 6/24/2022 11:32 AM, olcott wrote:
>> On 6/24/2022 11:09 AM, Malcolm McLean wrote:
>>> On Friday, 24 June 2022 at 16:50:10 UTC+1, olcott wrote:
>>>> On 6/24/2022 8:34 AM, Malcolm McLean wrote:
>>>>> On Friday, 24 June 2022 at 14:07:19 UTC+1, olcott wrote:
>>>>>> On 6/24/2022 2:53 AM, Malcolm McLean wrote:
>>>>>>> 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.
>>>>>>
>>>>>> I already fully addressed that in my reply to you yesterday. P(P)
>>>>>> has a
>>>>>> dependency relationship on the return value of H(P,P) that the
>>>>>> correctly
>>>>>> emulated input to H(P,P) does not have. This changes their behavior
>>>>>> relative to each other.
>>>>>>
>>>>> I can see an alternative explanation. I was going to say "it is
>>>>> obvious" but
>>>>> no-one else has stepped in to point it out. Maybe because it's too
>>>>> obvious
>>>>> and they want to give other posters a chance.
>>>> To what exact extent do you have this mandatory prerequisite knowledge?
>>>> To fully understand this code a software engineer must be an expert in:
>>>> the C programming language, the x86 programming language, exactly how C
>>>> translates into x86 and the ability to recognize infinite recursion at
>>>> the x86 assembly language level.
>>>> 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 of P.
>>>> The halt decider and its input are written in C compiled with a
>>>> Microsoft C compiler that generates a standard COFF object file. This
>>>> file is the input to the x86utm operating system that runs on both
>>>> Microsoft Windows and Linux.
>>>>
>>> I'm a C programmer and I have done machine code programming, though not
>>> with the x86 chip. But I'd dispute your requirements.
>>
>>
>> THIS IS THE STIPULATED SOFTWARE ENGINEERING REQUIREMENTS THUS
>> DISAGREEMENT IS INHERENTLY INCORRECT.
>>
>>  From a purely software engineering perspective H is correctly defined
>> to correctly determine that its correct and complete x86 emulation of
>> its input would never reach the "ret" instruction of this input and it
>> is proven that H does do this correctly in a finite number of steps.
>>
>
> THIS IS THE STIPULATED SOFTWARE ENGINEERING REQUIREMENTS THUS
> DISAGREEMENT IS INHERENTLY INCORRECT.

STIPULTING that something is correct is inherently incorrect.

>
> 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.
>
> It is proven that H does meet this requirement.

No, because you said *ITS* correct and complete x86 emulation was
showing something when it didn't do one. Thus, H has FAILED to meet its
requirements.

Until you can show how H can do a COMPLETE emulation of a non-halting
input in finite time (not just 'prove' that it doesn't halt, that wasn't
the requrement, it was DO the emulation) your H just fails to meet you
software specifications for it.

Note, a Halt Decider isn't normally required to do a complete emulation
of its input, but that is because it isn't also the test of its answer
being correct, that is done by the INDEPENDENT running or complete
emulation of the input, which allow the decider to correct answer at
least some non-halting inputs. (Because it can find patterns that are
proven to be non-halting for the test machine).

Your removal of the allowance of a separate test operation, that CAN be
infinite in operation while the decider stays finite in operation dooms
your decider to either not meet its requriment to show non-halting, or
not meet its requirement to answer in finite time.

Note, your H fails to meet YOUR requirements when deciding on
Infinite_Loop, even though it can give the correct answer by the normal
requirements, because it never showed by its own complete and correct
emulation that the input doesn't halt (only by referencing another
emulation that does, which isn't YOUR stated requirement).
>
>
>>> To re-tread the analogy,
>>> our measurements show that tigers use more energy than they take in.
>>> Now you could construct an very complicated explanation for that using
>>> advanced quantum mechanics and other concepts. And you do need to have
>>> a rudimentary understanding of physics to see where the difficulty lies.
>>
>>> But you don't need more than the rudimentary understanding to suggest
>>> the
>>> alternative explanation, and to realise that it is overwhelmingly
>>> more likely.
>>
>> It seems that you may be saying that it is OK to disbelieve verified
>> facts some of the time. I vehemently disagree and this position could
>> cause both the end of Democracy in the USA and the extinction of
>> humanity in the world through lack of climate change action.
>>
>> Ordinary software engineering conclusively proves that all of my
>> claims that I just stated are easily verified as factually correct.
>>
>> Anyone that disagrees with claims that are verified as factually
>> correct is either insufficiently technically competent or less than
>> totally honest. Someone that refuses to acknowledge that claims are
>> correct when they know that these claims are correct is less than
>> totally honest.
>>
>> I believe that you are as honest as you can be and the issue is that
>> you have a lack of sufficient understanding.
>>
>
>

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.81
clearnet tor