Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

God requireth not a uniformity of religion. -- Roger Williams


devel / comp.theory / Re: Concise refutation of halting problem proofs V5 [Linz version]

SubjectAuthor
* Concise refutation of halting problem proofs V5olcott
+* Concise refutation of halting problem proofs V5Ben Bacarisse
|+* Concise refutation of halting problem proofs V5olcott
||+* Concise refutation of halting problem proofs V5Richard Damon
|||`* Concise refutation of halting problem proofs V5olcott
||| `- Concise refutation of halting problem proofs V5Richard Damon
||+* Concise refutation of halting problem proofs V5dklei...@gmail.com
|||`* Concise refutation of halting problem proofs V5olcott
||| `* Concise refutation of halting problem proofs V5dklei...@gmail.com
|||  `* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   +* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   |+* Concise refutation of halting problem proofs V5 [Linz version]Richard Damon
|||   ||+* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   |||+* Concise refutation of halting problem proofs V5 [Linz version]Malcolm McLean
|||   ||||+* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   |||||+* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   ||||||`* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   |||||| `* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   ||||||  `* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   ||||||   `* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   ||||||    `- Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   |||||`- Concise refutation of halting problem proofs V5 [Linz version]Richard Damon
|||   ||||`- Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   |||+* Concise refutation of halting problem proofs V5 [Linz version]Andy Walker
|||   ||||+* Concise refutation of halting problem proofs V5 [ logicalolcott
|||   |||||`- Concise refutation of halting problem proofs V5 [ logicalRichard Damon
|||   ||||`* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   |||| `* Concise refutation of halting problem proofs V5 [Linz version]Andy Walker
|||   ||||  +* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   ||||  |`- Concise refutation of halting problem proofs V5 [Linz version]Mike Terry
|||   ||||  `- Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   |||`* Concise refutation of halting problem proofs V5 [Linz version]Richard Damon
|||   ||| `* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   |||  `* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   |||   `- Concise refutation of halting problem proofs V5 [Linz version]Richard Damon
|||   ||`* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   || +* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   || |`* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   || | `* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   || |  `* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   || |   `* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   || |    `* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   || |     `* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   || |      `* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   || |       `* Concise refutation of halting problem proofs V5 [Linz version]dklei...@gmail.com
|||   || |        `* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   || |         `* Concise refutation of halting problem proofs V5 [Linz version]André G. Isaak
|||   || |          `* Concise refutation of halting problem proofs V5 [ logical necessity ](POE)olcott
|||   || |           `* Concise refutation of halting problem proofs V5 [ logicalAndré G. Isaak
|||   || |            `* Concise refutation of halting problem proofs V5 [ logicalolcott
|||   || |             +- Concise refutation of halting problem proofs V5 [ logicalRichard Damon
|||   || |             +* Concise refutation of halting problem proofs V5 [ logicalAndré G. Isaak
|||   || |             |`* Concise refutation of halting problem proofs V5 [ logicalolcott
|||   || |             | `* Concise refutation of halting problem proofs V5 [ logicalAndré G. Isaak
|||   || |             |  +* Concise refutation of halting problem proofs V5 [ logicalolcott
|||   || |             |  |+- Concise refutation of halting problem proofs V5 [ logicalAndré G. Isaak
|||   || |             |  |`- Concise refutation of halting problem proofs V5 [ logicalRichard Damon
|||   || |             |  `* Logical Necessity and the Principle of Explosionolcott
|||   || |             |   +- Logical Necessity and the Principle of ExplosionRichard Damon
|||   || |             |   `* Logical Necessity and the Principle of ExplosionAndré G. Isaak
|||   || |             |    `* Logical Necessity and the Principle of Explosionolcott
|||   || |             |     +- Logical Necessity and the Principle of ExplosionRichard Damon
|||   || |             |     `* Logical Necessity and the Principle of ExplosionAndré G. Isaak
|||   || |             |      `* Logical Necessity and the Principle of Explosionolcott
|||   || |             |       `- Logical Necessity and the Principle of ExplosionAndré G. Isaak
|||   || |             `- Concise refutation of halting problem proofs V5 [ logicalMalcolm McLean
|||   || `- Concise refutation of halting problem proofs V5 [Linz version]Richard Damon
|||   |`* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   | `* Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   |  `* Concise refutation of halting problem proofs V5 [Linz version]olcott
|||   |   `- Concise refutation of halting problem proofs V5 [Linz version]Ben Bacarisse
|||   `- Concise refutation of halting problem proofs V5 [Linz version]Richard Damon
||`* Concise refutation of halting problem proofs V5Ben Bacarisse
|| `* Concise refutation of halting problem proofs V5olcott
||  `- Concise refutation of halting problem proofs V5Ben Bacarisse
|`* Concise refutation of halting problem proofs V5 (Linz version)olcott
| +- Concise refutation of halting problem proofs V5 (Linz version)Ben Bacarisse
| `- Concise refutation of halting problem proofs V5 (Linz version)Richard Damon
`- Concise refutation of halting problem proofs V5Richard Damon

Pages:1234
Concise refutation of halting problem proofs V5

<QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>

 copy mid

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

 copy link   Newsgroups: comp.theory comp.ai.philosophy sci.logic sci.math
Followup: comp.theory
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!news.uzoreto.com!tr2.eu1.usenetexpress.com!feeder.usenetexpress.com!tr2.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Tue, 09 Nov 2021 08:52:50 -0600
Date: Tue, 9 Nov 2021 08:52:48 -0600
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Thunderbird/91.3.0
Newsgroups: comp.theory,comp.ai.philosophy,sci.logic,sci.math
Content-Language: en-US
From: NoO...@NoWhere.com (olcott)
Subject: Concise refutation of halting problem proofs V5
Followup-To: comp.theory
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
Lines: 77
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-ltWaIQd9C8n0ReF4I0hmtH1ubzqoOBHpnI/bhEyoCvhy4hIcGMsCs6AJM9YdY4iUQbIXDHcLLCDrPPO!QfmWB8+4Ac4SHSVfRu5y4NS/LkhBWtUsWG2FioSsBNH6DZvRVDcPjghynjKfJv7cKSipZ5DW5Mt7!tA==
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: 3609
 by: olcott - Tue, 9 Nov 2021 14:52 UTC

// Simplified Linz Ĥ (Linz:1990:319)
// Strachey(1965) CPL translated to C
void P(u32 x)
{ if (H(x, x))
HERE: goto HERE;
}

_P()
[00000c36](01) 55 push ebp
[00000c37](02) 8bec mov ebp,esp
[00000c39](03) 8b4508 mov eax,[ebp+08] // 2nd Param
[00000c3c](01) 50 push eax
[00000c3d](03) 8b4d08 mov ecx,[ebp+08] // 1st Param
[00000c40](01) 51 push ecx
[00000c41](05) e820fdffff call 00000966 // call H
[00000c46](03) 83c408 add esp,+08
[00000c49](02) 85c0 test eax,eax
[00000c4b](02) 7402 jz 00000c4f
[00000c4d](02) ebfe jmp 00000c4d
[00000c4f](01) 5d pop ebp
[00000c50](01) c3 ret
Size in bytes:(0027) [00000c50]

Begin Local Halt Decider Simulation at Machine Address:c36

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
[00000c36][002117ca][002117ce] 55 push ebp
[00000c37][002117ca][002117ce] 8bec mov ebp,esp
[00000c39][002117ca][002117ce] 8b4508 mov eax,[ebp+08]
[00000c3c][002117c6][00000c36] 50 push eax // push P
[00000c3d][002117c6][00000c36] 8b4d08 mov ecx,[ebp+08]
[00000c40][002117c2][00000c36] 51 push ecx // push P
[00000c41][002117be][00000c46] e820fdffff call 00000966 // call H(P,P)

Because P calls H(P,P) P specifies infinitely nested simulation to every
simulating halt decider H.

This has been verified with the execution trace of a correct pure
simulation of P.

Whether or not H aborts its simulation P never reaches its final state
therefore the simulated P never halts.

If the simulated P never halts then H(P,P)==0 is always correct for
every simulating halt decider H.

To refute the claim that the direct execution of P(P) halts thus its
simulation is incorrect H(P,P) directly executes its input instead of
simulating it. The result is the infinitely nested simulation becomes
infinite recursion.

In no case does the following directly executed P ever reach its final
state of c50.

// call void P(I);
int H(u32 P, u32 I)
{ if (!Halts(P,I)
return 0;
((void(*)(int))P)(I);
return 1;
}

int main()
{ H((u32)P, (u32)P);
}

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

Re: Concise refutation of halting problem proofs V5

<871r3pxrgc.fsf@bsb.me.uk>

 copy mid

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

 copy link   Newsgroups: comp.theory
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: ben.use...@bsb.me.uk (Ben Bacarisse)
Newsgroups: comp.theory
Subject: Re: Concise refutation of halting problem proofs V5
Date: Tue, 09 Nov 2021 15:46:11 +0000
Organization: A noiseless patient Spider
Lines: 56
Message-ID: <871r3pxrgc.fsf@bsb.me.uk>
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Info: reader02.eternal-september.org; posting-host="85c53abacd32481a9eba26655465b427";
logging-data="5471"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19Azlsvy7RAA5uKZ4xeONT/GGjWco1keyM="
Cancel-Lock: sha1:b92klB30A1G2iyXMJ4O2i9cN1M4=
sha1:I7bnXehN6nT3nSKtne+EHphB2Mc=
X-BSB-Auth: 1.4d6cdb08476555d590de.20211109154611GMT.871r3pxrgc.fsf@bsb.me.uk
 by: Ben Bacarisse - Tue, 9 Nov 2021 15:46 UTC

olcott <NoOne@NoWhere.com> writes:

> // Simplified Linz Ĥ (Linz:1990:319)
> // Strachey(1965) CPL translated to C
> void P(u32 x)
> {
> if (H(x, x))
> HERE: goto HERE;
> }
>
> _P()
> [00000c36](01) 55 push ebp
> [00000c37](02) 8bec mov ebp,esp
> [00000c39](03) 8b4508 mov eax,[ebp+08] // 2nd Param
> [00000c3c](01) 50 push eax
> [00000c3d](03) 8b4d08 mov ecx,[ebp+08] // 1st Param
> [00000c40](01) 51 push ecx
> [00000c41](05) e820fdffff call 00000966 // call H
> [00000c46](03) 83c408 add esp,+08
> [00000c49](02) 85c0 test eax,eax
> [00000c4b](02) 7402 jz 00000c4f
> [00000c4d](02) ebfe jmp 00000c4d
> [00000c4f](01) 5d pop ebp
> [00000c50](01) c3 ret
> Size in bytes:(0027) [00000c50]
>
> Begin Local Halt Decider Simulation at Machine Address:c36
>
> machine stack stack machine assembly
> address address data code language
> ======== ======== ======== ========= =============
> [00000c36][002117ca][002117ce] 55 push ebp
> [00000c37][002117ca][002117ce] 8bec mov ebp,esp
> [00000c39][002117ca][002117ce] 8b4508 mov eax,[ebp+08]
> [00000c3c][002117c6][00000c36] 50 push eax // push P
> [00000c3d][002117c6][00000c36] 8b4d08 mov ecx,[ebp+08]
> [00000c40][002117c2][00000c36] 51 push ecx // push P
> [00000c41][002117be][00000c46] e820fdffff call 00000966 // call H(P,P)

Aww... you stopped at the good bit. We'd love to see H fire up a nested
simulation (you don't do that though do you -- you just pretend).

And even if you want keep H all hidden and secret, you could show the
rest of the trace of P. The trouble is that that will confirm, yet
again that H is wrong. H(P,P) will be shown to return 0 and P(P).

What is your plan here? Keep posting more "versions" until someone
decides that false really is the right return from H when the arguments
represent a hating computation? That's not going to happen because
(almost) everyone here knows what a halt decider should do.

So presumably the plan in really just to keep chatting. That's a fine
plan, if you enjoy the chatting.

--
Ben.

Re: Concise refutation of halting problem proofs V5

<sme6cl$ti4$1@dont-email.me>

 copy mid

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

 copy link   Newsgroups: comp.theory sci.logic
Followup: comp.theory
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.theory,sci.logic
Subject: Re: Concise refutation of halting problem proofs V5
Followup-To: comp.theory
Date: Tue, 9 Nov 2021 10:07:47 -0600
Organization: A noiseless patient Spider
Lines: 72
Message-ID: <sme6cl$ti4$1@dont-email.me>
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 9 Nov 2021 16:07:49 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="a8861a107128644b80b0eaa7d3b2767b";
logging-data="30276"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+Bs07bMVi/Z0ZhbsW8BTP0"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.3.0
Cancel-Lock: sha1:fUMYCk8H611+FDTZtXM8/Q+r3jA=
In-Reply-To: <871r3pxrgc.fsf@bsb.me.uk>
Content-Language: en-US
 by: olcott - Tue, 9 Nov 2021 16:07 UTC

On 11/9/2021 9:46 AM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> // Simplified Linz Ĥ (Linz:1990:319)
>> // Strachey(1965) CPL translated to C
>> void P(u32 x)
>> {
>> if (H(x, x))
>> HERE: goto HERE;
>> }
>>
>> _P()
>> [00000c36](01) 55 push ebp
>> [00000c37](02) 8bec mov ebp,esp
>> [00000c39](03) 8b4508 mov eax,[ebp+08] // 2nd Param
>> [00000c3c](01) 50 push eax
>> [00000c3d](03) 8b4d08 mov ecx,[ebp+08] // 1st Param
>> [00000c40](01) 51 push ecx
>> [00000c41](05) e820fdffff call 00000966 // call H
>> [00000c46](03) 83c408 add esp,+08
>> [00000c49](02) 85c0 test eax,eax
>> [00000c4b](02) 7402 jz 00000c4f
>> [00000c4d](02) ebfe jmp 00000c4d
>> [00000c4f](01) 5d pop ebp
>> [00000c50](01) c3 ret
>> Size in bytes:(0027) [00000c50]
>>
>> Begin Local Halt Decider Simulation at Machine Address:c36
>>
>> machine stack stack machine assembly
>> address address data code language
>> ======== ======== ======== ========= =============
>> [00000c36][002117ca][002117ce] 55 push ebp
>> [00000c37][002117ca][002117ce] 8bec mov ebp,esp
>> [00000c39][002117ca][002117ce] 8b4508 mov eax,[ebp+08]
>> [00000c3c][002117c6][00000c36] 50 push eax // push P
>> [00000c3d][002117c6][00000c36] 8b4d08 mov ecx,[ebp+08]
>> [00000c40][002117c2][00000c36] 51 push ecx // push P
>> [00000c41][002117be][00000c46] e820fdffff call 00000966 // call H(P,P)
>
> Aww... you stopped at the good bit. We'd love to see H fire up a nested
> simulation (you don't do that though do you -- you just pretend).
>

When it comes to the x86 language you are totally out of your element
thus no sense talking to you about this.

Even from a computer science POV we know that when one invocation of
H(P,P) derives the above simulation of its input that subsequent
directly invoked or correctly simulated invocations of H(P,P) must
derive this same sequence of steps of P.

I would say that it seems a little goofy of you to deny this yet I chalk
that up to your utter cluelessness of the x86 language.

> And even if you want keep H all hidden and secret, you could show the
> rest of the trace of P. The trouble is that that will confirm, yet
> again that H is wrong. H(P,P) will be shown to return 0 and P(P).
>
> What is your plan here? Keep posting more "versions" until someone
> decides that false really is the right return from H when the arguments
> represent a hating computation? That's not going to happen because
> (almost) everyone here knows what a halt decider should do.
>
> So presumably the plan in really just to keep chatting. That's a fine
> plan, if you enjoy the chatting.
>

--
Copyright 2021 Pete Olcott "Great spirits have always encountered
violent opposition from mediocre minds." Einstein

Re: Concise refutation of halting problem proofs V5

<sWDiJ.26009$IB7.10803@fx02.iad>

 copy mid

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

 copy link   Newsgroups: comp.theory
Path: i2pn2.org!i2pn.org!aioe.org!feeder5.feed.usenet.farm!feeder1.feed.usenet.farm!feed.usenet.farm!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx02.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.3.0
Subject: Re: Concise refutation of halting problem proofs V5
Content-Language: en-US
Newsgroups: comp.theory
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <sme6cl$ti4$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 93
Message-ID: <sWDiJ.26009$IB7.10803@fx02.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: Tue, 9 Nov 2021 18:58:13 -0500
X-Received-Bytes: 4800
 by: Richard Damon - Tue, 9 Nov 2021 23:58 UTC

On 11/9/21 11:07 AM, olcott wrote:
> On 11/9/2021 9:46 AM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> // Simplified Linz Ĥ (Linz:1990:319)
>>> // Strachey(1965) CPL translated to C
>>> void P(u32 x)
>>> {
>>>    if (H(x, x))
>>>      HERE: goto HERE;
>>> }
>>>
>>> _P()
>>> [00000c36](01)  55          push ebp
>>> [00000c37](02)  8bec        mov ebp,esp
>>> [00000c39](03)  8b4508      mov eax,[ebp+08] // 2nd Param
>>> [00000c3c](01)  50          push eax
>>> [00000c3d](03)  8b4d08      mov ecx,[ebp+08] // 1st Param
>>> [00000c40](01)  51          push ecx
>>> [00000c41](05)  e820fdffff  call 00000966    // call H
>>> [00000c46](03)  83c408      add esp,+08
>>> [00000c49](02)  85c0        test eax,eax
>>> [00000c4b](02)  7402        jz 00000c4f
>>> [00000c4d](02)  ebfe        jmp 00000c4d
>>> [00000c4f](01)  5d          pop ebp
>>> [00000c50](01)  c3          ret
>>> Size in bytes:(0027) [00000c50]
>>>
>>> Begin Local Halt Decider Simulation at Machine Address:c36
>>>
>>>   machine   stack     stack     machine    assembly
>>>   address   address   data      code       language
>>>   ========  ========  ========  =========  =============
>>> [00000c36][002117ca][002117ce] 55          push ebp
>>> [00000c37][002117ca][002117ce] 8bec        mov ebp,esp
>>> [00000c39][002117ca][002117ce] 8b4508      mov eax,[ebp+08]
>>> [00000c3c][002117c6][00000c36] 50          push eax       // push P
>>> [00000c3d][002117c6][00000c36] 8b4d08      mov ecx,[ebp+08]
>>> [00000c40][002117c2][00000c36] 51          push ecx       // push P
>>> [00000c41][002117be][00000c46] e820fdffff  call 00000966  // call H(P,P)
>>
>> Aww... you stopped at the good bit.  We'd love to see H fire up a nested
>> simulation (you don't do that though do you -- you just pretend).
>>
>
> When it comes to the x86 language you are totally out of your element
> thus no sense talking to you about this.

You seem to be too, as you don't seem to understand the call instruction.

>
> Even from a computer science POV we know that when one invocation of
> H(P,P) derives the above simulation of its input that subsequent
> directly invoked or correctly simulated invocations of H(P,P) must
> derive this same sequence of steps of P.

Except that it doesn't. Since you claim that H(P,P) will return a
non-halting return code, that means that this call to H must do so two.

It is an invalid transormation to convert a simulation of a conditional
simulator into a simulation of the machine it is simulating.

(Or, if it isn't really a simulator, but a debug stepper with conditions
either).

>
> I would say that it seems a little goofy of you to deny this yet I chalk
> that up to your utter cluelessness of the x86 language.

No, the problem is your 'proof' is only valid when H is EXACTLY an
unconditional simulator/execution of its input. But it is easy to show
(as you do) that in THAT case, P(P) and H(P,P) are BOTH mutually
non-halting computaiton.

FAIL.

>
>> And even if you want keep H all hidden and secret, you could show the
>> rest of the trace of P.  The trouble is that that will confirm, yet
>> again that H is wrong.  H(P,P) will be shown to return 0 and P(P).
>>
>> What is your plan here?  Keep posting more "versions" until someone
>> decides that false really is the right return from H when the arguments
>> represent a hating computation?  That's not going to happen because
>> (almost) everyone here knows what a halt decider should do.
>>
>> So presumably the plan in really just to keep chatting.  That's a fine
>> plan, if you enjoy the chatting.
>>
>
>

Re: Concise refutation of halting problem proofs V5

<ApWdnaBlAu9Mkxb8nZ2dnUU7-IHNnZ2d@giganews.com>

 copy mid

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

 copy link   Newsgroups: comp.theory
Path: i2pn2.org!i2pn.org!aioe.org!feeder1.feed.usenet.farm!feed.usenet.farm!tr3.eu1.usenetexpress.com!feeder.usenetexpress.com!tr3.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Tue, 09 Nov 2021 18:14:09 -0600
Date: Tue, 9 Nov 2021 18:14:07 -0600
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Thunderbird/91.3.0
Subject: Re: Concise refutation of halting problem proofs V5
Content-Language: en-US
Newsgroups: comp.theory
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com> <871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me> <sWDiJ.26009$IB7.10803@fx02.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <sWDiJ.26009$IB7.10803@fx02.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <ApWdnaBlAu9Mkxb8nZ2dnUU7-IHNnZ2d@giganews.com>
Lines: 120
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-6x4Vz4bpAUUDrMhnAENkbX+rI3IQZD3o0+XxXksrOTAN3TObPw9GNJ4pAdtvM/g2XtTeXJAzptSp71a!CUQf0o04BwRxJR3pVzExy7T5r/KnBToDoLcMJfvZkR7KZfXpr32Yv+g9xkhszj8EwCD92DTKfgvi!tQ==
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: 6077
 by: olcott - Wed, 10 Nov 2021 00:14 UTC

On 11/9/2021 5:58 PM, Richard Damon wrote:
> On 11/9/21 11:07 AM, olcott wrote:
>> On 11/9/2021 9:46 AM, Ben Bacarisse wrote:
>>> olcott <NoOne@NoWhere.com> writes:
>>>
>>>> // Simplified Linz Ĥ (Linz:1990:319)
>>>> // Strachey(1965) CPL translated to C
>>>> void P(u32 x)
>>>> {
>>>>    if (H(x, x))
>>>>      HERE: goto HERE;
>>>> }
>>>>
>>>> _P()
>>>> [00000c36](01)  55          push ebp
>>>> [00000c37](02)  8bec        mov ebp,esp
>>>> [00000c39](03)  8b4508      mov eax,[ebp+08] // 2nd Param
>>>> [00000c3c](01)  50          push eax
>>>> [00000c3d](03)  8b4d08      mov ecx,[ebp+08] // 1st Param
>>>> [00000c40](01)  51          push ecx
>>>> [00000c41](05)  e820fdffff  call 00000966    // call H
>>>> [00000c46](03)  83c408      add esp,+08
>>>> [00000c49](02)  85c0        test eax,eax
>>>> [00000c4b](02)  7402        jz 00000c4f
>>>> [00000c4d](02)  ebfe        jmp 00000c4d
>>>> [00000c4f](01)  5d          pop ebp
>>>> [00000c50](01)  c3          ret
>>>> Size in bytes:(0027) [00000c50]
>>>>
>>>> Begin Local Halt Decider Simulation at Machine Address:c36
>>>>
>>>>   machine   stack     stack     machine    assembly
>>>>   address   address   data      code       language
>>>>   ========  ========  ========  =========  =============
>>>> [00000c36][002117ca][002117ce] 55          push ebp
>>>> [00000c37][002117ca][002117ce] 8bec        mov ebp,esp
>>>> [00000c39][002117ca][002117ce] 8b4508      mov eax,[ebp+08]
>>>> [00000c3c][002117c6][00000c36] 50          push eax       // push P
>>>> [00000c3d][002117c6][00000c36] 8b4d08      mov ecx,[ebp+08]
>>>> [00000c40][002117c2][00000c36] 51          push ecx       // push P
>>>> [00000c41][002117be][00000c46] e820fdffff  call 00000966  // call
>>>> H(P,P)
>>>
>>> Aww... you stopped at the good bit.  We'd love to see H fire up a nested
>>> simulation (you don't do that though do you -- you just pretend).
>>>
>>
>> When it comes to the x86 language you are totally out of your element
>> thus no sense talking to you about this.
>
> You seem to be too, as you don't seem to understand the call instruction.

It is not that I don't understand the call instruction, it that the
hundreds of pages of the detail of the simulation of the halt decider by
another instance of the halt decider are inessential to the point I am
making.

>
>
>>
>> Even from a computer science POV we know that when one invocation of
>> H(P,P) derives the above simulation of its input that subsequent
>> directly invoked or correctly simulated invocations of H(P,P) must
>> derive this same sequence of steps of P.
>
> Except that it doesn't. Since you claim that H(P,P) will return a
> non-halting return code, that means that this call to H must do so two.

By this same reasoning every element of an infinitely recursive sequence
must return to its caller. Infinitely nested simulation never halts, yet
does stop running when it is aborted.

>
> It is an invalid transormation to convert a simulation of a conditional
> simulator into a simulation of the machine it is simulating.
>

A simulating halt decider continues as a pure simulator of its input
until it detects an infinite execution behavior pattern or its input halts.

> (Or, if it isn't really a simulator, but a debug stepper with conditions
> either).
>
>>
>> I would say that it seems a little goofy of you to deny this yet I
>> chalk that up to your utter cluelessness of the x86 language.
>
> No, the problem is your 'proof' is only valid when H is EXACTLY an
> unconditional simulator/execution of its input. But it is easy to show
> (as you do) that in THAT case, P(P) and H(P,P) are BOTH mutually
> non-halting computaiton.
>
> FAIL.

>
>>
>>> And even if you want keep H all hidden and secret, you could show the
>>> rest of the trace of P.  The trouble is that that will confirm, yet
>>> again that H is wrong.  H(P,P) will be shown to return 0 and P(P).
>>>
>>> What is your plan here?  Keep posting more "versions" until someone
>>> decides that false really is the right return from H when the arguments
>>> represent a hating computation?  That's not going to happen because
>>> (almost) everyone here knows what a halt decider should do.
>>>
>>> So presumably the plan in really just to keep chatting.  That's a fine
>>> plan, if you enjoy the chatting.
>>>
>>
>>
>

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

Re: Concise refutation of halting problem proofs V5

<96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>

 copy mid

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

 copy link   Newsgroups: comp.theory
X-Received: by 2002:a37:4152:: with SMTP id o79mr9525273qka.169.1636504062615;
Tue, 09 Nov 2021 16:27:42 -0800 (PST)
X-Received: by 2002:a25:71d5:: with SMTP id m204mr11978580ybc.374.1636504062438;
Tue, 09 Nov 2021 16:27:42 -0800 (PST)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.theory
Date: Tue, 9 Nov 2021 16:27:42 -0800 (PST)
In-Reply-To: <sme6cl$ti4$1@dont-email.me>
Injection-Info: google-groups.googlegroups.com; posting-host=47.208.151.23; posting-account=7Xc2EwkAAABXMcQfERYamr3b-64IkBws
NNTP-Posting-Host: 47.208.151.23
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
Subject: Re: Concise refutation of halting problem proofs V5
From: dkleine...@gmail.com (dklei...@gmail.com)
Injection-Date: Wed, 10 Nov 2021 00:27:42 +0000
Content-Type: text/plain; charset="UTF-8"
Lines: 12
 by: dklei...@gmail.com - Wed, 10 Nov 2021 00:27 UTC

On Tuesday, November 9, 2021 at 8:07:52 AM UTC-8, olcott wrote:

> When it comes to the x86 language you are totally out of your element
> thus no sense talking to you about this.
I'm getting bored with this trope. I question whether you are in your
element talking about it.

First - which/what version of what started as 8086?

Second - why not use an assembler? Are you unfamiliar with assemblers?
I believe you once described how you used the Microsoft C# compiler as
an assembler. The code you shown us is not IMHO very good code.

Re: Concise refutation of halting problem proofs V5

<YnEiJ.107750$831.58799@fx40.iad>

 copy mid

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

 copy link   Newsgroups: comp.theory
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx40.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.3.0
Subject: Re: Concise refutation of halting problem proofs V5
Content-Language: en-US
Newsgroups: comp.theory
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 135
Message-ID: <YnEiJ.107750$831.58799@fx40.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: Tue, 9 Nov 2021 19:29:45 -0500
X-Received-Bytes: 5678
X-Original-Bytes: 5545
 by: Richard Damon - Wed, 10 Nov 2021 00:29 UTC

On 11/9/21 9:52 AM, olcott wrote:
> // Simplified Linz Ĥ (Linz:1990:319)
> // Strachey(1965) CPL translated to C
> void P(u32 x)
> {
>   if (H(x, x))
>     HERE: goto HERE;
> }
>
> _P()
> [00000c36](01)  55          push ebp
> [00000c37](02)  8bec        mov ebp,esp
> [00000c39](03)  8b4508      mov eax,[ebp+08] // 2nd Param
> [00000c3c](01)  50          push eax
> [00000c3d](03)  8b4d08      mov ecx,[ebp+08] // 1st Param
> [00000c40](01)  51          push ecx
> [00000c41](05)  e820fdffff  call 00000966    // call H
> [00000c46](03)  83c408      add esp,+08
> [00000c49](02)  85c0        test eax,eax
> [00000c4b](02)  7402        jz 00000c4f
> [00000c4d](02)  ebfe        jmp 00000c4d
> [00000c4f](01)  5d          pop ebp
> [00000c50](01)  c3          ret
> Size in bytes:(0027) [00000c50]
>
> Begin Local Halt Decider Simulation at Machine Address:c36
>
>  machine   stack     stack     machine    assembly
>  address   address   data      code       language
>  ========  ========  ========  =========  =============
> [00000c36][002117ca][002117ce] 55          push ebp
> [00000c37][002117ca][002117ce] 8bec        mov ebp,esp
> [00000c39][002117ca][002117ce] 8b4508      mov eax,[ebp+08]
> [00000c3c][002117c6][00000c36] 50          push eax       // push P
> [00000c3d][002117c6][00000c36] 8b4d08      mov ecx,[ebp+08]
> [00000c40][002117c2][00000c36] 51          push ecx       // push P
> [00000c41][002117be][00000c46] e820fdffff  call 00000966  // call H(P,P)
>
> Because P calls H(P,P) P specifies infinitely nested simulation to every
> simulating halt decider H.

Except it doesn't

It only specifies infinitely nested simulatios of H just unconditionally
simualates its input.

Yes, if H is non-aborting, so H is the equivalent of a pure simulator,
then P(P) is non-halting as you show, but H(P,P) never answers so fails.

Once you let H abort its simulation, then your statement is untrue as H
WILL abort the simulation and keep it from being infinite, and this
makes P(P) halting.

>
> This has been verified with the execution trace of a correct pure
> simulation of P.

Nope. A CORRECT pure simulation of P(P), for the case when H(P,P)
returns the 0, shows that P(P) Halts.

Only the PARTIAL simulation done by H implies a non-halting (actual, not
yet halting) computation for P(P).

>
> Whether or not H aborts its simulation P never reaches its final state
> therefore the simulated P never halts.

CHOOSE which is H, that determines WHICH way it fails, on DIFFERENT Ps.

If H does not abort its simulaiton, then the P based on it IS
non-halting for P(P), but so is H(P,P) so H fails.

If P does abort its simulation, and return non-halting, it turns out
that the P based on THAT H will always Halt, and H makes the mistake of
assuming that the copy of itself in P will not abort its simulation, and
thus H is using UNSOUND logic.

>
> If the simulated P never halts then H(P,P)==0 is always correct for
> every simulating halt decider H.

Except that if H(P,P) returns 0, then P(P) halts and H hasn't actually
proven that it won't. only your UNSOUND logic wants to try to claim it.

>
> To refute the claim that the direct execution of P(P) halts thus its
> simulation is incorrect H(P,P) directly executes its input instead of
> simulating it. The result is the infinitely nested simulation becomes
> infinite recursion.

Your 'Direct Execution' via H argument only works when H IS
non-aborting. Remember, every H has a different P, so you can't just
globally change H.

In fact, your H1 machine just prove that H is wrong, H1 is a copy of H
that won't abort its simulation of P(P) based on the original H, and H1
thus shows what the direct exectuion of that P does, it HALTS.

Thus, your H1 doesn't show that H was right as you claim, but shows that
it was WRONG.

>
> In no case does the following directly executed P ever reach its final
> state of c50.

So this version of H needs to have a Halts function that decides if P(I)
will Halt,

You need to prove that Halts is correct.

YOu have just kicked the can down a level.

This does NOT prove if P(I) is actually non-halting, as if Halts THINKS
it is, it never gets run.

Thus, this machine doesn't prove anything except that you don't know how
to prove things.

>
> // call void P(I);
> int H(u32 P, u32 I)
> {
>   if (!Halts(P,I)
>     return 0;
>   ((void(*)(int))P)(I);
>   return 1;
> }
>
> int main()
> {
>   H((u32)P, (u32)P);
> }
>
>

Re: Concise refutation of halting problem proofs V5

<nsEiJ.30220$Bu7.26047@fx26.iad>

 copy mid

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

 copy link   Newsgroups: comp.theory
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer02.ams1!peer.ams1.xlned.com!news.xlned.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx26.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.3.0
Subject: Re: Concise refutation of halting problem proofs V5
Content-Language: en-US
Newsgroups: comp.theory
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
<sWDiJ.26009$IB7.10803@fx02.iad>
<ApWdnaBlAu9Mkxb8nZ2dnUU7-IHNnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <ApWdnaBlAu9Mkxb8nZ2dnUU7-IHNnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 134
Message-ID: <nsEiJ.30220$Bu7.26047@fx26.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: Tue, 9 Nov 2021 19:34:27 -0500
X-Received-Bytes: 6582
 by: Richard Damon - Wed, 10 Nov 2021 00:34 UTC

On 11/9/21 7:14 PM, olcott wrote:
> On 11/9/2021 5:58 PM, Richard Damon wrote:
>> On 11/9/21 11:07 AM, olcott wrote:
>>> On 11/9/2021 9:46 AM, Ben Bacarisse wrote:
>>>> olcott <NoOne@NoWhere.com> writes:
>>>>
>>>>> // Simplified Linz Ĥ (Linz:1990:319)
>>>>> // Strachey(1965) CPL translated to C
>>>>> void P(u32 x)
>>>>> {
>>>>>    if (H(x, x))
>>>>>      HERE: goto HERE;
>>>>> }
>>>>>
>>>>> _P()
>>>>> [00000c36](01)  55          push ebp
>>>>> [00000c37](02)  8bec        mov ebp,esp
>>>>> [00000c39](03)  8b4508      mov eax,[ebp+08] // 2nd Param
>>>>> [00000c3c](01)  50          push eax
>>>>> [00000c3d](03)  8b4d08      mov ecx,[ebp+08] // 1st Param
>>>>> [00000c40](01)  51          push ecx
>>>>> [00000c41](05)  e820fdffff  call 00000966    // call H
>>>>> [00000c46](03)  83c408      add esp,+08
>>>>> [00000c49](02)  85c0        test eax,eax
>>>>> [00000c4b](02)  7402        jz 00000c4f
>>>>> [00000c4d](02)  ebfe        jmp 00000c4d
>>>>> [00000c4f](01)  5d          pop ebp
>>>>> [00000c50](01)  c3          ret
>>>>> Size in bytes:(0027) [00000c50]
>>>>>
>>>>> Begin Local Halt Decider Simulation at Machine Address:c36
>>>>>
>>>>>   machine   stack     stack     machine    assembly
>>>>>   address   address   data      code       language
>>>>>   ========  ========  ========  =========  =============
>>>>> [00000c36][002117ca][002117ce] 55          push ebp
>>>>> [00000c37][002117ca][002117ce] 8bec        mov ebp,esp
>>>>> [00000c39][002117ca][002117ce] 8b4508      mov eax,[ebp+08]
>>>>> [00000c3c][002117c6][00000c36] 50          push eax       // push P
>>>>> [00000c3d][002117c6][00000c36] 8b4d08      mov ecx,[ebp+08]
>>>>> [00000c40][002117c2][00000c36] 51          push ecx       // push P
>>>>> [00000c41][002117be][00000c46] e820fdffff  call 00000966  // call
>>>>> H(P,P)
>>>>
>>>> Aww... you stopped at the good bit.  We'd love to see H fire up a
>>>> nested
>>>> simulation (you don't do that though do you -- you just pretend).
>>>>
>>>
>>> When it comes to the x86 language you are totally out of your element
>>> thus no sense talking to you about this.
>>
>> You seem to be too, as you don't seem to understand the call instruction.
>
> It is not that I don't understand the call instruction, it that the
> hundreds of pages of the detail of the simulation of the halt decider by
> another instance of the halt decider are inessential to the point I am
> making.
>
>>
>>
>>>
>>> Even from a computer science POV we know that when one invocation of
>>> H(P,P) derives the above simulation of its input that subsequent
>>> directly invoked or correctly simulated invocations of H(P,P) must
>>> derive this same sequence of steps of P.
>>
>> Except that it doesn't. Since you claim that H(P,P) will return a
>> non-halting return code, that means that this call to H must do so two.
>
> By this same reasoning every element of an infinitely recursive sequence
> must return to its caller. Infinitely nested simulation never halts, yet
> does stop running when it is aborted.

No, thats not what I said. The problem is that it ONE copy of H will
return to its caller, then ALL copies of H, given the same input, will.

Since the top level H(P,P) returns 0 (as you claim of being correct in
doing so) that means that, if we actually run the computation P(P) that
was given as a representation to H, the H in it will do so also,

IF H's simulation disagrees with that result, the the simulation done by
H doesn't match the computaiton it is simulating, and thus the
simulation MUST be incorrect.

>
>>
>> It is an invalid transormation to convert a simulation of a
>> conditional simulator into a simulation of the machine it is simulating.
>>
>
> A simulating halt decider continues as a pure simulator of its input
> until it detects an infinite execution behavior pattern or its input halts.

And if it ever stops its simulation, it has shown that it NEVER was a
Pure Simulator, and thus treating it as one was incorrect.

>
>> (Or, if it isn't really a simulator, but a debug stepper with
>> conditions either).
>>
>>>
>>> I would say that it seems a little goofy of you to deny this yet I
>>> chalk that up to your utter cluelessness of the x86 language.
>>
>> No, the problem is your 'proof' is only valid when H is EXACTLY an
>> unconditional simulator/execution of its input. But it is easy to show
>> (as you do) that in THAT case, P(P) and H(P,P) are BOTH mutually
>> non-halting computaiton.
>>
>> FAIL.
>
>
>
>>
>>>
>>>> And even if you want keep H all hidden and secret, you could show the
>>>> rest of the trace of P.  The trouble is that that will confirm, yet
>>>> again that H is wrong.  H(P,P) will be shown to return 0 and P(P).
>>>>
>>>> What is your plan here?  Keep posting more "versions" until someone
>>>> decides that false really is the right return from H when the arguments
>>>> represent a hating computation?  That's not going to happen because
>>>> (almost) everyone here knows what a halt decider should do.
>>>>
>>>> So presumably the plan in really just to keep chatting.  That's a fine
>>>> plan, if you enjoy the chatting.
>>>>
>>>
>>>
>>
>
>

Re: Concise refutation of halting problem proofs V5

<i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com>

 copy mid

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

 copy link   Newsgroups: comp.theory
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!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Tue, 09 Nov 2021 18:42:21 -0600
Date: Tue, 9 Nov 2021 18:42:19 -0600
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.3.0
Subject: Re: Concise refutation of halting problem proofs V5
Content-Language: en-US
Newsgroups: comp.theory
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
<96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com>
Lines: 32
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-jyEGbunOHFFXzCyyX4lMrjSIlslI/2EeDi4hSMYOtVs67NyqdRnOO2qnWxQMXnau6YN+PibJo98ylc5!bKpCNIdUDPRwUCg+cc8oVo16OAecAj61GCf3Za6HvhaoadCnijW32OlIp6KL08ZGO9XJHGekwnuP!0w==
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: 2431
 by: olcott - Wed, 10 Nov 2021 00:42 UTC

On 11/9/2021 6:27 PM, dklei...@gmail.com wrote:
> On Tuesday, November 9, 2021 at 8:07:52 AM UTC-8, olcott wrote:
>
>> When it comes to the x86 language you are totally out of your element
>> thus no sense talking to you about this.
>
> I'm getting bored with this trope. I question whether you are in your
> element talking about it.
>
> First - which/what version of what started as 8086?
>

I only use a tiny subset of 80386 that would otherwise only be a tiny
subset of 8088 if I did not use 32-bit addressing.

> Second - why not use an assembler? Are you unfamiliar with assemblers?

The x86 language specifies a ready made directed graph of all control
flow, thus easy to analyze.

> I believe you once described how you used the Microsoft C# compiler as
> an assembler. The code you shown us is not IMHO very good code.

The x86 code is directly generated by the Microsoft C compiler.
It is actually quite clean code.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

Re: Concise refutation of halting problem proofs V5

<fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com>

 copy mid

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

 copy link   Newsgroups: comp.theory
X-Received: by 2002:a05:622a:54f:: with SMTP id m15mr14596559qtx.365.1636519530099;
Tue, 09 Nov 2021 20:45:30 -0800 (PST)
X-Received: by 2002:a25:e6c5:: with SMTP id d188mr14002850ybh.217.1636519529902;
Tue, 09 Nov 2021 20:45:29 -0800 (PST)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.theory
Date: Tue, 9 Nov 2021 20:45:29 -0800 (PST)
In-Reply-To: <i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com>
Injection-Info: google-groups.googlegroups.com; posting-host=47.208.151.23; posting-account=7Xc2EwkAAABXMcQfERYamr3b-64IkBws
NNTP-Posting-Host: 47.208.151.23
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me> <96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
<i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com>
Subject: Re: Concise refutation of halting problem proofs V5
From: dkleine...@gmail.com (dklei...@gmail.com)
Injection-Date: Wed, 10 Nov 2021 04:45:30 +0000
Content-Type: text/plain; charset="UTF-8"
Lines: 24
 by: dklei...@gmail.com - Wed, 10 Nov 2021 04:45 UTC

On Tuesday, November 9, 2021 at 4:42:28 PM UTC-8, olcott wrote:
> On 11/9/2021 6:27 PM, dklei...@gmail.com wrote:

> > ... - why not use an assembler? Are you unfamiliar with assemblers?

> The x86 language specifies a ready made directed graph of all control
> flow, thus easy to analyze.

I agree that the 386 code is relatively easy to follow. But you are actually
coding in C (probably Microsoft C) and using the assumptions that
Microsoft makes as the operating context (for example, how call arguments
are passed) and these assumptions do not cause the simplest code to be
sent to the object code. Your arguments would be much easier to follow
in their native C than in object code.

Anyone with any experience in disassembly of code given them in machine
code knows that, at least with non-optimizing assemblers, code generated
from C sources is easily disassembled back to C.

> > I believe you once described how you used the Microsoft C# compiler as
> > an assembler. The code you shown us is not IMHO very good code.
> The x86 code is directly generated by the Microsoft C compiler.
> It is actually quite clean code.

How much optimization did you apply?

Re: Concise refutation of halting problem proofs V5 (Linz version)

<FKidnYodj5r30hb8nZ2dnUU7-RXNnZ2d@giganews.com>

 copy mid

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

 copy link   Newsgroups: comp.theory
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: Tue, 09 Nov 2021 22:49:46 -0600
Date: Tue, 9 Nov 2021 22:49:44 -0600
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.3.0
Subject: Re: Concise refutation of halting problem proofs V5 (Linz version)
Content-Language: en-US
Newsgroups: comp.theory
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <871r3pxrgc.fsf@bsb.me.uk>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <FKidnYodj5r30hb8nZ2dnUU7-RXNnZ2d@giganews.com>
Lines: 76
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-dI71IolPTeXVXrRMOUb9PVLZ3ENESS6Ta66gW3tauJSOT1TB5cB1g8bTwtEzWydKob4awpwkqgWtzJM!oSmW2FNSxfolrWAWcBpq8EUqZYs7Ir7jxHftgYYwCbQwLdUX6vQpQpQ0x7k18J4TzmQAZOJqRz1v!Yg==
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: 4332
 by: olcott - Wed, 10 Nov 2021 04:49 UTC

On 11/9/2021 9:46 AM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> // Simplified Linz Ĥ (Linz:1990:319)
>> // Strachey(1965) CPL translated to C
>> void P(u32 x)
>> {
>> if (H(x, x))
>> HERE: goto HERE;
>> }
>>
>> _P()
>> [00000c36](01) 55 push ebp
>> [00000c37](02) 8bec mov ebp,esp
>> [00000c39](03) 8b4508 mov eax,[ebp+08] // 2nd Param
>> [00000c3c](01) 50 push eax
>> [00000c3d](03) 8b4d08 mov ecx,[ebp+08] // 1st Param
>> [00000c40](01) 51 push ecx
>> [00000c41](05) e820fdffff call 00000966 // call H
>> [00000c46](03) 83c408 add esp,+08
>> [00000c49](02) 85c0 test eax,eax
>> [00000c4b](02) 7402 jz 00000c4f
>> [00000c4d](02) ebfe jmp 00000c4d
>> [00000c4f](01) 5d pop ebp
>> [00000c50](01) c3 ret
>> Size in bytes:(0027) [00000c50]
>>
>> Begin Local Halt Decider Simulation at Machine Address:c36
>>
>> machine stack stack machine assembly
>> address address data code language
>> ======== ======== ======== ========= =============
>> [00000c36][002117ca][002117ce] 55 push ebp
>> [00000c37][002117ca][002117ce] 8bec mov ebp,esp
>> [00000c39][002117ca][002117ce] 8b4508 mov eax,[ebp+08]
>> [00000c3c][002117c6][00000c36] 50 push eax // push P
>> [00000c3d][002117c6][00000c36] 8b4d08 mov ecx,[ebp+08]
>> [00000c40][002117c2][00000c36] 51 push ecx // push P
>> [00000c41][002117be][00000c46] e820fdffff call 00000966 // call H(P,P)
>
> Aww... you stopped at the good bit. We'd love to see H fire up a nested
> simulation (you don't do that though do you -- you just pretend).
>
> And even if you want keep H all hidden and secret, you could show the
> rest of the trace of P. The trouble is that that will confirm, yet
> again that H is wrong. H(P,P) will be shown to return 0 and P(P).
>
> What is your plan here? Keep posting more "versions" until someone
> decides that false really is the right return from H when the arguments
> represent a hating computation? That's not going to happen because
> (almost) everyone here knows what a halt decider should do.
>
> So presumably the plan in really just to keep chatting. That's a fine
> plan, if you enjoy the chatting.
>

In this Linz machine:
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
it is true that the correct pure simulation of the
input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach its final state
whether or not the simulating halt decider at
Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ aborted the simulation of its input.

This conclusively proves that this state transition
is correct: Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

As long as the halt decider H reports the halt
status of the behavior of its actual input P then
H is necessarily correct no matter how P behaves
in any other situation.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

Re: Concise refutation of halting problem proofs V5 [Linz version]

<VZWdnX77sYCZzhb8nZ2dnUU7-aWdnZ2d@giganews.com>

 copy mid

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

 copy link   Newsgroups: comp.theory
Path: i2pn2.org!rocksolid2!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: Tue, 09 Nov 2021 23:05:07 -0600
Date: Tue, 9 Nov 2021 23:05:06 -0600
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.3.0
Subject: Re: Concise refutation of halting problem proofs V5 [Linz version]
Content-Language: en-US
Newsgroups: comp.theory
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
<96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
<i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com>
<fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <VZWdnX77sYCZzhb8nZ2dnUU7-aWdnZ2d@giganews.com>
Lines: 52
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-Pod3HI/AyjivOD4u3WuUkVJev04GDO3bY7Sd79H42WCdTxkwMmVwpjXVGi4LsJgFA8TCTtu1FdU080X!yMaxJG0/21FtQFv1owMKf3QqFaY7eLSst5CObfoFvCpqR0gVEK22xiSbEisAua2s/VIUaQ621dtK!cA==
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: 3532
 by: olcott - Wed, 10 Nov 2021 05:05 UTC

On 11/9/2021 10:45 PM, dklei...@gmail.com wrote:
> On Tuesday, November 9, 2021 at 4:42:28 PM UTC-8, olcott wrote:
>> On 11/9/2021 6:27 PM, dklei...@gmail.com wrote:
>
>>> ... - why not use an assembler? Are you unfamiliar with assemblers?
>
>> The x86 language specifies a ready made directed graph of all control
>> flow, thus easy to analyze.
>
> I agree that the 386 code is relatively easy to follow. But you are actually
> coding in C (probably Microsoft C) and using the assumptions that
> Microsoft makes as the operating context (for example, how call arguments
> are passed) and these assumptions do not cause the simplest code to be
> sent to the object code. Your arguments would be much easier to follow
> in their native C than in object code.
>
> Anyone with any experience in disassembly of code given them in machine
> code knows that, at least with non-optimizing assemblers, code generated
> from C sources is easily disassembled back to C.
>
>>> I believe you once described how you used the Microsoft C# compiler as
>>> an assembler. The code you shown us is not IMHO very good code.
>> The x86 code is directly generated by the Microsoft C compiler.
>> It is actually quite clean code.
>
> How much optimization did you apply?
>

None.

Here is the same thing using Peter Linz notation:

In this Linz machine:
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
it is true that the correct pure simulation of the
input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach its final state
whether or not the simulating halt decider at
Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ aborted the simulation of its input.

This conclusively proves that this state transition
is correct: Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

As long as the halt decider H reports the halt
status of the behavior of its actual input P then
H is necessarily correct no matter how P behaves
in any other situation.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

Re: Concise refutation of halting problem proofs V5 [Linz version]

<87bl2sw8e7.fsf@bsb.me.uk>

 copy mid

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

 copy link   Newsgroups: comp.theory
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: ben.use...@bsb.me.uk (Ben Bacarisse)
Newsgroups: comp.theory
Subject: Re: Concise refutation of halting problem proofs V5 [Linz version]
Date: Wed, 10 Nov 2021 11:35:28 +0000
Organization: A noiseless patient Spider
Lines: 22
Message-ID: <87bl2sw8e7.fsf@bsb.me.uk>
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
<96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
<i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com>
<fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com>
<VZWdnX77sYCZzhb8nZ2dnUU7-aWdnZ2d@giganews.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Info: reader02.eternal-september.org; posting-host="0c198982b61379bd46027c61d9639410";
logging-data="9610"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19va1DQ6EqDEvo6gCFAoHRM7skaicu1yTM="
Cancel-Lock: sha1:Rg5wM8UiOdXUfv5Kx1GkunC7BEs=
sha1:66W0hOSNCb0hYcaTVjrM5lgn4KM=
X-BSB-Auth: 1.67d148f5135d33dafb71.20211110113528GMT.87bl2sw8e7.fsf@bsb.me.uk
 by: Ben Bacarisse - Wed, 10 Nov 2021 11:35 UTC

olcott <NoOne@NoWhere.com> writes:

> Here is the same thing using Peter Linz notation:

Oh dear, back to talking about Turing machines...

> In this Linz machine:
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
> it is true that the correct pure simulation of the
> input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩

There is no string ⟨Ĥ⟩, so there is nothing that can be simulated. You
keep removing the clause that defines Ĥ's behaviour:

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
if (and only if) Ĥ applied to ⟨Ĥ⟩ does not halt.

With that clause put back, you (well, other people at least) can see
that no TM can behave like this.

--
Ben.

Re: Concise refutation of halting problem proofs V5

<875yt0w7jt.fsf@bsb.me.uk>

 copy mid

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

 copy link   Newsgroups: comp.theory
Followup: comp.theory
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: ben.use...@bsb.me.uk (Ben Bacarisse)
Newsgroups: comp.theory
Subject: Re: Concise refutation of halting problem proofs V5
Followup-To: comp.theory
Date: Wed, 10 Nov 2021 11:53:42 +0000
Organization: A noiseless patient Spider
Lines: 82
Message-ID: <875yt0w7jt.fsf@bsb.me.uk>
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Info: reader02.eternal-september.org; posting-host="0c198982b61379bd46027c61d9639410";
logging-data="9610"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+6rQnwJQhUu1XQshSQqK2nW6koKl5Ct78="
Cancel-Lock: sha1:8/f9ZaBVbQdtpPok0XYcogxMwMk=
sha1:fH7Cxh8ZjQ/ZaT8onNW04nLAr9U=
X-BSB-Auth: 1.2eb4ff31d1745ce1fb69.20211110115342GMT.875yt0w7jt.fsf@bsb.me.uk
 by: Ben Bacarisse - Wed, 10 Nov 2021 11:53 UTC

olcott <polcott2@gmail.com> writes:

> On 11/9/2021 9:46 AM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> // Simplified Linz Ĥ (Linz:1990:319)
>>> // Strachey(1965) CPL translated to C
>>> void P(u32 x)
>>> {
>>> if (H(x, x))
>>> HERE: goto HERE;
>>> }
>>>
>>> _P()
>>> [00000c36](01) 55 push ebp
>>> [00000c37](02) 8bec mov ebp,esp
>>> [00000c39](03) 8b4508 mov eax,[ebp+08] // 2nd Param
>>> [00000c3c](01) 50 push eax
>>> [00000c3d](03) 8b4d08 mov ecx,[ebp+08] // 1st Param
>>> [00000c40](01) 51 push ecx
>>> [00000c41](05) e820fdffff call 00000966 // call H
>>> [00000c46](03) 83c408 add esp,+08
>>> [00000c49](02) 85c0 test eax,eax
>>> [00000c4b](02) 7402 jz 00000c4f
>>> [00000c4d](02) ebfe jmp 00000c4d
>>> [00000c4f](01) 5d pop ebp
>>> [00000c50](01) c3 ret
>>> Size in bytes:(0027) [00000c50]
>>>
>>> Begin Local Halt Decider Simulation at Machine Address:c36
>>>
>>> machine stack stack machine assembly
>>> address address data code language
>>> ======== ======== ======== ========= =============
>>> [00000c36][002117ca][002117ce] 55 push ebp
>>> [00000c37][002117ca][002117ce] 8bec mov ebp,esp
>>> [00000c39][002117ca][002117ce] 8b4508 mov eax,[ebp+08]
>>> [00000c3c][002117c6][00000c36] 50 push eax // push P
>>> [00000c3d][002117c6][00000c36] 8b4d08 mov ecx,[ebp+08]
>>> [00000c40][002117c2][00000c36] 51 push ecx // push P
>>> [00000c41][002117be][00000c46] e820fdffff call 00000966 // call H(P,P)
>> Aww... you stopped at the good bit. We'd love to see H fire up a nested
>> simulation (you don't do that though do you -- you just pretend).
>
> When it comes to the x86 language you are totally out of your element
> thus no sense talking to you about this.

You really want to goad me into talking about the code and not the big
reason why are wrong!

You are wrong because H(P,P) == 0 but P(P) halts. Nothing else matters.
The fact you don't show this incorrect behaviour in your traces suggests
you know something is wrong, but the fact you are wrong is what matters.

> Even from a computer science POV we know that when one invocation of
> H(P,P) derives the above simulation of its input that subsequent
> directly invoked or correctly simulated invocations of H(P,P) must
> derive this same sequence of steps of P.

Waffle. H(P,P) == 0 is wrong because P(P) halts. I think this should
be the only reply to any post you make about your code. Trying to
explain to you why your rationalisations are wrong is, in my opinion, a
waste of time

> I would say that it seems a little goofy of you to deny this yet I
> chalk that up to your utter cluelessness of the x86 language.

That H(P,P) == 0 is wrong because P(P) halts can be understood by simply
consulting the definition of the problem you claim to have been studying
for decades. You can't insult your way out of the error.

>> What is your plan here? Keep posting more "versions" until someone
>> decides that false really is the right return from H when the arguments
>> represent a hating computation? That's not going to happen because
>> (almost) everyone here knows what a halt decider should do.
>> So presumably the plan in really just to keep chatting. That's a fine
>> plan, if you enjoy the chatting.

I'd still like to know what your plan is.

--
Ben.

Re: Concise refutation of halting problem proofs V5 (Linz version)

<87zgqcusi4.fsf@bsb.me.uk>

 copy mid

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

 copy link   Newsgroups: comp.theory
Followup: comp.theory
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: ben.use...@bsb.me.uk (Ben Bacarisse)
Newsgroups: comp.theory
Subject: Re: Concise refutation of halting problem proofs V5 (Linz version)
Followup-To: comp.theory
Date: Wed, 10 Nov 2021 12:04:03 +0000
Organization: A noiseless patient Spider
Lines: 35
Message-ID: <87zgqcusi4.fsf@bsb.me.uk>
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk>
<FKidnYodj5r30hb8nZ2dnUU7-RXNnZ2d@giganews.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Info: reader02.eternal-september.org; posting-host="0c198982b61379bd46027c61d9639410";
logging-data="9610"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19pna1NMjPqlBxOXQzT32B2/RlHvWNKhSI="
Cancel-Lock: sha1:Gx0dEyABk8zTtLejUcjsVli+gvs=
sha1:jh3Yd0GR2R8YSOxced6rDLfF5SY=
X-BSB-Auth: 1.ec2a7575a1e979567f54.20211110120403GMT.87zgqcusi4.fsf@bsb.me.uk
 by: Ben Bacarisse - Wed, 10 Nov 2021 12:04 UTC

olcott <NoOne@NoWhere.com> writes:

> In this Linz machine:
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

It's only Linz's machine if this line applies if (and only if) Ĥ applied
to ⟨Ĥ⟩ does not halt. In other words, it's only Linz's machine if it is
logically impossible.

> it is true that the correct pure simulation of the
> input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach its final state
> whether or not the simulating halt decider at
> Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ aborted the simulation of its input.

There is no string ⟨Ĥ⟩, so there is nothing to simulate. I can specify
an x such that

x < 3
is (and only if) x > 5

and you can speculate about what a TM, E, that determines if x is even
when given <x>, the binary encoding of x, but I will always just tell
you that there is no such string, so the computation E <x> is
meaningless. UTM ⟨Ĥ⟩ ⟨Ĥ⟩ is similarly meaningless. There is no string
⟨Ĥ⟩ ⟨Ĥ⟩.

> This conclusively proves that this state transition
> is correct: Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

That transition happens if, and only if, it does not happen.

You really should leave Turing machines alone.

--
Ben.

Re: Concise refutation of halting problem proofs V5 [Linz version]

<CAOiJ.5854$a24.3827@fx13.iad>

 copy mid

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

 copy link   Newsgroups: comp.theory
Path: i2pn2.org!i2pn.org!aioe.org!feeder1.feed.usenet.farm!feed.usenet.farm!peer01.ams4!peer.am4.highwinds-media.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx13.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.3.0
Subject: Re: Concise refutation of halting problem proofs V5 [Linz version]
Content-Language: en-US
Newsgroups: comp.theory
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
<96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
<i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com>
<fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com>
<VZWdnX77sYCZzhb8nZ2dnUU7-aWdnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <VZWdnX77sYCZzhb8nZ2dnUU7-aWdnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 73
Message-ID: <CAOiJ.5854$a24.3827@fx13.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: Wed, 10 Nov 2021 07:05:53 -0500
X-Received-Bytes: 3981
 by: Richard Damon - Wed, 10 Nov 2021 12:05 UTC

On 11/10/21 12:05 AM, olcott wrote:
> On 11/9/2021 10:45 PM, dklei...@gmail.com wrote:
>> On Tuesday, November 9, 2021 at 4:42:28 PM UTC-8, olcott wrote:
>>> On 11/9/2021 6:27 PM, dklei...@gmail.com wrote:
>>
>>>> ... - why not use an assembler? Are you unfamiliar with assemblers?
>>
>>> The x86 language specifies a ready made directed graph of all control
>>> flow, thus easy to analyze.
>>
>> I agree that the 386 code is relatively easy to follow. But you are
>> actually
>> coding in C (probably Microsoft C) and using the assumptions that
>> Microsoft makes as the operating context (for example, how call arguments
>> are passed) and these assumptions do not cause the simplest code to be
>> sent to the object code. Your arguments would  be much easier to follow
>> in their native C than in  object code.
>>
>> Anyone with any experience in disassembly of code given them in machine
>> code knows that, at least with non-optimizing assemblers, code generated
>> from C sources is easily disassembled back to C.
>>
>>>> I believe you once described how you used the Microsoft C# compiler as
>>>> an assembler. The code you shown us is not IMHO very good code.
>>> The x86 code is directly generated by the Microsoft C compiler.
>>> It is actually quite clean code.
>>
>> How much optimization did you apply?
>>
>
> None.
>
> Here is the same thing using Peter Linz notation:
>
> In this Linz machine:
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
> it is true that the correct pure simulation of the
> input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach its final state
> whether or not the simulating halt decider at
> Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ aborted the simulation of its input.

Except that we actually know that if H goes to qn then H^ will end up at
H^qn and halt, and thus a real pure simulationo of H^ will reach that
same final state.

H is NOT a pure simulator, so the fact that it doesn't see that happens
is irrelevent.

>
> This conclusively proves that this state transition
> is correct: Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

No, it doesn't.
>
> As long as the halt decider H reports the halt
> status of the behavior of its actual input P then
> H is necessarily correct no matter how P behaves
> in any other situation.
>
You keep on makeing the wrong claim.

Inputs don't halt. Machines do.

When the machine represented by the input is run, it halts.

When the input is given to a real UTM, it halts.

Only when the input is given to your PARTIAL simulator H does is get
aborted before reaching its terminal state, that is NOT non-halting,
that is not-yet-halted, for which we can show the final result will be
halting.

FAIL.

Re: Concise refutation of halting problem proofs V5 (Linz version)

<PYOiJ.112783$I%1.31840@fx36.iad>

 copy mid

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

 copy link   Newsgroups: comp.theory
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!news.uzoreto.com!feeder.usenetexpress.com!tr1.eu1.usenetexpress.com!nntp.speedium.network!feeder01!81.171.65.14.MISMATCH!peer02.ams4!peer.am4.highwinds-media.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx36.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.3.0
Subject: Re: Concise refutation of halting problem proofs V5 (Linz version)
Content-Language: en-US
Newsgroups: comp.theory
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com> <871r3pxrgc.fsf@bsb.me.uk> <FKidnYodj5r30hb8nZ2dnUU7-RXNnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <FKidnYodj5r30hb8nZ2dnUU7-RXNnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 107
Message-ID: <PYOiJ.112783$I%1.31840@fx36.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: Wed, 10 Nov 2021 07:31:42 -0500
X-Received-Bytes: 5487
 by: Richard Damon - Wed, 10 Nov 2021 12:31 UTC

On 11/9/21 11:49 PM, olcott wrote:
> On 11/9/2021 9:46 AM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> // Simplified Linz Ĥ (Linz:1990:319)
>>> // Strachey(1965) CPL translated to C
>>> void P(u32 x)
>>> {
>>>    if (H(x, x))
>>>      HERE: goto HERE;
>>> }
>>>
>>> _P()
>>> [00000c36](01)  55          push ebp
>>> [00000c37](02)  8bec        mov ebp,esp
>>> [00000c39](03)  8b4508      mov eax,[ebp+08] // 2nd Param
>>> [00000c3c](01)  50          push eax
>>> [00000c3d](03)  8b4d08      mov ecx,[ebp+08] // 1st Param
>>> [00000c40](01)  51          push ecx
>>> [00000c41](05)  e820fdffff  call 00000966    // call H
>>> [00000c46](03)  83c408      add esp,+08
>>> [00000c49](02)  85c0        test eax,eax
>>> [00000c4b](02)  7402        jz 00000c4f
>>> [00000c4d](02)  ebfe        jmp 00000c4d
>>> [00000c4f](01)  5d          pop ebp
>>> [00000c50](01)  c3          ret
>>> Size in bytes:(0027) [00000c50]
>>>
>>> Begin Local Halt Decider Simulation at Machine Address:c36
>>>
>>>   machine   stack     stack     machine    assembly
>>>   address   address   data      code       language
>>>   ========  ========  ========  =========  =============
>>> [00000c36][002117ca][002117ce] 55          push ebp
>>> [00000c37][002117ca][002117ce] 8bec        mov ebp,esp
>>> [00000c39][002117ca][002117ce] 8b4508      mov eax,[ebp+08]
>>> [00000c3c][002117c6][00000c36] 50          push eax       // push P
>>> [00000c3d][002117c6][00000c36] 8b4d08      mov ecx,[ebp+08]
>>> [00000c40][002117c2][00000c36] 51          push ecx       // push P
>>> [00000c41][002117be][00000c46] e820fdffff  call 00000966  // call H(P,P)
>>
>> Aww... you stopped at the good bit.  We'd love to see H fire up a nested
>> simulation (you don't do that though do you -- you just pretend).
>>
>> And even if you want keep H all hidden and secret, you could show the
>> rest of the trace of P.  The trouble is that that will confirm, yet
>> again that H is wrong.  H(P,P) will be shown to return 0 and P(P).
>>
>> What is your plan here?  Keep posting more "versions" until someone
>> decides that false really is the right return from H when the arguments
>> represent a hating computation?  That's not going to happen because
>> (almost) everyone here knows what a halt decider should do.
>>
>> So presumably the plan in really just to keep chatting.  That's a fine
>> plan, if you enjoy the chatting.
>>
>
> In this Linz machine:
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
> it is true that the correct pure simulation of the
> input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach its final state
> whether or not the simulating halt decider at
> Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ aborted the simulation of its input.
>
> This conclusively proves that this state transition
> is correct: Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

If this is your trace of what the machine did, the we know that H^
halted, as that is what the state H^.qn does,

We aso know that in this case, H was REQUIRED to go to qy, as the
machine that its input represented applied to the input also given is
shown to halt. Thus H failed to meet its requirement.

Since H^.qx is a copy of H's q0, and we have the requirement on H that H
goes to qy if the computation its input represents halts.

Linz formal term was basically:

H wM w -> qy iff M w halts.

Since in this case M = H^, wM = <H^> and w = <H^> this becomes

H <H^> <H^> -> qy iff H^ <H^> halts.

You just showed that H^ <H^> halted as H^ <H^> goes to H^.qx <H^> <H^>
and since H <H^> <H^> goes to qn per your claim, we see that H was wrong.

>
> As long as the halt decider H reports the halt
> status of the behavior of its actual input P then
> H is necessarily correct no matter how P behaves
> in any other situation.
>

No, inputs don't halt.

H needs to report on the behavior of the machine its input REPRESENTS,
or equivalently, what this input would do when given to a REAL pure
simulator (not the partial simulator of H).

These halt, so H needs to give the halting answer to be right.

(But if you change H to do that, you have changed P, and that answer is
no longer right).

Re: Concise refutation of halting problem proofs V5 [Linz version]

<c4PiJ.91732$IW4.25504@fx48.iad>

 copy mid

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

 copy link   Newsgroups: comp.theory
Path: i2pn2.org!i2pn.org!paganini.bofh.team!news.dns-netz.com!news.freedyn.net!newsfeed.xs4all.nl!newsfeed7.news.xs4all.nl!feeder5.feed.usenet.farm!feeder1.feed.usenet.farm!feed.usenet.farm!peer02.ams4!peer.am4.highwinds-media.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx48.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.3.0
Subject: Re: Concise refutation of halting problem proofs V5 [Linz version]
Content-Language: en-US
Newsgroups: comp.theory
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
<96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
<i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com>
<fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com>
<VZWdnX77sYCZzhb8nZ2dnUU7-aWdnZ2d@giganews.com> <87bl2sw8e7.fsf@bsb.me.uk>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <87bl2sw8e7.fsf@bsb.me.uk>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 40
Message-ID: <c4PiJ.91732$IW4.25504@fx48.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: Wed, 10 Nov 2021 07:39:35 -0500
X-Received-Bytes: 2898
 by: Richard Damon - Wed, 10 Nov 2021 12:39 UTC

On 11/10/21 6:35 AM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> Here is the same thing using Peter Linz notation:
>
> Oh dear, back to talking about Turing machines...
>
>> In this Linz machine:
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>> it is true that the correct pure simulation of the
>> input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩
>
> There is no string ⟨Ĥ⟩, so there is nothing that can be simulated. You
> keep removing the clause that defines Ĥ's behaviour:
>
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
> if (and only if) Ĥ applied to ⟨Ĥ⟩ does not halt.
>
> With that clause put back, you (well, other people at least) can see
> that no TM can behave like this.
>

But, if you step back a bit and ask about the H^ based on a machine H
that CLAIMS to meet the requirements, then you can have a H^ and a <H^>.

The issue then is you need to realize that just because you have claimed
that H meets the requirements doesn't make it so (and you can't just
stipulate that it does, as that gets you back to the empty set).

Give that it is just a claim, we can use the test to see if the claim is
valid, and we see that H(<H^>,<H^>) doesn't match the actual behavior of
H^(<H^>) so we have proved the claim invalid.

This is in fact, exactly what Linz does. Peters problem is that he seems
to be having H change its definition through the proof, at one point
beng a pure simulator, and then at another point being a simulator that
aborts.

He then ignores that fact that there is no such thing as a pure
simulator that aborts its simulation.

Re: Concise refutation of halting problem proofs V5 [Linz version]

<87tugkuo79.fsf@bsb.me.uk>

 copy mid

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

 copy link   Newsgroups: comp.theory
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: ben.use...@bsb.me.uk (Ben Bacarisse)
Newsgroups: comp.theory
Subject: Re: Concise refutation of halting problem proofs V5 [Linz version]
Date: Wed, 10 Nov 2021 13:36:58 +0000
Organization: A noiseless patient Spider
Lines: 65
Message-ID: <87tugkuo79.fsf@bsb.me.uk>
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
<96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
<i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com>
<fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com>
<VZWdnX77sYCZzhb8nZ2dnUU7-aWdnZ2d@giganews.com>
<87bl2sw8e7.fsf@bsb.me.uk> <c4PiJ.91732$IW4.25504@fx48.iad>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Info: reader02.eternal-september.org; posting-host="0c198982b61379bd46027c61d9639410";
logging-data="32427"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+kWBajrhwOC+8lMm3GxrFYSZM9OyusUK4="
Cancel-Lock: sha1:ALDwn7s82ixSLubmAvDR8pYorbk=
sha1:ZiiRfhtUzXOy1vOx9it2ZTiXSIU=
X-BSB-Auth: 1.63a135c7798681a8a6f0.20211110133658GMT.87tugkuo79.fsf@bsb.me.uk
 by: Ben Bacarisse - Wed, 10 Nov 2021 13:36 UTC

Richard Damon <Richard@Damon-Family.org> writes:

> On 11/10/21 6:35 AM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> Here is the same thing using Peter Linz notation:
>> Oh dear, back to talking about Turing machines...
>>
>>> In this Linz machine:
>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>>> it is true that the correct pure simulation of the
>>> input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩
>> There is no string ⟨Ĥ⟩, so there is nothing that can be simulated. You
>> keep removing the clause that defines Ĥ's behaviour:
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>> if (and only if) Ĥ applied to ⟨Ĥ⟩ does not halt.
>> With that clause put back, you (well, other people at least) can see
>> that no TM can behave like this.
>
> But, if you step back a bit and ask about the H^ based on a machine H
> that CLAIMS to meet the requirements, then you can have a H^ and a
> <H^>.

I disagree (though it's largely philosophical at this point). From the
claim that H meets Linz's spec we can deduce all sort of things. One of
which is that there is no string <H^>. But can also deduce any other
contradiction you like.

And that's the trouble. Anything PO says about such an H^ is validly
entailed by the assumption. He can even claim that 1 == 0 follows from
"Linz's specs", and he'd be right. At some stage you have to point out
the contradictions and force PO to abandon the initial assumption.

I, for one, am fed up with trying to explain ever more silly
consequences of the initial assumption about H. The proof is simple and
the contradiction entailed is obvious.

> The issue then is you need to realize that just because you have
> claimed that H meets the requirements doesn't make it so

PO needs to realise not that the claim does not make it so but that the
claim makes it /not/ so. It's not the same thing.

> Give that it is just a claim, we can use the test to see if the claim
> is valid, and we see that H(<H^>,<H^>) doesn't match the actual
> behavior of H^(<H^>) so we have proved the claim invalid.

Indeed. So tell PO that there is no string <H^>. If there were, there
wold be a TM H^ halts if it does not and does not halt if it does.

His removal of the key condition on H^ is crucial to his attempt to keep
the discussion going. Every time that line appears, the correct
condition must be added to it do he can't get away from the fact that no
such H^ could exist.

> This is in fact, exactly what Linz does. Peters problem is that he
> seems to be having H change its definition through the proof, at one
> point beng a pure simulator, and then at another point being a
> simulator that aborts.

What proof? Proof of what? I have seen no logically connected argument
from PO that could pass the test of being even a very informal proof.

--
Ben.

Re: Concise refutation of halting problem proofs V5 [Linz version]

<A-ydnW8335m7TRb8nZ2dnUU78b3NnZ2d@giganews.com>

 copy mid

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

 copy link   Newsgroups: comp.theory sci.logic
Followup: comp.theory
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!border2.nntp.ams1.giganews.com!nntp.giganews.com!buffer2.nntp.ams1.giganews.com!buffer1.nntp.ams1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 10 Nov 2021 07:59:02 -0600
Date: Wed, 10 Nov 2021 07:59:01 -0600
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.3.0
Subject: Re: Concise refutation of halting problem proofs V5 [Linz version]
Content-Language: en-US
Newsgroups: comp.theory,sci.logic
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
<96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
<i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com>
<fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com>
<VZWdnX77sYCZzhb8nZ2dnUU7-aWdnZ2d@giganews.com> <87bl2sw8e7.fsf@bsb.me.uk>
Followup-To: comp.theory
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <87bl2sw8e7.fsf@bsb.me.uk>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <A-ydnW8335m7TRb8nZ2dnUU78b3NnZ2d@giganews.com>
Lines: 34
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-Uatn6dHB6qV1+h7nacSXFu/iGHAr8rvbU/1jNv4HRZHGEDMiSb91wckDf82Lpba60EvHh2X09V/wXaa!GdLcrfnvK0F63GWV0C++0pToeE1C0nZcbjcfZNUW0JOJmio9sytztQdgqzuN+mbsSNbNF9mDf36M!ug==
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: 2711
 by: olcott - Wed, 10 Nov 2021 13:59 UTC

On 11/10/2021 5:35 AM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> Here is the same thing using Peter Linz notation:
>
> Oh dear, back to talking about Turing machines...
>
>> In this Linz machine:
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>> it is true that the correct pure simulation of the
>> input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩
>
> There is no string ⟨Ĥ⟩, so there is nothing that can be simulated. You
> keep removing the clause that defines Ĥ's behaviour:
>
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
> if (and only if) Ĥ applied to ⟨Ĥ⟩ does not halt.
>
> With that clause put back, you (well, other people at least) can see
> that no TM can behave like this.
>
if (and only if) Ĥ.qx applied to ⟨Ĥ⟩ ⟨Ĥ⟩ does not halt.

As long as the halt decider Ĥ.qx reports the halt
status of the behavior of its actual input ⟨Ĥ⟩ ⟨Ĥ⟩ then
Ĥ.qx is necessarily correct no matter how Ĥ behaves
in any other situation.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

Re: Concise refutation of halting problem proofs V5

<28WdnZ_bI-f5TBb8nZ2dnUU7-V_NnZ2d@giganews.com>

 copy mid

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

 copy link   Newsgroups: comp.theory sci.logic
Followup: comp.theory
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!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 10 Nov 2021 08:04:20 -0600
Date: Wed, 10 Nov 2021 08:04:20 -0600
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.3.0
Subject: Re: Concise refutation of halting problem proofs V5
Content-Language: en-US
Newsgroups: comp.theory,sci.logic
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
<875yt0w7jt.fsf@bsb.me.uk>
Followup-To: comp.theory
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <875yt0w7jt.fsf@bsb.me.uk>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <28WdnZ_bI-f5TBb8nZ2dnUU7-V_NnZ2d@giganews.com>
Lines: 94
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-n7Zs3RnCmoEutUzriMDRSA7azCqD5588jhd6mxUkAaV3WSE6S/4miWTvQFuyQx3bFGEGTST8i7Y6QKn!IBG544jx0jXqokoav9pFnNZ7zz2LRfKM0Nk3+dDgEOHhMva+qAl1GLNjwzrRzDVPtaSc7B5ZfD2t!TA==
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: 5340
 by: olcott - Wed, 10 Nov 2021 14:04 UTC

On 11/10/2021 5:53 AM, Ben Bacarisse wrote:
> olcott <polcott2@gmail.com> writes:
>
>> On 11/9/2021 9:46 AM, Ben Bacarisse wrote:
>>> olcott <NoOne@NoWhere.com> writes:
>>>
>>>> // Simplified Linz Ĥ (Linz:1990:319)
>>>> // Strachey(1965) CPL translated to C
>>>> void P(u32 x)
>>>> {
>>>> if (H(x, x))
>>>> HERE: goto HERE;
>>>> }
>>>>
>>>> _P()
>>>> [00000c36](01) 55 push ebp
>>>> [00000c37](02) 8bec mov ebp,esp
>>>> [00000c39](03) 8b4508 mov eax,[ebp+08] // 2nd Param
>>>> [00000c3c](01) 50 push eax
>>>> [00000c3d](03) 8b4d08 mov ecx,[ebp+08] // 1st Param
>>>> [00000c40](01) 51 push ecx
>>>> [00000c41](05) e820fdffff call 00000966 // call H
>>>> [00000c46](03) 83c408 add esp,+08
>>>> [00000c49](02) 85c0 test eax,eax
>>>> [00000c4b](02) 7402 jz 00000c4f
>>>> [00000c4d](02) ebfe jmp 00000c4d
>>>> [00000c4f](01) 5d pop ebp
>>>> [00000c50](01) c3 ret
>>>> Size in bytes:(0027) [00000c50]
>>>>
>>>> Begin Local Halt Decider Simulation at Machine Address:c36
>>>>
>>>> machine stack stack machine assembly
>>>> address address data code language
>>>> ======== ======== ======== ========= =============
>>>> [00000c36][002117ca][002117ce] 55 push ebp
>>>> [00000c37][002117ca][002117ce] 8bec mov ebp,esp
>>>> [00000c39][002117ca][002117ce] 8b4508 mov eax,[ebp+08]
>>>> [00000c3c][002117c6][00000c36] 50 push eax // push P
>>>> [00000c3d][002117c6][00000c36] 8b4d08 mov ecx,[ebp+08]
>>>> [00000c40][002117c2][00000c36] 51 push ecx // push P
>>>> [00000c41][002117be][00000c46] e820fdffff call 00000966 // call H(P,P)
>>> Aww... you stopped at the good bit. We'd love to see H fire up a nested
>>> simulation (you don't do that though do you -- you just pretend).
>>
>> When it comes to the x86 language you are totally out of your element
>> thus no sense talking to you about this.
>
> You really want to goad me into talking about the code and not the big
> reason why are wrong!
>
> You are wrong because H(P,P) == 0 but P(P) halts. Nothing else matters.
> The fact you don't show this incorrect behaviour in your traces suggests
> you know something is wrong, but the fact you are wrong is what matters.
>
>> Even from a computer science POV we know that when one invocation of
>> H(P,P) derives the above simulation of its input that subsequent
>> directly invoked or correctly simulated invocations of H(P,P) must
>> derive this same sequence of steps of P.
>
> Waffle. H(P,P) == 0 is wrong because P(P) halts. I think this should
> be the only reply to any post you make about your code. Trying to
> explain to you why your rationalisations are wrong is, in my opinion, a
> waste of time
>
>> I would say that it seems a little goofy of you to deny this yet I
>> chalk that up to your utter cluelessness of the x86 language.
>
> That H(P,P) == 0 is wrong because P(P) halts can be understood by simply
> consulting the definition of the problem you claim to have been studying
> for decades. You can't insult your way out of the error.
>

As long as the halt decider H(P,P) reports the halt status of the
behavior of its actual input then H is necessarily correct no matter how
P(P) behaves in any other situation.

>>> What is your plan here? Keep posting more "versions" until someone
>>> decides that false really is the right return from H when the arguments
>>> represent a hating computation? That's not going to happen because
>>> (almost) everyone here knows what a halt decider should do.
>>> So presumably the plan in really just to keep chatting. That's a fine
>>> plan, if you enjoy the chatting.
>
> I'd still like to know what your plan is.
>

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

Re: Concise refutation of halting problem proofs V5 [Linz version]

<28WdnZ7bI-edTxb8nZ2dnUU7-V-dnZ2d@giganews.com>

 copy mid

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

 copy link   Newsgroups: comp.theory
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!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 10 Nov 2021 08:06:56 -0600
Date: Wed, 10 Nov 2021 08:06:57 -0600
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.3.0
Subject: Re: Concise refutation of halting problem proofs V5 [Linz version]
Content-Language: en-US
Newsgroups: comp.theory
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
<96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
<i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com>
<fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com>
<VZWdnX77sYCZzhb8nZ2dnUU7-aWdnZ2d@giganews.com> <87bl2sw8e7.fsf@bsb.me.uk>
<c4PiJ.91732$IW4.25504@fx48.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <c4PiJ.91732$IW4.25504@fx48.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <28WdnZ7bI-edTxb8nZ2dnUU7-V-dnZ2d@giganews.com>
Lines: 63
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-BZVYei/VIO/3t1eKojiRoU6PybXNyRANtlsaisUOFyDTySKSMedHvxpXadCLaRQh11G9KPTI3JUan31!wElnhNEEu7NVMRTbhP92+yy6NzjyTf31UiDQULXPQtHbNl3ZEBeaoje17xiPDQfj0cTtEAs33uN9!uA==
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: 4061
 by: olcott - Wed, 10 Nov 2021 14:06 UTC

On 11/10/2021 6:39 AM, Richard Damon wrote:
> On 11/10/21 6:35 AM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> Here is the same thing using Peter Linz notation:
>>
>> Oh dear, back to talking about Turing machines...
>>
>>> In this Linz machine:
>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>>> it is true that the correct pure simulation of the
>>> input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩
>>
>> There is no string ⟨Ĥ⟩, so there is nothing that can be simulated.  You
>> keep removing the clause that defines Ĥ's behaviour:
>>
>>    Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>>    if (and only if) Ĥ applied to ⟨Ĥ⟩ does not halt.
>>
>> With that clause put back, you (well, other people at least) can see
>> that no TM can behave like this.
>>
>
> But, if you step back a bit and ask about the H^ based on a machine H
> that CLAIMS to meet the requirements, then you can have a H^ and a <H^>.
>
> The issue then is you need to realize that just because you have claimed
> that H meets the requirements doesn't make it so (and you can't just
> stipulate that it does, as that gets you back to the empty set).
>
> Give that it is just a claim, we can use the test to see if the claim is
> valid, and we see that H(<H^>,<H^>) doesn't match the actual behavior of
> H^(<H^>) so we have proved the claim invalid.
>
> This is in fact, exactly what Linz does. Peters problem is that he seems
> to be having H change its definition through the proof, at one point
> beng a pure simulator, and then at another point being a simulator that
> aborts.
>
> He then ignores that fact that there is no such thing as a pure
> simulator that aborts its simulation.

In this Linz machine:
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
it is true that the correct pure simulation of the
input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach its final state
whether or not the simulating halt decider at
Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ aborted the simulation of its input.

This conclusively proves that this state transition
is correct: Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

As long as the halt decider Ĥ.qx reports the halt
status of the behavior of its actual input ⟨Ĥ⟩ ⟨Ĥ⟩ then
Ĥ.qx is necessarily correct no matter how Ĥ behaves
in any other situation.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

Re: Concise refutation of halting problem proofs V5 [Linz version]

<7a19a873-4220-46ea-ac99-030ce3c56981n@googlegroups.com>

 copy mid

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

 copy link   Newsgroups: comp.theory
X-Received: by 2002:a05:622a:56:: with SMTP id y22mr68715qtw.364.1636555009570;
Wed, 10 Nov 2021 06:36:49 -0800 (PST)
X-Received: by 2002:a25:9d86:: with SMTP id v6mr5496ybp.179.1636555009380;
Wed, 10 Nov 2021 06:36:49 -0800 (PST)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.theory
Date: Wed, 10 Nov 2021 06:36:49 -0800 (PST)
In-Reply-To: <87tugkuo79.fsf@bsb.me.uk>
Injection-Info: google-groups.googlegroups.com; posting-host=2a00:23a8:400a:5601:6d29:a8e:b145:4a79;
posting-account=Dz2zqgkAAADlK5MFu78bw3ab-BRFV4Qn
NNTP-Posting-Host: 2a00:23a8:400a:5601:6d29:a8e:b145:4a79
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me> <96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
<i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com> <fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com>
<VZWdnX77sYCZzhb8nZ2dnUU7-aWdnZ2d@giganews.com> <87bl2sw8e7.fsf@bsb.me.uk>
<c4PiJ.91732$IW4.25504@fx48.iad> <87tugkuo79.fsf@bsb.me.uk>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <7a19a873-4220-46ea-ac99-030ce3c56981n@googlegroups.com>
Subject: Re: Concise refutation of halting problem proofs V5 [Linz version]
From: malcolm....@gmail.com (Malcolm McLean)
Injection-Date: Wed, 10 Nov 2021 14:36:49 +0000
Content-Type: text/plain; charset="UTF-8"
Lines: 20
 by: Malcolm McLean - Wed, 10 Nov 2021 14:36 UTC

On Wednesday, 10 November 2021 at 13:37:01 UTC, Ben Bacarisse wrote:
>
> I, for one, am fed up with trying to explain ever more silly
> consequences of the initial assumption about H. The proof is simple and
> the contradiction entailed is obvious.
>
There seems to be an oscillating between a pure simulator and a halt
decider. Then recently there's been a distinction between a decider which
simulates its input and one which executes its input directly.

But the core problem remains that the halt decider returns "false" for a
machine / program which halts. I haven't see any real advance on that, and
as you say, it become repetitive pointing it out.
>
> Indeed. So tell PO that there is no string <H^>. If there were, there
> wold be a TM H^ halts if it does not and does not halt if it does.
>
There might be a assumption that H is a correct halt decider built into
PO's argument somewhere, but I haven't actually found it. However I
haven't been paying such close attention.

Re: Concise refutation of halting problem proofs V5 [Linz version]

<VI-dnQc6NMECfRb8nZ2dnUU7-NnNnZ2d@giganews.com>

 copy mid

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

 copy link   Newsgroups: comp.theory sci.logic sci.math comp.ai.philosophy
Followup: comp.theory
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!feeds.phibee-telecom.net!newsfeed.xs4all.nl!newsfeed7.news.xs4all.nl!tr1.eu1.usenetexpress.com!feeder.usenetexpress.com!tr1.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 10 Nov 2021 09:09:19 -0600
Date: Wed, 10 Nov 2021 09:09:19 -0600
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Thunderbird/91.3.0
Subject: Re: Concise refutation of halting problem proofs V5 [Linz version]
Content-Language: en-US
Newsgroups: comp.theory,sci.logic,sci.math,comp.ai.philosophy
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com> <871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me> <96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com> <i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com> <fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com> <VZWdnX77sYCZzhb8nZ2dnUU7-aWdnZ2d@giganews.com> <87bl2sw8e7.fsf@bsb.me.uk> <c4PiJ.91732$IW4.25504@fx48.iad> <87tugkuo79.fsf@bsb.me.uk> <7a19a873-4220-46ea-ac99-030ce3c56981n@googlegroups.com>
Followup-To: comp.theory
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <7a19a873-4220-46ea-ac99-030ce3c56981n@googlegroups.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <VI-dnQc6NMECfRb8nZ2dnUU7-NnNnZ2d@giganews.com>
Lines: 36
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-LDbdTKUECuoXbzOamlwjbPl/CHrHv6ZzGBvNjtoXe8JxwV5gG3y04q0qy2C0+TJM2hDrZnbVRvqWFV8!Cz6t13Fkn9qb4rcdL/ovNJvwX90qgorqrjGlCWsxyAkzYKyqC6be1bT1546LNJ2lo0Q1+s4XyoZN!vQ==
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: 3247
 by: olcott - Wed, 10 Nov 2021 15:09 UTC

On 11/10/2021 8:36 AM, Malcolm McLean wrote:
> On Wednesday, 10 November 2021 at 13:37:01 UTC, Ben Bacarisse wrote:
>>
>> I, for one, am fed up with trying to explain ever more silly
>> consequences of the initial assumption about H. The proof is simple and
>> the contradiction entailed is obvious.
>>
> There seems to be an oscillating between a pure simulator and a halt
> decider. Then recently there's been a distinction between a decider which
> simulates its input and one which executes its input directly.
>
> But the core problem remains that the halt decider returns "false" for a
> machine / program which halts. I haven't see any real advance on that, and
> as you say, it become repetitive pointing it out.

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

If the input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ never halts then the transition to ⊢* Ĥ.qn
is necessarily correct no matter what Ĥ ⟨Ĥ⟩ does. A halt decider is only
accountable for correctly deciding the halt status of its actual input.

>>
>> Indeed. So tell PO that there is no string <H^>. If there were, there
>> wold be a TM H^ halts if it does not and does not halt if it does.
>>
> There might be a assumption that H is a correct halt decider built into
> PO's argument somewhere, but I haven't actually found it. However I
> haven't been paying such close attention.
>

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

Re: Concise refutation of halting problem proofs V5 [Linz version]

<87ilx0uiem.fsf@bsb.me.uk>

 copy mid

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

 copy link   Newsgroups: comp.theory
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: ben.use...@bsb.me.uk (Ben Bacarisse)
Newsgroups: comp.theory
Subject: Re: Concise refutation of halting problem proofs V5 [Linz version]
Date: Wed, 10 Nov 2021 15:42:09 +0000
Organization: A noiseless patient Spider
Lines: 48
Message-ID: <87ilx0uiem.fsf@bsb.me.uk>
References: <QvadnQ3nvOTfFhf8nZ2dnUU7-SfNnZ2d@giganews.com>
<871r3pxrgc.fsf@bsb.me.uk> <sme6cl$ti4$1@dont-email.me>
<96809c55-4e87-4a97-a1bc-ad67ea4258aan@googlegroups.com>
<i9udnRQsSszwiBb8nZ2dnUU7-SfNnZ2d@giganews.com>
<fc2bd138-c245-4e76-b7b3-44bc1c2ae36an@googlegroups.com>
<VZWdnX77sYCZzhb8nZ2dnUU7-aWdnZ2d@giganews.com>
<87bl2sw8e7.fsf@bsb.me.uk> <c4PiJ.91732$IW4.25504@fx48.iad>
<87tugkuo79.fsf@bsb.me.uk>
<7a19a873-4220-46ea-ac99-030ce3c56981n@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Info: reader02.eternal-september.org; posting-host="0c198982b61379bd46027c61d9639410";
logging-data="392"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+2GH3p1+38T5N9z4Bhic0My7SMuNoaqM8="
Cancel-Lock: sha1:GT4hEXlDkTK29/jAGqpAeIhmfkc=
sha1:GREFitoYufZG4ISKK7K7E/vuVxw=
X-BSB-Auth: 1.eff9c0efeaa0e85a0cec.20211110154210GMT.87ilx0uiem.fsf@bsb.me.uk
 by: Ben Bacarisse - Wed, 10 Nov 2021 15:42 UTC

Malcolm McLean <malcolm.arthur.mclean@gmail.com> writes:

> On Wednesday, 10 November 2021 at 13:37:01 UTC, Ben Bacarisse wrote:
>>
>> I, for one, am fed up with trying to explain ever more silly
>> consequences of the initial assumption about H. The proof is simple and
>> the contradiction entailed is obvious.
>>
> There seems to be an oscillating between a pure simulator and a halt
> decider. Then recently there's been a distinction between a decider which
> simulates its input and one which executes its input directly.

It been the same plan for years -- H(H^,H^) == false is correct because
of what would happen if H were not what is it. It's been crystal clear
ever since the absurd idea that Halts (as it was then) was right because
of what would happen in line 15 were commented out. But PO has been
working hard to make to less clear every since.

The endless churn of ill-defined words is just an attempt to make the
wrong answer from H appear less obviously wrong.

> But the core problem remains that the halt decider returns "false" for a
> machine / program which halts. I haven't see any real advance on that, and
> as you say, it become repetitive pointing it out.

I think the repetition helps, but it's important to be clear about which
error should pointed out: when it's "Linz's H^" the error is to say
anything other than "it does not exist". If it's the code H (which
obviously exists), the error is that H(P,P) == 0 despite P(P) halting.

>> Indeed. So tell PO that there is no string <H^>. If there were, there
>> wold be a TM H^ halts if it does not and does not halt if it does.
>>
> There might be a assumption that H is a correct halt decider built into
> PO's argument somewhere, but I haven't actually found it. However I
> haven't been paying such close attention.

PO uses the same name for everything so confusion is possible, but when
he writes H^ (Ĥ) he refers to the construction in Linz. This sub-thread
started with the words "In this Linz machine:" so there is no doubt that
the H^ comes from an H that is assumed to be a halt decider.

When he's talking about his junk C code, the function H obviously
exists. The problem there is simply that it returns the wrong result in
the key case.

--
Ben.

Pages:1234
server_pubkey.txt

rocksolid light 0.9.7
clearnet tor