Path: ...!news.mixmin.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: Re: Why do people here insist on denying these verified facts?
Date: Thu, 27 Jun 2024 10:02:54 +0300
Organization: -
Lines: 187
Message-ID: <v5j2qu$2kgmo$1@dont-email.me>
References: <v56n8h$3pr25$1@dont-email.me> <v56ntj$onl3$7@i2pn2.org> <v56ps2$3q4ea$1@dont-email.me> <v56sk3$p1du$2@i2pn2.org> <v56tfv$3ql1v$2@dont-email.me> <v570n5$onl4$11@i2pn2.org> <v571lc$3rrgk$1@dont-email.me> <v57603$onl3$12@i2pn2.org> <v576cg$3soh6$2@dont-email.me> <v576nv$onl3$14@i2pn2.org> <v5775h$3soh6$5@dont-email.me> <v58r5s$9j01$1@dont-email.me> <v597og$brmn$3@dont-email.me> <v5b7cm$qtn6$1@dont-email.me> <v5btmn$v0vb$6@dont-email.me> <v5e3df$1gco9$1@dont-email.me> <v5egoe$1ikpr$4@dont-email.me> <v5ggmi$21nkc$1@dont-email.me> <v5h1bo$24jbd$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 27 Jun 2024 09:02:54 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="d7b27c8cdba91f30a1cc0e0727f68863";
	logging-data="2769624"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+pobr3AjSWLA3L29JzOSMt"
User-Agent: Unison/2.2
Cancel-Lock: sha1:CvzMmOIy06yJB6OwsFcwJuxtOBU=
Bytes: 8989

On 2024-06-26 12:25:28 +0000, olcott said:

> On 6/26/2024 2:41 AM, Mikko wrote:
>> On 2024-06-25 13:29:50 +0000, olcott said:
>> 
>>> On 6/25/2024 4:42 AM, Mikko wrote:
>>>> On 2024-06-24 13:52:23 +0000, olcott said:
>>>> 
>>>>> On 6/24/2024 2:31 AM, Mikko wrote:
>>>>>> On 2024-06-23 13:25:36 +0000, olcott said:
>>>>>> 
>>>>>>> On 6/23/2024 4:50 AM, Mikko wrote:
>>>>>>>> On 2024-06-22 19:03:13 +0000, olcott said:
>>>>>>>> 
>>>>>>>>> On 6/22/2024 1:55 PM, Richard Damon wrote:
>>>>>>>>>> On 6/22/24 2:49 PM, olcott wrote:
>>>>>>>>>>> On 6/22/2024 1:43 PM, Richard Damon wrote:
>>>>>>>>>>>> On 6/22/24 1:29 PM, olcott wrote:
>>>>>>>>>>>>> On 6/22/2024 12:13 PM, Richard Damon wrote:
>>>>>>>>>>>>>> On 6/22/24 12:18 PM, olcott wrote:
>>>>>>>>>>>>>>> 
>>>>>>>>>>>>>>> void DDD()
>>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>>    HHH0(DDD);
>>>>>>>>>>>>>>> }
>>>>>>>>>>>>>>> 
>>>>>>>>>>>>>>> The input to HHH0(DDD) includes itself.
>>>>>>>>>>>>>>> The input to HHH1(DDD) DOES NOT include itself.
>>>>>>>>>>>>>>> 
>>>>>>>>>>>>>>> It is stipulated that correct emulation is defined by the
>>>>>>>>>>>>>>> semantics of the x86 programming language and nothing else.
>>>>>>>>>>>>>> 
>>>>>>>>>>>>>> And thus, your emulation traces show that your "Simulating Halt 
>>>>>>>>>>>>>> Deciders" do not do a "Correct Simulation"
>>>>>>>>>>>>> 
>>>>>>>>>>>>> Apparently your ADD preventing you from paying close attention
>>>>>>>>>>>>> to ALL of my words.
>>>>>>>>>>>>> 
>>>>>>>>>>>>> *Function names adapted to correspond to my updated paper*
>>>>>>>>>>>>> 
>>>>>>>>>>>>> void DDD()
>>>>>>>>>>>>> {
>>>>>>>>>>>>>    H0(DDD);
>>>>>>>>>>>>> }
>>>>>>>>>>>>> 
>>>>>>>>>>>>> *When we stipulate that the only measure of a correct*
>>>>>>>>>>>>> *emulation is the semantics of the x86 programming language*
>>>>>>>>>>>>> 
>>>>>>>>>>>>> *When we stipulate that the only measure of a correct*
>>>>>>>>>>>>> *emulation is the semantics of the x86 programming language*
>>>>>>>>>>>>> 
>>>>>>>>>>>>> *When we stipulate that the only measure of a correct*
>>>>>>>>>>>>> *emulation is the semantics of the x86 programming language*
>>>>>>>>>>>>> 
>>>>>>>>>>>>> *When we stipulate that the only measure of a correct*
>>>>>>>>>>>>> *emulation is the semantics of the x86 programming language*
>>>>>>>>>>>>> 
>>>>>>>>>>>>> *When we stipulate that the only measure of a correct*
>>>>>>>>>>>>> *emulation is the semantics of the x86 programming language*
>>>>>>>>>>>>> 
>>>>>>>>>>>>> then we see that when DDD is correctly emulated by H0 that
>>>>>>>>>>>>> its call to H0(DDD) cannot possibly return.
>>>>>>>>>>>> 
>>>>>>>>>>>> Since your H0 has never demonstrated that is actually DOES the correct 
>>>>>>>>>>>> simulation per your stipulation,
>>>>>>>>>>> 
>>>>>>>>>>> Liar
>>>>>>>>>>> 
>>>>>>>>>> 
>>>>>>>>>> Then where is it?
>>>>>>>>>> 
>>>>>>>>> When we stipulate that the only measure of a correct emulation
>>>>>>>>> is the semantics of the x86 programming language then we see that
>>>>>>>>> when DDD is correctly emulated by H0 that its call to H0(DDD)
>>>>>>>>> cannot possibly return.
>>>>>>>> 
>>>>>>>> Semantics of the x86 programming language does not specifiy emulation
>>>>>>>> or correctness of emulation.
>>>>>>>> 
>>>>>>> 
>>>>>>> WRONG!
>>>>>> 
>>>>>> Unless you point where in Intel's documentation emulation or correctness
>>>>>> of emulation is specified you have no basis to say "WRONG".
>>>>>> 
>>>>> 
>>>>> Not at all. That is the same as saying that 2 + 3 = 5
>>>>> is wrong until proven by PA.
>>>> 
>>>> If you want to claim that 2 + 3 = 5 you must show some basis for the claim.
>>>> One obvious source of such basis is Peano Arithmetic. Likewise, if you say
>>>> "WRONG" you must show some basis for the claim. When the statement claimed
>>>> "WRONG" is about x86 programming language, an sobvious source for such basis
>>>> is Intel's documentation.
>>>> 
>>>>>>> Otherwise we could say that for the decimal integers
>>>>>>> 2 + 3 = 17 and the semantics of arithmetic does not disagree.
>>>> 
>>>> No, you can only say that you don't know any disageement between them.
>>>> Without a proof threse is a possibility of an unknown disagreement.
>>>> 
>>>>>> I can believe you couls but I would not.
>>>>>> 
>>>>>>> The semantics of arithmetic agrees that for the decimal
>>>>>>> integers 2 + 3 = 5.
>>>>>> 
>>>>>> Intel's processors seem to agree, too. But I havn't checked every one.
>>>>> 
>>>>> _DDD()
>>>>> [00002172] 55               push ebp      ; housekeeping
>>>>> [00002173] 8bec             mov ebp,esp   ; housekeeping
>>>>> [00002175] 6872210000       push 00002172 ; push DDD
>>>>> [0000217a] e853f4ffff       call 000015d2 ; call H0(DDD)
>>>>> [0000217f] 83c404           add esp,+04
>>>>> [00002182] 5d               pop ebp
>>>>> [00002183] c3               ret
>>>>> Size in bytes:(0018) [00002183]
>>>>> 
>>>>> The call from DDD to H0(DDD) when DDD is correctly emulated
>>>>> by H0 cannot possibly return.
>>>> 
>>>> What is shown above does not prove that the call to 15d3 does not
>>>> return, nor whether there is H0 or HHH0 or something else at that
>>>> location.
>>>> 
>>> 
>>> It is stipulated that DDD is correctly emulated by the
>>> H0 at machine address 000015d2.
>> 
>> There is no such stipulation in the above text. The C code specifies
>> and a comment in the machine code claims that H0 is called but don't
>> say what H0 does.
>> 
>>> It is stipulated the the correct simulation is ruled by
>>> the semantics of the x86 programming language.
>> 
>> That does not fully define "correct simulation" but may specify enough
>> of it to contradict the previous stipulation.
>> 
>>> *This conclusively proves*
>>> The call from DDD to H0(DDD) when DDD is correctly emulated
>>> by H0 *CANNOT POSSIBLY RETURN*
>> 
>> It proves nothing if no proof is shown.
>> 
> 
> I will use your system of reasoning.
> The semantics of decimal arithmetic prove that 2 + 3 = 5.

You nave not shown the proof.

> Your reply
> Aritmetic has no semantics and there is no such thing as numbers

There is the standard semantics of Peano arithmetic and various other
arithmetics. You have not proven that there is no such thing as numbers.
Whether that is provable depends on the exact meanings of "there is" and
"such" and "numbers". These (and many other) vernacular words are fuzzy.

>>> I am unwilling to talk about anything else with you until
>>> you agree to this.
>> 
>> Unlikely to ever happen, especially about stipulations.
> 
> _DDD()
> [00002172] 55               push ebp      ; housekeeping
> [00002173] 8bec             mov ebp,esp   ; housekeeping
> [00002175] 6872210000       push 00002172 ; push DDD
> [0000217a] e853f4ffff       call 000015d2 ; call H0(DDD)
> [0000217f] 83c404           add esp,+04
> [00002182] 5d               pop ebp
> [00002183] c3               ret
> Size in bytes:(0018) [00002183]
> 
> For every x86 emulator H0 at machine address 0000217a
> The call from DDD to H0(DDD) when DDD is correctly emulated
> by H0 cannot possibly return is proven correct by the semantics
> of the x86 programming language.

Proofs about machine language programs tend to be long as one must
prove about every instruction at least that it does not invalidate
========== REMAINDER OF ARTICLE TRUNCATED ==========