On 7/3/2022 10:51 AM, Mr Flibble wrote:
> On Sun, 3 Jul 2022 10:48:18 -0500
> olcott <NoOne@NoWhere.com> wrote:
>
>> On 7/3/2022 10:45 AM, Mr Flibble wrote:
>>> On Sun, 3 Jul 2022 10:30:45 -0500
>>> olcott <NoOne@NoWhere.com> wrote:
>>>
>>>> On 7/3/2022 10:21 AM, Mr Flibble wrote:
>>>>> On Sun, 3 Jul 2022 09:57:57 -0500
>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>
>>>>>> On 7/3/2022 9:27 AM, Mr Flibble wrote:
>>>>>>> On Sat, 2 Jul 2022 17:13:01 -0500
>>>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>>>
>>>>>>>> On 7/2/2022 5:05 PM, Mr Flibble wrote:
>>>>>>>>> On Sat, 2 Jul 2022 16:26:45 -0500
>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>>>>>
>>>>>>>>>> On 7/2/2022 1:44 PM, Mr Flibble wrote:
>>>>>>>>>>> On Sat, 2 Jul 2022 13:41:14 -0500
>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>>>>>>>
>>>>>>>>>>>> On 7/2/2022 1:28 PM, Mr Flibble wrote:
>>>>>>>>>>>>> On Sat, 2 Jul 2022 12:30:03 -0500
>>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>>>>>>>>>
>>>>>>>>>>>>>> On 7/2/2022 12:26 PM, Mr Flibble wrote:
>>>>>>>>>>>>>>> On Sat, 2 Jul 2022 12:15:58 -0500
>>>>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> On 7/2/2022 12:10 PM, Mr Flibble wrote:
>>>>>>>>>>>>>>>>> On Sat, 2 Jul 2022 11:42:48 -0500
>>>>>>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> On 7/2/2022 11:26 AM, Mr Flibble wrote:
>>>>>>>>>>>>>>>>>>> On Sat, 2 Jul 2022 10:34:34 -0500
>>>>>>>>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> This much more concise version of my paper focuses
>>>>>>>>>>>>>>>>>>>> on the actual execution of three fully operational
>>>>>>>>>>>>>>>>>>>> examples.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> H0 correctly determines that Infinite_Loop() never
>>>>>>>>>>>>>>>>>>>> halts H correctly determines that
>>>>>>>>>>>>>>>>>>>> Infinite_Recursion() never halts H correctly
>>>>>>>>>>>>>>>>>>>> determines that P() never halts
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> void P(u32 x)
>>>>>>>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>>>>>>> if (H(x, x))
>>>>>>>>>>>>>>>>>>>> HERE: goto HERE;
>>>>>>>>>>>>>>>>>>>> return;
>>>>>>>>>>>>>>>>>>>> }
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> int main()
>>>>>>>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>>>>>>> Output("Input_Halts = ", H((u32)P,
>>>>>>>>>>>>>>>>>>>> (u32)P)); }
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> As shown below the above P and H have the required
>>>>>>>>>>>>>>>>>>>> (halting problem) pathological relationship to each
>>>>>>>>>>>>>>>>>>>> other:
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> For any program H that might
>>>>>>>>>>>>>>>>>>>> determine if programs halt, a "pathological"
>>>>>>>>>>>>>>>>>>>> program P, called with some input,
>>>>>>>>>>>>>>>>>>>> can pass its own source and its input to
>>>>>>>>>>>>>>>>>>>> H and then specifically do the
>>>>>>>>>>>>>>>>>>>> opposite of what H predicts P will do. No H
>>>>>>>>>>>>>>>>>>>> can exist that handles this case.
>>>>>>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Halting_problem
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> I really need software engineers to verify that H
>>>>>>>>>>>>>>>>>>>> does correctly predict that its complete and
>>>>>>>>>>>>>>>>>>>> correct x86 emulation of its input would never
>>>>>>>>>>>>>>>>>>>> reach the "ret" instruction of this input.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> *Halting problem proofs refuted on the basis of
>>>>>>>>>>>>>>>>>>>> software engineering*
>>>>>>>>>>>>>>>>>>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> void Px(u32 x)
>>>>>>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>>>>>> H(x, x);
>>>>>>>>>>>>>>>>>>> return;
>>>>>>>>>>>>>>>>>>> }
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> int main()
>>>>>>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>>>>>> Output("Input_Halts = ", H((u32)Px,
>>>>>>>>>>>>>>>>>>> (u32)Px)); }
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> ...[000013e8][00102357][00000000] 83c408
>>>>>>>>>>>>>>>>>>> add esp,+08 ...[000013eb][00102353][00000000] 50
>>>>>>>>>>>>>>>>>>> push eax ...[000013ec][0010234f][00000427]
>>>>>>>>>>>>>>>>>>> 6827040000 push 00000427
>>>>>>>>>>>>>>>>>>> ---[000013f1][0010234f][00000427] e880f0ffff call
>>>>>>>>>>>>>>>>>>> 00000476 Input_Halts = 0
>>>>>>>>>>>>>>>>>>> ...[000013f6][00102357][00000000] 83c408
>>>>>>>>>>>>>>>>>>> add esp,+08 ...[000013f9][00102357][00000000] 33c0
>>>>>>>>>>>>>>>>>>> xor eax,eax ...[000013fb][0010235b][00100000] 5d
>>>>>>>>>>>>>>>>>>> pop ebp ...[000013fc][0010235f][00000004] c3 ret
>>>>>>>>>>>>>>>>>>> Number of Instructions Executed(16120)
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> As can be seen above Olcott's H decides that Px does
>>>>>>>>>>>>>>>>>>> not halt but it is obvious that Px should always
>>>>>>>>>>>>>>>>>>> halt if H is a valid halt decider that always
>>>>>>>>>>>>>>>>>>> returns a decision to its caller (Px). Olcott's H
>>>>>>>>>>>>>>>>>>> does not return a decision to its caller (Px) and
>>>>>>>>>>>>>>>>>>> is thus invalid.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> /Flibble
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Your false assumptions are directly contradicted by
>>>>>>>>>>>>>>>>>> the semantics of the x86 programming language.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> *x86 Instruction Set Reference* https://c9x.me/x86/
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> void Px(u32 x)
>>>>>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>>>>> H(x, x);
>>>>>>>>>>>>>>>>>> return;
>>>>>>>>>>>>>>>>>> }
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> int main()
>>>>>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>>>>> Output("Input_Halts = ", H((u32)Px,
>>>>>>>>>>>>>>>>>> (u32)Px)); }
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> _Px()
>>>>>>>>>>>>>>>>>> [00001192](01) 55 push ebp
>>>>>>>>>>>>>>>>>> [00001193](02) 8bec mov ebp,esp
>>>>>>>>>>>>>>>>>> [00001195](03) 8b4508 mov eax,[ebp+08]
>>>>>>>>>>>>>>>>>> [00001198](01) 50 push eax
>>>>>>>>>>>>>>>>>> [00001199](03) 8b4d08 mov ecx,[ebp+08]
>>>>>>>>>>>>>>>>>> [0000119c](01) 51 push ecx
>>>>>>>>>>>>>>>>>> [0000119d](05) e8d0fdffff call 00000f72
>>>>>>>>>>>>>>>>>> [000011a2](03) 83c408 add esp,+08
>>>>>>>>>>>>>>>>>> [000011a5](01) 5d pop ebp
>>>>>>>>>>>>>>>>>> [000011a6](01) c3 ret
>>>>>>>>>>>>>>>>>> Size in bytes:(0021) [000011a6]
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> _main()
>>>>>>>>>>>>>>>>>> [000011d2](01) 55 push ebp
>>>>>>>>>>>>>>>>>> [000011d3](02) 8bec mov ebp,esp
>>>>>>>>>>>>>>>>>> [000011d5](05) 6892110000 push 00001192
>>>>>>>>>>>>>>>>>> [000011da](05) 6892110000 push 00001192
>>>>>>>>>>>>>>>>>> [000011df](05) e88efdffff call 00000f72
>>>>>>>>>>>>>>>>>> [000011e4](03) 83c408 add esp,+08
>>>>>>>>>>>>>>>>>> [000011e7](01) 50 push eax
>>>>>>>>>>>>>>>>>> [000011e8](05) 68a3040000 push 000004a3
>>>>>>>>>>>>>>>>>> [000011ed](05) e800f3ffff call 000004f2
>>>>>>>>>>>>>>>>>> [000011f2](03) 83c408 add esp,+08
>>>>>>>>>>>>>>>>>> [000011f5](02) 33c0 xor eax,eax
>>>>>>>>>>>>>>>>>> [000011f7](01) 5d pop ebp
>>>>>>>>>>>>>>>>>> [000011f8](01) c3 ret
>>>>>>>>>>>>>>>>>> Size in bytes:(0039) [000011f8]
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> machine stack stack machine
>>>>>>>>>>>>>>>>>> assembly address address data code
>>>>>>>>>>>>>>>>>> language ======== ======== ======== =========
>>>>>>>>>>>>>>>>>> ============= [000011d2][00101f7f][00000000] 55
>>>>>>>>>>>>>>>>>> push ebp [000011d3][00101f7f][00000000] 8bec
>>>>>>>>>>>>>>>>>> mov ebp,esp [000011d5][00101f7b][00001192]
>>>>>>>>>>>>>>>>>> 6892110000 push 00001192
>>>>>>>>>>>>>>>>>> [000011da][00101f77][00001192] 6892110000 push
>>>>>>>>>>>>>>>>>> 00001192 [000011df][00101f73][000011e4] e88efdffff
>>>>>>>>>>>>>>>>>> call 00000f72
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> H: Begin Simulation Execution Trace Stored
>>>>>>>>>>>>>>>>>> at:11202b Address_of_H:f72
>>>>>>>>>>>>>>>>>> [00001192][00112017][0011201b] 55 push ebp
>>>>>>>>>>>>>>>>>> [00001193][00112017][0011201b] 8bec mov ebp,esp
>>>>>>>>>>>>>>>>>> [00001195][00112017][0011201b] 8b4508 mov
>>>>>>>>>>>>>>>>>> eax,[ebp+08] [00001198][00112013][00001192] 50
>>>>>>>>>>>>>>>>>> push eax // push Px
>>>>>>>>>>>>>>>>>> [00001199][00112013][00001192] 8b4d08 mov
>>>>>>>>>>>>>>>>>> ecx,[ebp+08] [0000119c][0011200f][00001192] 51
>>>>>>>>>>>>>>>>>> push ecx // push Px [0000119d][0011200b][000011a2]
>>>>>>>>>>>>>>>>>> e8d0fdffff call 00000f72 // call H(Px,Px) H:
>>>>>>>>>>>>>>>>>> Infinitely Recursive Simulation Detected Simulation
>>>>>>>>>>>>>>>>>> Stopped
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> H knows its own machine address and on this basis it
>>>>>>>>>>>>>>>>>> can easily examine its stored execution_trace of Px
>>>>>>>>>>>>>>>>>> (see above) to determine: (a) Px is calling H with
>>>>>>>>>>>>>>>>>> the same arguments that H was called with. (b) No
>>>>>>>>>>>>>>>>>> instructions in Px could possibly escape this
>>>>>>>>>>>>>>>>>> otherwise infinitely recursive emulation. (c) H
>>>>>>>>>>>>>>>>>> aborts its emulation of Px before its call to H is
>>>>>>>>>>>>>>>>>> emulated.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> [000011e4][00101f7f][00000000] 83c408 add esp,+08
>>>>>>>>>>>>>>>>>> [000011e7][00101f7b][00000000] 50 push eax
>>>>>>>>>>>>>>>>>> [000011e8][00101f77][000004a3] 68a3040000 push
>>>>>>>>>>>>>>>>>> 000004a3 [000011ed][00101f77][000004a3] e800f3ffff
>>>>>>>>>>>>>>>>>> call 000004f2 Input_Halts = 0
>>>>>>>>>>>>>>>>>> [000011f2][00101f7f][00000000] 83c408 add esp,+08
>>>>>>>>>>>>>>>>>> [000011f5][00101f7f][00000000] 33c0 xor eax,eax
>>>>>>>>>>>>>>>>>> [000011f7][00101f83][00000018] 5d pop ebp
>>>>>>>>>>>>>>>>>> [000011f8][00101f87][00000000] c3 ret
>>>>>>>>>>>>>>>>>> Number of Instructions Executed(880) == 13 Pages
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> If H wasn't a simulation-based halting decider then
>>>>>>>>>>>>>>>>> Px() would always halt; the infinite recursion is a
>>>>>>>>>>>>>>>>> manifestation of your invalid simulation-based halting
>>>>>>>>>>>>>>>>> decider. There is no recursion in [Strachey 1965].
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> /Flibble
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> In other words you are rejecting the concept of a
>>>>>>>>>>>>>>>> simulating halt decider even though I conclusively
>>>>>>>>>>>>>>>> proved that it does correctly determine the halt
>>>>>>>>>>>>>>>> status of: (see my new paper)
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> No I am rejecting your simulating halt decider as it
>>>>>>>>>>>>>>> gets the answer wrong for Px() which is not a
>>>>>>>>>>>>>>> pathological input. Px() halts.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> /Flibble
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> I just proved that H(Px,Px) does correctly predict that
>>>>>>>>>>>>>> its complete and correct x86 emulation of its input
>>>>>>>>>>>>>> would never reach the "ret" instruction of this input
>>>>>>>>>>>>>> because of the pathological relationship between H and
>>>>>>>>>>>>>> Px.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Wrong. Px() is not a pathological input as defined by the
>>>>>>>>>>>>> halting problem and [Strachey 1965] as it does not try to
>>>>>>>>>>>>> do the opposite of what H decides.
>>>>>>>>>>>>>
>>>>>>>>>>>>> /Flibble
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> Your lack of comprehension does not actually count as any
>>>>>>>>>>>> rebuttal at all.
>>>>>>>>>>>>
>>>>>>>>>>>> void P(u32 x)
>>>>>>>>>>>> {
>>>>>>>>>>>> if (H(x, x))
>>>>>>>>>>>> HERE: goto HERE;
>>>>>>>>>>>> return;
>>>>>>>>>>>> }
>>>>>>>>>>>>
>>>>>>>>>>>> int main()
>>>>>>>>>>>> {
>>>>>>>>>>>> Output("Input_Halts = ", H((u32)P, (u32)P));
>>>>>>>>>>>> }
>>>>>>>>>>>>
>>>>>>>>>>>> As shown below the above P and H have the required (halting
>>>>>>>>>>>> problem) pathological relationship to each other:
>>>>>>>>>>> [snip]
>>>>>>>>>>>
>>>>>>>>>>> P does but Px does not. I am talking about Px not P.
>>>>>>>>>>>
>>>>>>>>>>> void Px(u32 x)
>>>>>>>>>>> {
>>>>>>>>>>> H(x, x);
>>>>>>>>>>> return;
>>>>>>>>>>> }
>>>>>>>>>>>
>>>>>>>>>>> int main()
>>>>>>>>>>> {
>>>>>>>>>>> Output("Input_Halts = ", H((u32)Px, (u32)Px));
>>>>>>>>>>> }
>>>>>>>>>>>
>>>>>>>>>>> ...[000013e8][00102357][00000000] 83c408 add
>>>>>>>>>>> esp,+08 ...[000013eb][00102353][00000000] 50
>>>>>>>>>>> push eax ...[000013ec][0010234f][00000427] 6827040000
>>>>>>>>>>> push 00000427 ---[000013f1][0010234f][00000427] e880f0ffff
>>>>>>>>>>> call 00000476 Input_Halts = 0
>>>>>>>>>>> ...[000013f6][00102357][00000000] 83c408 add
>>>>>>>>>>> esp,+08 ...[000013f9][00102357][00000000] 33c0
>>>>>>>>>>> xor eax,eax ...[000013fb][0010235b][00100000] 5d
>>>>>>>>>>> pop ebp ...[000013fc][0010235f][00000004] c3
>>>>>>>>>>> ret Number of Instructions Executed(16120)
>>>>>>>>>>>
>>>>>>>>>>> As can be seen above Olcott's H decides that Px does not
>>>>>>>>>>> halt but it is obvious that Px should always halt if H is a
>>>>>>>>>>> valid halt decider that always returns a decision to its
>>>>>>>>>>> caller (Px). Olcott's H does not return a decision to its
>>>>>>>>>>> caller (Px) and is thus invalid.
>>>>>>>>>>>
>>>>>>>>>>> /Flibble
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> >
>>>>>>>>>>
>>>>>>>>>> Your false assumptions are directly contradicted by the
>>>>>>>>>> semantics of the x86 programming language.
>>>>>>>>>>
>>>>>>>>>> *x86 Instruction Set Reference* https://c9x.me/x86/
>>>>>>>>>>
>>>>>>>>>> void Px(u32 x)
>>>>>>>>>> {
>>>>>>>>>> H(x, x);
>>>>>>>>>> return;
>>>>>>>>>> }
>>>>>>>>>>
>>>>>>>>>> int main()
>>>>>>>>>> {
>>>>>>>>>> Output("Input_Halts = ", H((u32)Px, (u32)Px));
>>>>>>>>>> }
>>>>>>>>>>
>>>>>>>>>> _Px()
>>>>>>>>>> [00001192](01) 55 push ebp
>>>>>>>>>> [00001193](02) 8bec mov ebp,esp
>>>>>>>>>> [00001195](03) 8b4508 mov eax,[ebp+08]
>>>>>>>>>> [00001198](01) 50 push eax
>>>>>>>>>> [00001199](03) 8b4d08 mov ecx,[ebp+08]
>>>>>>>>>> [0000119c](01) 51 push ecx
>>>>>>>>>> [0000119d](05) e8d0fdffff call 00000f72
>>>>>>>>>> [000011a2](03) 83c408 add esp,+08
>>>>>>>>>> [000011a5](01) 5d pop ebp
>>>>>>>>>> [000011a6](01) c3 ret
>>>>>>>>>> Size in bytes:(0021) [000011a6]
>>>>>>>>>>
>>>>>>>>>> _main()
>>>>>>>>>> [000011d2](01) 55 push ebp
>>>>>>>>>> [000011d3](02) 8bec mov ebp,esp
>>>>>>>>>> [000011d5](05) 6892110000 push 00001192
>>>>>>>>>> [000011da](05) 6892110000 push 00001192
>>>>>>>>>> [000011df](05) e88efdffff call 00000f72
>>>>>>>>>> [000011e4](03) 83c408 add esp,+08
>>>>>>>>>> [000011e7](01) 50 push eax
>>>>>>>>>> [000011e8](05) 68a3040000 push 000004a3
>>>>>>>>>> [000011ed](05) e800f3ffff call 000004f2
>>>>>>>>>> [000011f2](03) 83c408 add esp,+08
>>>>>>>>>> [000011f5](02) 33c0 xor eax,eax
>>>>>>>>>> [000011f7](01) 5d pop ebp
>>>>>>>>>> [000011f8](01) c3 ret
>>>>>>>>>> Size in bytes:(0039) [000011f8]
>>>>>>>>>>
>>>>>>>>>> machine stack stack machine assembly
>>>>>>>>>> address address data code language
>>>>>>>>>> ======== ======== ======== ========= =============
>>>>>>>>>> [000011d2][00101f7f][00000000] 55 push ebp
>>>>>>>>>> [000011d3][00101f7f][00000000] 8bec mov ebp,esp
>>>>>>>>>> [000011d5][00101f7b][00001192] 6892110000 push 00001192
>>>>>>>>>> [000011da][00101f77][00001192] 6892110000 push 00001192
>>>>>>>>>> [000011df][00101f73][000011e4] e88efdffff call 00000f72
>>>>>>>>>>
>>>>>>>>>> H: Begin Simulation Execution Trace Stored at:11202b
>>>>>>>>>> Address_of_H:f72
>>>>>>>>>> [00001192][00112017][0011201b] 55 push ebp
>>>>>>>>>> [00001193][00112017][0011201b] 8bec mov ebp,esp
>>>>>>>>>> [00001195][00112017][0011201b] 8b4508 mov eax,[ebp+08]
>>>>>>>>>> [00001198][00112013][00001192] 50 push eax //
>>>>>>>>>> push Px [00001199][00112013][00001192] 8b4d08 mov
>>>>>>>>>> ecx,[ebp+08] [0000119c][0011200f][00001192] 51 push
>>>>>>>>>> ecx // push Px [0000119d][0011200b][000011a2]
>>>>>>>>>> e8d0fdffff call 00000f72 // call H(Px,Px) H: Infinitely
>>>>>>>>>> Recursive Simulation Detected Simulation Stopped
>>>>>>>>>>
>>>>>>>>>> H knows its own machine address and on this basis it can
>>>>>>>>>> easily examine its stored execution_trace of Px (see above)
>>>>>>>>>> to determine: (a) Px is calling H with the same arguments
>>>>>>>>>> that H was called with. (b) No instructions in Px could
>>>>>>>>>> possibly escape this otherwise infinitely recursive
>>>>>>>>>> emulation. (c) H aborts its emulation of Px before its call
>>>>>>>>>> to H is emulated.
>>>>>>>>>>
>>>>>>>>>> [000011e4][00101f7f][00000000] 83c408 add esp,+08
>>>>>>>>>> [000011e7][00101f7b][00000000] 50 push eax
>>>>>>>>>> [000011e8][00101f77][000004a3] 68a3040000 push 000004a3
>>>>>>>>>> [000011ed][00101f77][000004a3] e800f3ffff call 000004f2
>>>>>>>>>> Input_Halts = 0
>>>>>>>>>> [000011f2][00101f7f][00000000] 83c408 add esp,+08
>>>>>>>>>> [000011f5][00101f7f][00000000] 33c0 xor eax,eax
>>>>>>>>>> [000011f7][00101f83][00000018] 5d pop ebp
>>>>>>>>>> [000011f8][00101f87][00000000] c3 ret
>>>>>>>>>> Number of Instructions Executed(880) == 13 Pages
>>>>>>>>>
>>>>>>>>> I see you wish to pointlessly go around in circles. Oh well.
>>>>>>>>>
>>>>>>>>> Px() is not a pathological input as defined by the halting
>>>>>>>>> problem and [Strachey 1965] as it does not try to do the
>>>>>>>>> opposite of what H decides.
>>>>>>>>>
>>>>>>>>> Px() always halts so your H gets the answer wrong.
>>>>>>>>>
>>>>>>>>> /Flibble
>>>>>>>>
>>>>>>>> I found that my reply did not make it to all the groups so I
>>>>>>>> posted it again.
>>>>>>>>
>>>>>>>> *This general principle refutes conventional halting problem
>>>>>>>> proofs* Every simulating halt decider that correctly simulates
>>>>>>>> its input until it correctly predicts that this simulated input
>>>>>>>> would never reach its final state, correctly rejects this input
>>>>>>>> as non-halting.
>>>>>>>
>>>>>>> Your H does not "correctly predict" that Px() does reach its
>>>>>>> final state and so should accept the input as halting.
>>>>>>>
>>>>>>> /Flibble
>>>>>>>
>>>>>>
>>>>>> (x86 Instruction Set Reference* https://c9x.me/x86/
>>>>>>
>>>>>> The semantics of the x86 language conclusively proves that the
>>>>>> above code is correct. People that disagree with verified facts
>>>>>> are either incompetent or liars. Since you cannot even understand
>>>>>> that the return statement in Px is unreachable code, (to every
>>>>>> simulating halt decider H) you would be incompetent.
>>>>>
>>>>> Not EVERY simulating halt decider, only YOURS gets the answer
>>>>> wrong. Px() halts.
>>>>>
>>>>> /Flibble
>>>>>
>>>>
>>>> Since you cannot even understand that the return statement in Px is
>>>> unreachable code, (to *every simulating halt* decider H) you would
>>>> be incompetent.
>>>
>>> Not at all. If I was to design a simulating halt decider then rather
>>> than aborting the simulation at the point where P()/Px() calls H I
>>> would instead fork the simulation, returning 0 to one branch (the
>>> non-halting branch) and 1 to the other branch (the halting branch)
>>> and then continue to simulate both branches in parallel thereby
>>> getting rid of the "infinite recursion".
>>>
>>> /Flibble
>>>
>>
>> Yet that is *not* what the actual code specifies. Every function
>> called in infinite recursion is not allowed to return to its caller.
>
> The infinite recursion is an artifact of how YOU are trying to solve
> the problem; there is no infinite recursion in [Strachey 1965] and
> associated proofs.
>
> /Flibble
>

On Sun, 3 Jul 2022 11:05:21 -0500
olcott <NoOne@NoWhere.com> wrote:

> On 7/3/2022 10:51 AM, Mr Flibble wrote:
> > On Sun, 3 Jul 2022 10:48:18 -0500
> > olcott <NoOne@NoWhere.com> wrote:
> >
> >> On 7/3/2022 10:45 AM, Mr Flibble wrote:
> >>> On Sun, 3 Jul 2022 10:30:45 -0500
> >>> olcott <NoOne@NoWhere.com> wrote:
> >>>
> >>>> On 7/3/2022 10:21 AM, Mr Flibble wrote:
> >>>>> On Sun, 3 Jul 2022 09:57:57 -0500
> >>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>
> >>>>>> On 7/3/2022 9:27 AM, Mr Flibble wrote:
> >>>>>>> On Sat, 2 Jul 2022 17:13:01 -0500
> >>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>
> >>>>>>>> On 7/2/2022 5:05 PM, Mr Flibble wrote:
> >>>>>>>>> On Sat, 2 Jul 2022 16:26:45 -0500
> >>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>
> >>>>>>>>>> On 7/2/2022 1:44 PM, Mr Flibble wrote:
> >>>>>>>>>>> On Sat, 2 Jul 2022 13:41:14 -0500
> >>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>>>
> >>>>>>>>>>>> On 7/2/2022 1:28 PM, Mr Flibble wrote:
> >>>>>>>>>>>>> On Sat, 2 Jul 2022 12:30:03 -0500
> >>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>>>>>
> >>>>>>>>>>>>>> On 7/2/2022 12:26 PM, Mr Flibble wrote:
> >>>>>>>>>>>>>>> On Sat, 2 Jul 2022 12:15:58 -0500
> >>>>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>> On 7/2/2022 12:10 PM, Mr Flibble wrote:
> >>>>>>>>>>>>>>>>> On Sat, 2 Jul 2022 11:42:48 -0500
> >>>>>>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> On 7/2/2022 11:26 AM, Mr Flibble wrote:
> >>>>>>>>>>>>>>>>>>> On Sat, 2 Jul 2022 10:34:34 -0500
> >>>>>>>>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> This much more concise version of my paper
> >>>>>>>>>>>>>>>>>>>> focuses on the actual execution of three fully
> >>>>>>>>>>>>>>>>>>>> operational examples.
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> H0 correctly determines that Infinite_Loop()
> >>>>>>>>>>>>>>>>>>>> never halts H correctly determines that
> >>>>>>>>>>>>>>>>>>>> Infinite_Recursion() never halts H correctly
> >>>>>>>>>>>>>>>>>>>> determines that P() never halts
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> void P(u32 x)
> >>>>>>>>>>>>>>>>>>>> {
> >>>>>>>>>>>>>>>>>>>> if (H(x, x))
> >>>>>>>>>>>>>>>>>>>> HERE: goto HERE;
> >>>>>>>>>>>>>>>>>>>> return;
> >>>>>>>>>>>>>>>>>>>> }
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> int main()
> >>>>>>>>>>>>>>>>>>>> {
> >>>>>>>>>>>>>>>>>>>> Output("Input_Halts = ", H((u32)P,
> >>>>>>>>>>>>>>>>>>>> (u32)P)); }
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> As shown below the above P and H have the
> >>>>>>>>>>>>>>>>>>>> required (halting problem) pathological
> >>>>>>>>>>>>>>>>>>>> relationship to each other:
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> For any program H that might
> >>>>>>>>>>>>>>>>>>>> determine if programs halt, a "pathological"
> >>>>>>>>>>>>>>>>>>>> program P, called with some
> >>>>>>>>>>>>>>>>>>>> input, can pass its own source and its input to
> >>>>>>>>>>>>>>>>>>>> H and then specifically do the
> >>>>>>>>>>>>>>>>>>>> opposite of what H predicts P will do. No H
> >>>>>>>>>>>>>>>>>>>> can exist that handles this case.
> >>>>>>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Halting_problem
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> I really need software engineers to verify that H
> >>>>>>>>>>>>>>>>>>>> does correctly predict that its complete and
> >>>>>>>>>>>>>>>>>>>> correct x86 emulation of its input would never
> >>>>>>>>>>>>>>>>>>>> reach the "ret" instruction of this input.
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> *Halting problem proofs refuted on the basis of
> >>>>>>>>>>>>>>>>>>>> software engineering*
> >>>>>>>>>>>>>>>>>>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>> void Px(u32 x)
> >>>>>>>>>>>>>>>>>>> {
> >>>>>>>>>>>>>>>>>>> H(x, x);
> >>>>>>>>>>>>>>>>>>> return;
> >>>>>>>>>>>>>>>>>>> }
> >>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>> int main()
> >>>>>>>>>>>>>>>>>>> {
> >>>>>>>>>>>>>>>>>>> Output("Input_Halts = ", H((u32)Px,
> >>>>>>>>>>>>>>>>>>> (u32)Px)); }
> >>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>> ...[000013e8][00102357][00000000] 83c408
> >>>>>>>>>>>>>>>>>>> add esp,+08 ...[000013eb][00102353][00000000] 50
> >>>>>>>>>>>>>>>>>>> push eax ...[000013ec][0010234f][00000427]
> >>>>>>>>>>>>>>>>>>> 6827040000 push 00000427
> >>>>>>>>>>>>>>>>>>> ---[000013f1][0010234f][00000427] e880f0ffff call
> >>>>>>>>>>>>>>>>>>> 00000476 Input_Halts = 0
> >>>>>>>>>>>>>>>>>>> ...[000013f6][00102357][00000000] 83c408
> >>>>>>>>>>>>>>>>>>> add esp,+08 ...[000013f9][00102357][00000000] 33c0
> >>>>>>>>>>>>>>>>>>> xor eax,eax ...[000013fb][0010235b][00100000] 5d
> >>>>>>>>>>>>>>>>>>> pop ebp ...[000013fc][0010235f][00000004] c3 ret
> >>>>>>>>>>>>>>>>>>> Number of Instructions Executed(16120)
> >>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>> As can be seen above Olcott's H decides that Px
> >>>>>>>>>>>>>>>>>>> does not halt but it is obvious that Px should
> >>>>>>>>>>>>>>>>>>> always halt if H is a valid halt decider that
> >>>>>>>>>>>>>>>>>>> always returns a decision to its caller (Px).
> >>>>>>>>>>>>>>>>>>> Olcott's H does not return a decision to its
> >>>>>>>>>>>>>>>>>>> caller (Px) and is thus invalid.
> >>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>> /Flibble
> >>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> Your false assumptions are directly contradicted by
> >>>>>>>>>>>>>>>>>> the semantics of the x86 programming language.
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> *x86 Instruction Set Reference*
> >>>>>>>>>>>>>>>>>> https://c9x.me/x86/
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> void Px(u32 x)
> >>>>>>>>>>>>>>>>>> {
> >>>>>>>>>>>>>>>>>> H(x, x);
> >>>>>>>>>>>>>>>>>> return;
> >>>>>>>>>>>>>>>>>> }
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> int main()
> >>>>>>>>>>>>>>>>>> {
> >>>>>>>>>>>>>>>>>> Output("Input_Halts = ", H((u32)Px,
> >>>>>>>>>>>>>>>>>> (u32)Px)); }
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> _Px()
> >>>>>>>>>>>>>>>>>> [00001192](01) 55 push ebp
> >>>>>>>>>>>>>>>>>> [00001193](02) 8bec mov ebp,esp
> >>>>>>>>>>>>>>>>>> [00001195](03) 8b4508 mov eax,[ebp+08]
> >>>>>>>>>>>>>>>>>> [00001198](01) 50 push eax
> >>>>>>>>>>>>>>>>>> [00001199](03) 8b4d08 mov ecx,[ebp+08]
> >>>>>>>>>>>>>>>>>> [0000119c](01) 51 push ecx
> >>>>>>>>>>>>>>>>>> [0000119d](05) e8d0fdffff call 00000f72
> >>>>>>>>>>>>>>>>>> [000011a2](03) 83c408 add esp,+08
> >>>>>>>>>>>>>>>>>> [000011a5](01) 5d pop ebp
> >>>>>>>>>>>>>>>>>> [000011a6](01) c3 ret
> >>>>>>>>>>>>>>>>>> Size in bytes:(0021) [000011a6]
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> _main()
> >>>>>>>>>>>>>>>>>> [000011d2](01) 55 push ebp
> >>>>>>>>>>>>>>>>>> [000011d3](02) 8bec mov ebp,esp
> >>>>>>>>>>>>>>>>>> [000011d5](05) 6892110000 push 00001192
> >>>>>>>>>>>>>>>>>> [000011da](05) 6892110000 push 00001192
> >>>>>>>>>>>>>>>>>> [000011df](05) e88efdffff call 00000f72
> >>>>>>>>>>>>>>>>>> [000011e4](03) 83c408 add esp,+08
> >>>>>>>>>>>>>>>>>> [000011e7](01) 50 push eax
> >>>>>>>>>>>>>>>>>> [000011e8](05) 68a3040000 push 000004a3
> >>>>>>>>>>>>>>>>>> [000011ed](05) e800f3ffff call 000004f2
> >>>>>>>>>>>>>>>>>> [000011f2](03) 83c408 add esp,+08
> >>>>>>>>>>>>>>>>>> [000011f5](02) 33c0 xor eax,eax
> >>>>>>>>>>>>>>>>>> [000011f7](01) 5d pop ebp
> >>>>>>>>>>>>>>>>>> [000011f8](01) c3 ret
> >>>>>>>>>>>>>>>>>> Size in bytes:(0039) [000011f8]
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> machine stack stack machine
> >>>>>>>>>>>>>>>>>> assembly address address data code
> >>>>>>>>>>>>>>>>>> language ======== ======== ======== =========
> >>>>>>>>>>>>>>>>>> ============= [000011d2][00101f7f][00000000] 55
> >>>>>>>>>>>>>>>>>> push ebp [000011d3][00101f7f][00000000] 8bec
> >>>>>>>>>>>>>>>>>> mov ebp,esp [000011d5][00101f7b][00001192]
> >>>>>>>>>>>>>>>>>> 6892110000 push 00001192
> >>>>>>>>>>>>>>>>>> [000011da][00101f77][00001192] 6892110000 push
> >>>>>>>>>>>>>>>>>> 00001192 [000011df][00101f73][000011e4] e88efdffff
> >>>>>>>>>>>>>>>>>> call 00000f72
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> H: Begin Simulation Execution Trace Stored
> >>>>>>>>>>>>>>>>>> at:11202b Address_of_H:f72
> >>>>>>>>>>>>>>>>>> [00001192][00112017][0011201b] 55 push ebp
> >>>>>>>>>>>>>>>>>> [00001193][00112017][0011201b] 8bec mov
> >>>>>>>>>>>>>>>>>> ebp,esp [00001195][00112017][0011201b] 8b4508
> >>>>>>>>>>>>>>>>>> mov eax,[ebp+08] [00001198][00112013][00001192] 50
> >>>>>>>>>>>>>>>>>> push eax // push Px
> >>>>>>>>>>>>>>>>>> [00001199][00112013][00001192] 8b4d08 mov
> >>>>>>>>>>>>>>>>>> ecx,[ebp+08] [0000119c][0011200f][00001192] 51
> >>>>>>>>>>>>>>>>>> push ecx // push Px
> >>>>>>>>>>>>>>>>>> [0000119d][0011200b][000011a2] e8d0fdffff call
> >>>>>>>>>>>>>>>>>> 00000f72 // call H(Px,Px) H: Infinitely Recursive
> >>>>>>>>>>>>>>>>>> Simulation Detected Simulation Stopped
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> H knows its own machine address and on this basis
> >>>>>>>>>>>>>>>>>> it can easily examine its stored execution_trace
> >>>>>>>>>>>>>>>>>> of Px (see above) to determine: (a) Px is calling
> >>>>>>>>>>>>>>>>>> H with the same arguments that H was called with.
> >>>>>>>>>>>>>>>>>> (b) No instructions in Px could possibly escape
> >>>>>>>>>>>>>>>>>> this otherwise infinitely recursive emulation. (c)
> >>>>>>>>>>>>>>>>>> H aborts its emulation of Px before its call to H
> >>>>>>>>>>>>>>>>>> is emulated.
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> [000011e4][00101f7f][00000000] 83c408 add
> >>>>>>>>>>>>>>>>>> esp,+08 [000011e7][00101f7b][00000000] 50
> >>>>>>>>>>>>>>>>>> push eax [000011e8][00101f77][000004a3] 68a3040000
> >>>>>>>>>>>>>>>>>> push 000004a3 [000011ed][00101f77][000004a3]
> >>>>>>>>>>>>>>>>>> e800f3ffff call 000004f2 Input_Halts = 0
> >>>>>>>>>>>>>>>>>> [000011f2][00101f7f][00000000] 83c408 add
> >>>>>>>>>>>>>>>>>> esp,+08 [000011f5][00101f7f][00000000] 33c0
> >>>>>>>>>>>>>>>>>> xor eax,eax [000011f7][00101f83][00000018] 5d
> >>>>>>>>>>>>>>>>>> pop ebp [000011f8][00101f87][00000000] c3
> >>>>>>>>>>>>>>>>>> ret Number of Instructions Executed(880) == 13
> >>>>>>>>>>>>>>>>>> Pages
> >>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>> If H wasn't a simulation-based halting decider then
> >>>>>>>>>>>>>>>>> Px() would always halt; the infinite recursion is a
> >>>>>>>>>>>>>>>>> manifestation of your invalid simulation-based
> >>>>>>>>>>>>>>>>> halting decider. There is no recursion in
> >>>>>>>>>>>>>>>>> [Strachey 1965].
> >>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>> /Flibble
> >>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>> In other words you are rejecting the concept of a
> >>>>>>>>>>>>>>>> simulating halt decider even though I conclusively
> >>>>>>>>>>>>>>>> proved that it does correctly determine the halt
> >>>>>>>>>>>>>>>> status of: (see my new paper)
> >>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>> No I am rejecting your simulating halt decider as it
> >>>>>>>>>>>>>>> gets the answer wrong for Px() which is not a
> >>>>>>>>>>>>>>> pathological input. Px() halts.
> >>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>> /Flibble
> >>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>
> >>>>>>>>>>>>>> I just proved that H(Px,Px) does correctly predict that
> >>>>>>>>>>>>>> its complete and correct x86 emulation of its input
> >>>>>>>>>>>>>> would never reach the "ret" instruction of this input
> >>>>>>>>>>>>>> because of the pathological relationship between H and
> >>>>>>>>>>>>>> Px.
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> Wrong. Px() is not a pathological input as defined by
> >>>>>>>>>>>>> the halting problem and [Strachey 1965] as it does not
> >>>>>>>>>>>>> try to do the opposite of what H decides.
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> /Flibble
> >>>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>> Your lack of comprehension does not actually count as any
> >>>>>>>>>>>> rebuttal at all.
> >>>>>>>>>>>>
> >>>>>>>>>>>> void P(u32 x)
> >>>>>>>>>>>> {
> >>>>>>>>>>>> if (H(x, x))
> >>>>>>>>>>>> HERE: goto HERE;
> >>>>>>>>>>>> return;
> >>>>>>>>>>>> }
> >>>>>>>>>>>>
> >>>>>>>>>>>> int main()
> >>>>>>>>>>>> {
> >>>>>>>>>>>> Output("Input_Halts = ", H((u32)P, (u32)P));
> >>>>>>>>>>>> }
> >>>>>>>>>>>>
> >>>>>>>>>>>> As shown below the above P and H have the required
> >>>>>>>>>>>> (halting problem) pathological relationship to each
> >>>>>>>>>>>> other:
> >>>>>>>>>>> [snip]
> >>>>>>>>>>>
> >>>>>>>>>>> P does but Px does not. I am talking about Px not P.
> >>>>>>>>>>>
> >>>>>>>>>>> void Px(u32 x)
> >>>>>>>>>>> {
> >>>>>>>>>>> H(x, x);
> >>>>>>>>>>> return;
> >>>>>>>>>>> }
> >>>>>>>>>>>
> >>>>>>>>>>> int main()
> >>>>>>>>>>> {
> >>>>>>>>>>> Output("Input_Halts = ", H((u32)Px, (u32)Px));
> >>>>>>>>>>> }
> >>>>>>>>>>>
> >>>>>>>>>>> ...[000013e8][00102357][00000000] 83c408 add
> >>>>>>>>>>> esp,+08 ...[000013eb][00102353][00000000] 50
> >>>>>>>>>>> push eax ...[000013ec][0010234f][00000427] 6827040000
> >>>>>>>>>>> push 00000427 ---[000013f1][0010234f][00000427] e880f0ffff
> >>>>>>>>>>> call 00000476 Input_Halts = 0
> >>>>>>>>>>> ...[000013f6][00102357][00000000] 83c408 add
> >>>>>>>>>>> esp,+08 ...[000013f9][00102357][00000000] 33c0
> >>>>>>>>>>> xor eax,eax ...[000013fb][0010235b][00100000] 5d
> >>>>>>>>>>> pop ebp ...[000013fc][0010235f][00000004] c3
> >>>>>>>>>>> ret Number of Instructions Executed(16120)
> >>>>>>>>>>>
> >>>>>>>>>>> As can be seen above Olcott's H decides that Px does not
> >>>>>>>>>>> halt but it is obvious that Px should always halt if H is
> >>>>>>>>>>> a valid halt decider that always returns a decision to its
> >>>>>>>>>>> caller (Px). Olcott's H does not return a decision to its
> >>>>>>>>>>> caller (Px) and is thus invalid.
> >>>>>>>>>>>
> >>>>>>>>>>> /Flibble
> >>>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>> >
> >>>>>>>>>>
> >>>>>>>>>> Your false assumptions are directly contradicted by the
> >>>>>>>>>> semantics of the x86 programming language.
> >>>>>>>>>>
> >>>>>>>>>> *x86 Instruction Set Reference* https://c9x.me/x86/
> >>>>>>>>>>
> >>>>>>>>>> void Px(u32 x)
> >>>>>>>>>> {
> >>>>>>>>>> H(x, x);
> >>>>>>>>>> return;
> >>>>>>>>>> }
> >>>>>>>>>>
> >>>>>>>>>> int main()
> >>>>>>>>>> {
> >>>>>>>>>> Output("Input_Halts = ", H((u32)Px, (u32)Px));
> >>>>>>>>>> }
> >>>>>>>>>>
> >>>>>>>>>> _Px()
> >>>>>>>>>> [00001192](01) 55 push ebp
> >>>>>>>>>> [00001193](02) 8bec mov ebp,esp
> >>>>>>>>>> [00001195](03) 8b4508 mov eax,[ebp+08]
> >>>>>>>>>> [00001198](01) 50 push eax
> >>>>>>>>>> [00001199](03) 8b4d08 mov ecx,[ebp+08]
> >>>>>>>>>> [0000119c](01) 51 push ecx
> >>>>>>>>>> [0000119d](05) e8d0fdffff call 00000f72
> >>>>>>>>>> [000011a2](03) 83c408 add esp,+08
> >>>>>>>>>> [000011a5](01) 5d pop ebp
> >>>>>>>>>> [000011a6](01) c3 ret
> >>>>>>>>>> Size in bytes:(0021) [000011a6]
> >>>>>>>>>>
> >>>>>>>>>> _main()
> >>>>>>>>>> [000011d2](01) 55 push ebp
> >>>>>>>>>> [000011d3](02) 8bec mov ebp,esp
> >>>>>>>>>> [000011d5](05) 6892110000 push 00001192
> >>>>>>>>>> [000011da](05) 6892110000 push 00001192
> >>>>>>>>>> [000011df](05) e88efdffff call 00000f72
> >>>>>>>>>> [000011e4](03) 83c408 add esp,+08
> >>>>>>>>>> [000011e7](01) 50 push eax
> >>>>>>>>>> [000011e8](05) 68a3040000 push 000004a3
> >>>>>>>>>> [000011ed](05) e800f3ffff call 000004f2
> >>>>>>>>>> [000011f2](03) 83c408 add esp,+08
> >>>>>>>>>> [000011f5](02) 33c0 xor eax,eax
> >>>>>>>>>> [000011f7](01) 5d pop ebp
> >>>>>>>>>> [000011f8](01) c3 ret
> >>>>>>>>>> Size in bytes:(0039) [000011f8]
> >>>>>>>>>>
> >>>>>>>>>> machine stack stack machine assembly
> >>>>>>>>>> address address data code language
> >>>>>>>>>> ======== ======== ======== =========
> >>>>>>>>>> ============= [000011d2][00101f7f][00000000] 55
> >>>>>>>>>> push ebp [000011d3][00101f7f][00000000] 8bec mov
> >>>>>>>>>> ebp,esp [000011d5][00101f7b][00001192] 6892110000 push
> >>>>>>>>>> 00001192 [000011da][00101f77][00001192] 6892110000 push
> >>>>>>>>>> 00001192 [000011df][00101f73][000011e4] e88efdffff call
> >>>>>>>>>> 00000f72
> >>>>>>>>>>
> >>>>>>>>>> H: Begin Simulation Execution Trace Stored at:11202b
> >>>>>>>>>> Address_of_H:f72
> >>>>>>>>>> [00001192][00112017][0011201b] 55 push ebp
> >>>>>>>>>> [00001193][00112017][0011201b] 8bec mov ebp,esp
> >>>>>>>>>> [00001195][00112017][0011201b] 8b4508 mov eax,[ebp+08]
> >>>>>>>>>> [00001198][00112013][00001192] 50 push eax //
> >>>>>>>>>> push Px [00001199][00112013][00001192] 8b4d08 mov
> >>>>>>>>>> ecx,[ebp+08] [0000119c][0011200f][00001192] 51 push
> >>>>>>>>>> ecx // push Px [0000119d][0011200b][000011a2]
> >>>>>>>>>> e8d0fdffff call 00000f72 // call H(Px,Px) H: Infinitely
> >>>>>>>>>> Recursive Simulation Detected Simulation Stopped
> >>>>>>>>>>
> >>>>>>>>>> H knows its own machine address and on this basis it can
> >>>>>>>>>> easily examine its stored execution_trace of Px (see above)
> >>>>>>>>>> to determine: (a) Px is calling H with the same arguments
> >>>>>>>>>> that H was called with. (b) No instructions in Px could
> >>>>>>>>>> possibly escape this otherwise infinitely recursive
> >>>>>>>>>> emulation. (c) H aborts its emulation of Px before its call
> >>>>>>>>>> to H is emulated.
> >>>>>>>>>>
> >>>>>>>>>> [000011e4][00101f7f][00000000] 83c408 add esp,+08
> >>>>>>>>>> [000011e7][00101f7b][00000000] 50 push eax
> >>>>>>>>>> [000011e8][00101f77][000004a3] 68a3040000 push 000004a3
> >>>>>>>>>> [000011ed][00101f77][000004a3] e800f3ffff call 000004f2
> >>>>>>>>>> Input_Halts = 0
> >>>>>>>>>> [000011f2][00101f7f][00000000] 83c408 add esp,+08
> >>>>>>>>>> [000011f5][00101f7f][00000000] 33c0 xor eax,eax
> >>>>>>>>>> [000011f7][00101f83][00000018] 5d pop ebp
> >>>>>>>>>> [000011f8][00101f87][00000000] c3 ret
> >>>>>>>>>> Number of Instructions Executed(880) == 13 Pages
> >>>>>>>>>
> >>>>>>>>> I see you wish to pointlessly go around in circles. Oh well.
> >>>>>>>>>
> >>>>>>>>> Px() is not a pathological input as defined by the halting
> >>>>>>>>> problem and [Strachey 1965] as it does not try to do the
> >>>>>>>>> opposite of what H decides.
> >>>>>>>>>
> >>>>>>>>> Px() always halts so your H gets the answer wrong.
> >>>>>>>>>
> >>>>>>>>> /Flibble
> >>>>>>>>
> >>>>>>>> I found that my reply did not make it to all the groups so I
> >>>>>>>> posted it again.
> >>>>>>>>
> >>>>>>>> *This general principle refutes conventional halting problem
> >>>>>>>> proofs* Every simulating halt decider that correctly
> >>>>>>>> simulates its input until it correctly predicts that this
> >>>>>>>> simulated input would never reach its final state, correctly
> >>>>>>>> rejects this input as non-halting.
> >>>>>>>
> >>>>>>> Your H does not "correctly predict" that Px() does reach its
> >>>>>>> final state and so should accept the input as halting.
> >>>>>>>
> >>>>>>> /Flibble
> >>>>>>>
> >>>>>>
> >>>>>> (x86 Instruction Set Reference* https://c9x.me/x86/
> >>>>>>
> >>>>>> The semantics of the x86 language conclusively proves that the
> >>>>>> above code is correct. People that disagree with verified facts
> >>>>>> are either incompetent or liars. Since you cannot even
> >>>>>> understand that the return statement in Px is unreachable
> >>>>>> code, (to every simulating halt decider H) you would be
> >>>>>> incompetent.
> >>>>>
> >>>>> Not EVERY simulating halt decider, only YOURS gets the answer
> >>>>> wrong. Px() halts.
> >>>>>
> >>>>> /Flibble
> >>>>>
> >>>>
> >>>> Since you cannot even understand that the return statement in Px
> >>>> is unreachable code, (to *every simulating halt* decider H) you
> >>>> would be incompetent.
> >>>
> >>> Not at all. If I was to design a simulating halt decider then
> >>> rather than aborting the simulation at the point where P()/Px()
> >>> calls H I would instead fork the simulation, returning 0 to one
> >>> branch (the non-halting branch) and 1 to the other branch (the
> >>> halting branch) and then continue to simulate both branches in
> >>> parallel thereby getting rid of the "infinite recursion".
> >>>
> >>> /Flibble
> >>>
> >>
> >> Yet that is *not* what the actual code specifies. Every function
> >> called in infinite recursion is not allowed to return to its
> >> caller.
> >
> > The infinite recursion is an artifact of how YOU are trying to solve
> > the problem; there is no infinite recursion in [Strachey 1965] and
> > associated proofs.
> >
> > /Flibble
> >
>
> The halting problem expressly allows every algorithm in the universe
> as long as it correctly predicts the behavior of the input.

On 7/3/22 10:57 AM, olcott wrote:
> On 7/3/2022 9:27 AM, Mr Flibble wrote:
>> On Sat, 2 Jul 2022 17:13:01 -0500
>> olcott <NoOne@NoWhere.com> wrote:
>>
>>> On 7/2/2022 5:05 PM, Mr Flibble wrote:
>>>> On Sat, 2 Jul 2022 16:26:45 -0500
>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>> On 7/2/2022 1:44 PM, Mr Flibble wrote:
>>>>>> On Sat, 2 Jul 2022 13:41:14 -0500
>>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>>> On 7/2/2022 1:28 PM, Mr Flibble wrote:
>>>>>>>> On Sat, 2 Jul 2022 12:30:03 -0500
>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>>>>> On 7/2/2022 12:26 PM, Mr Flibble wrote:
>>>>>>>>>> On Sat, 2 Jul 2022 12:15:58 -0500
>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>>>>>>> On 7/2/2022 12:10 PM, Mr Flibble wrote:
>>>>>>>>>>>> On Sat, 2 Jul 2022 11:42:48 -0500
>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>>>>>>>>> On 7/2/2022 11:26 AM, Mr Flibble wrote:
>>>>>>>>>>>>>> On Sat, 2 Jul 2022 10:34:34 -0500
>>>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
>>>>>>>>>>>>>>> This much more concise version of my paper focuses on the
>>>>>>>>>>>>>>> actual execution of three fully operational examples.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> H0 correctly determines that Infinite_Loop() never halts
>>>>>>>>>>>>>>> H correctly determines that Infinite_Recursion() never
>>>>>>>>>>>>>>> halts H correctly determines that P() never halts
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> void P(u32 x)
>>>>>>>>>>>>>>>          {
>>>>>>>>>>>>>>>           if (H(x, x))
>>>>>>>>>>>>>>>             HERE: goto HERE;
>>>>>>>>>>>>>>>           return;
>>>>>>>>>>>>>>>          }
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> int main()
>>>>>>>>>>>>>>>          {
>>>>>>>>>>>>>>>           Output("Input_Halts = ", H((u32)P, (u32)P));
>>>>>>>>>>>>>>>          }
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> As shown below the above P and H have the required
>>>>>>>>>>>>>>> (halting problem) pathological relationship to each
>>>>>>>>>>>>>>> other:
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>              For any program H that might determine if
>>>>>>>>>>>>>>> programs halt, a "pathological"
>>>>>>>>>>>>>>>              program P, called with some input, can pass
>>>>>>>>>>>>>>> its own source and its input to
>>>>>>>>>>>>>>>              H and then specifically do the opposite of
>>>>>>>>>>>>>>> what H predicts P will do. No H
>>>>>>>>>>>>>>>              can exist that handles this case.
>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Halting_problem
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> I really need software engineers to verify that H does
>>>>>>>>>>>>>>> correctly predict that its complete and correct x86
>>>>>>>>>>>>>>> emulation of its input would never reach the "ret"
>>>>>>>>>>>>>>> instruction of this input.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> *Halting problem proofs refuted on the basis of software
>>>>>>>>>>>>>>> engineering*
>>>>>>>>>>>>>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> void Px(u32 x)
>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>           H(x, x);
>>>>>>>>>>>>>>           return;
>>>>>>>>>>>>>> }
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> int main()
>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>           Output("Input_Halts = ", H((u32)Px, (u32)Px));
>>>>>>>>>>>>>> }
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> ...[000013e8][00102357][00000000] 83c408          add
>>>>>>>>>>>>>> esp,+08 ...[000013eb][00102353][00000000] 50
>>>>>>>>>>>>>> push eax ...[000013ec][0010234f][00000427] 6827040000
>>>>>>>>>>>>>> push 00000427 ---[000013f1][0010234f][00000427] e880f0ffff
>>>>>>>>>>>>>> call 00000476 Input_Halts = 0
>>>>>>>>>>>>>> ...[000013f6][00102357][00000000] 83c408          add
>>>>>>>>>>>>>> esp,+08 ...[000013f9][00102357][00000000] 33c0
>>>>>>>>>>>>>> xor eax,eax ...[000013fb][0010235b][00100000] 5d
>>>>>>>>>>>>>>     pop ebp ...[000013fc][0010235f][00000004] c3
>>>>>>>>>>>>>> ret Number of Instructions Executed(16120)
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> As can be seen above Olcott's H decides that Px does not
>>>>>>>>>>>>>> halt but it is obvious that Px should always halt if H is
>>>>>>>>>>>>>> a valid halt decider that always returns a decision to its
>>>>>>>>>>>>>> caller (Px). Olcott's H does not return a decision to its
>>>>>>>>>>>>>> caller (Px) and is thus invalid.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> /Flibble
>>>>>>>>>>>>>
>>>>>>>>>>>>> Your false assumptions are directly contradicted by the
>>>>>>>>>>>>> semantics of the x86 programming language.
>>>>>>>>>>>>>
>>>>>>>>>>>>> *x86 Instruction Set Reference*  https://c9x.me/x86/
>>>>>>>>>>>>>
>>>>>>>>>>>>> void Px(u32 x)
>>>>>>>>>>>>> {
>>>>>>>>>>>>>          H(x, x);
>>>>>>>>>>>>>          return;
>>>>>>>>>>>>> }
>>>>>>>>>>>>>
>>>>>>>>>>>>> int main()
>>>>>>>>>>>>> {
>>>>>>>>>>>>>          Output("Input_Halts = ", H((u32)Px, (u32)Px));
>>>>>>>>>>>>> }
>>>>>>>>>>>>>
>>>>>>>>>>>>> _Px()
>>>>>>>>>>>>> [00001192](01)  55         push ebp
>>>>>>>>>>>>> [00001193](02)  8bec       mov ebp,esp
>>>>>>>>>>>>> [00001195](03)  8b4508     mov eax,[ebp+08]
>>>>>>>>>>>>> [00001198](01)  50         push eax
>>>>>>>>>>>>> [00001199](03)  8b4d08     mov ecx,[ebp+08]
>>>>>>>>>>>>> [0000119c](01)  51         push ecx
>>>>>>>>>>>>> [0000119d](05)  e8d0fdffff call 00000f72
>>>>>>>>>>>>> [000011a2](03)  83c408     add esp,+08
>>>>>>>>>>>>> [000011a5](01)  5d         pop ebp
>>>>>>>>>>>>> [000011a6](01)  c3         ret
>>>>>>>>>>>>> Size in bytes:(0021) [000011a6]
>>>>>>>>>>>>>
>>>>>>>>>>>>> _main()
>>>>>>>>>>>>> [000011d2](01)  55         push ebp
>>>>>>>>>>>>> [000011d3](02)  8bec       mov ebp,esp
>>>>>>>>>>>>> [000011d5](05)  6892110000 push 00001192
>>>>>>>>>>>>> [000011da](05)  6892110000 push 00001192
>>>>>>>>>>>>> [000011df](05)  e88efdffff call 00000f72
>>>>>>>>>>>>> [000011e4](03)  83c408     add esp,+08
>>>>>>>>>>>>> [000011e7](01)  50         push eax
>>>>>>>>>>>>> [000011e8](05)  68a3040000 push 000004a3
>>>>>>>>>>>>> [000011ed](05)  e800f3ffff call 000004f2
>>>>>>>>>>>>> [000011f2](03)  83c408     add esp,+08
>>>>>>>>>>>>> [000011f5](02)  33c0       xor eax,eax
>>>>>>>>>>>>> [000011f7](01)  5d         pop ebp
>>>>>>>>>>>>> [000011f8](01)  c3         ret
>>>>>>>>>>>>> Size in bytes:(0039) [000011f8]
>>>>>>>>>>>>>
>>>>>>>>>>>>>         machine   stack     stack     machine    assembly
>>>>>>>>>>>>>         address   address   data      code       language
>>>>>>>>>>>>>         ========  ========  ========  =========
>>>>>>>>>>>>> ============= [000011d2][00101f7f][00000000] 55
>>>>>>>>>>>>> push ebp [000011d3][00101f7f][00000000] 8bec       mov
>>>>>>>>>>>>> ebp,esp [000011d5][00101f7b][00001192] 6892110000 push
>>>>>>>>>>>>> 00001192 [000011da][00101f77][00001192] 6892110000 push
>>>>>>>>>>>>> 00001192 [000011df][00101f73][000011e4] e88efdffff call
>>>>>>>>>>>>> 00000f72
>>>>>>>>>>>>>
>>>>>>>>>>>>> H: Begin Simulation   Execution Trace Stored at:11202b
>>>>>>>>>>>>> Address_of_H:f72
>>>>>>>>>>>>> [00001192][00112017][0011201b] 55         push ebp
>>>>>>>>>>>>> [00001193][00112017][0011201b] 8bec       mov ebp,esp
>>>>>>>>>>>>> [00001195][00112017][0011201b] 8b4508     mov eax,[ebp+08]
>>>>>>>>>>>>> [00001198][00112013][00001192] 50         push eax      //
>>>>>>>>>>>>> push Px [00001199][00112013][00001192] 8b4d08     mov
>>>>>>>>>>>>> ecx,[ebp+08] [0000119c][0011200f][00001192] 51         push
>>>>>>>>>>>>> ecx      // push Px [0000119d][0011200b][000011a2]
>>>>>>>>>>>>> e8d0fdffff call 00000f72 // call H(Px,Px) H: Infinitely
>>>>>>>>>>>>> Recursive Simulation Detected Simulation Stopped
>>>>>>>>>>>>>
>>>>>>>>>>>>> H knows its own machine address and on this basis it can
>>>>>>>>>>>>> easily examine its stored execution_trace of Px (see above)
>>>>>>>>>>>>> to determine: (a) Px is calling H with the same arguments
>>>>>>>>>>>>> that H was called with. (b) No instructions in Px could
>>>>>>>>>>>>> possibly escape this otherwise infinitely recursive
>>>>>>>>>>>>> emulation. (c) H aborts its emulation of Px before its call
>>>>>>>>>>>>> to H is emulated.
>>>>>>>>>>>>>
>>>>>>>>>>>>> [000011e4][00101f7f][00000000] 83c408     add esp,+08
>>>>>>>>>>>>> [000011e7][00101f7b][00000000] 50         push eax
>>>>>>>>>>>>> [000011e8][00101f77][000004a3] 68a3040000 push 000004a3
>>>>>>>>>>>>> [000011ed][00101f77][000004a3] e800f3ffff call 000004f2
>>>>>>>>>>>>> Input_Halts = 0
>>>>>>>>>>>>> [000011f2][00101f7f][00000000] 83c408     add esp,+08
>>>>>>>>>>>>> [000011f5][00101f7f][00000000] 33c0       xor eax,eax
>>>>>>>>>>>>> [000011f7][00101f83][00000018] 5d         pop ebp
>>>>>>>>>>>>> [000011f8][00101f87][00000000] c3         ret
>>>>>>>>>>>>> Number of Instructions Executed(880) == 13 Pages
>>>>>>>>>>>> If H wasn't a simulation-based halting decider then Px()
>>>>>>>>>>>> would always halt; the infinite recursion is a
>>>>>>>>>>>> manifestation of your invalid simulation-based halting
>>>>>>>>>>>> decider.  There is no recursion in [Strachey 1965].
>>>>>>>>>>>>
>>>>>>>>>>>> /Flibble
>>>>>>>>>>>
>>>>>>>>>>> In other words you are rejecting the concept of a simulating
>>>>>>>>>>> halt decider even though I conclusively proved that it does
>>>>>>>>>>> correctly determine the halt status of: (see my new paper)
>>>>>>>>>>
>>>>>>>>>> No I am rejecting your simulating halt decider as it gets the
>>>>>>>>>> answer wrong for Px() which is not a pathological input. Px()
>>>>>>>>>> halts.
>>>>>>>>>>
>>>>>>>>>> /Flibble
>>>>>>>>>
>>>>>>>>> I just proved that H(Px,Px) does correctly predict that its
>>>>>>>>> complete and correct x86 emulation of its input would never
>>>>>>>>> reach the "ret" instruction of this input because of the
>>>>>>>>> pathological relationship between H and Px.
>>>>>>>> Wrong. Px() is not a pathological input as defined by the
>>>>>>>> halting problem and [Strachey 1965] as it does not try to do
>>>>>>>> the opposite of what H decides.
>>>>>>>>
>>>>>>>> /Flibble
>>>>>>>
>>>>>>> Your lack of comprehension does not actually count as any
>>>>>>> rebuttal at all.
>>>>>>>
>>>>>>> void P(u32 x)
>>>>>>>      {
>>>>>>>       if (H(x, x))
>>>>>>>         HERE: goto HERE;
>>>>>>>       return;
>>>>>>>      }
>>>>>>>
>>>>>>> int main()
>>>>>>>      {
>>>>>>>       Output("Input_Halts = ", H((u32)P, (u32)P));
>>>>>>>      }
>>>>>>>
>>>>>>> As shown below the above P and H have the required (halting
>>>>>>> problem) pathological relationship to each other:
>>>>>> [snip]
>>>>>>
>>>>>> P does but Px does not. I am talking about Px not P.
>>>>>>
>>>>>> void Px(u32 x)
>>>>>> {
>>>>>>       H(x, x);
>>>>>>       return;
>>>>>> }
>>>>>>
>>>>>> int main()
>>>>>> {
>>>>>>       Output("Input_Halts = ", H((u32)Px, (u32)Px));
>>>>>> }
>>>>>>
>>>>>> ...[000013e8][00102357][00000000] 83c408          add esp,+08
>>>>>> ...[000013eb][00102353][00000000] 50              push eax
>>>>>> ...[000013ec][0010234f][00000427] 6827040000      push 00000427
>>>>>> ---[000013f1][0010234f][00000427] e880f0ffff      call 00000476
>>>>>> Input_Halts = 0
>>>>>> ...[000013f6][00102357][00000000] 83c408          add esp,+08
>>>>>> ...[000013f9][00102357][00000000] 33c0            xor eax,eax
>>>>>> ...[000013fb][0010235b][00100000] 5d              pop ebp
>>>>>> ...[000013fc][0010235f][00000004] c3              ret
>>>>>> Number of Instructions Executed(16120)
>>>>>>
>>>>>> As can be seen above Olcott's H decides that Px does not halt but
>>>>>> it is obvious that Px should always halt if H is a valid halt
>>>>>> decider that always returns a decision to its caller (Px).
>>>>>> Olcott's H does not return a decision to its caller (Px) and is
>>>>>> thus invalid.
>>>>>>
>>>>>> /Flibble
>>>>>    >
>>>>>
>>>>> Your false assumptions are directly contradicted by the semantics
>>>>> of the x86 programming language.
>>>>>
>>>>> *x86 Instruction Set Reference*  https://c9x.me/x86/
>>>>>
>>>>> void Px(u32 x)
>>>>> {
>>>>>      H(x, x);
>>>>>      return;
>>>>> }
>>>>>
>>>>> int main()
>>>>> {
>>>>>      Output("Input_Halts = ", H((u32)Px, (u32)Px));
>>>>> }
>>>>>
>>>>> _Px()
>>>>> [00001192](01)  55         push ebp
>>>>> [00001193](02)  8bec       mov ebp,esp
>>>>> [00001195](03)  8b4508     mov eax,[ebp+08]
>>>>> [00001198](01)  50         push eax
>>>>> [00001199](03)  8b4d08     mov ecx,[ebp+08]
>>>>> [0000119c](01)  51         push ecx
>>>>> [0000119d](05)  e8d0fdffff call 00000f72
>>>>> [000011a2](03)  83c408     add esp,+08
>>>>> [000011a5](01)  5d         pop ebp
>>>>> [000011a6](01)  c3         ret
>>>>> Size in bytes:(0021) [000011a6]
>>>>>
>>>>> _main()
>>>>> [000011d2](01)  55         push ebp
>>>>> [000011d3](02)  8bec       mov ebp,esp
>>>>> [000011d5](05)  6892110000 push 00001192
>>>>> [000011da](05)  6892110000 push 00001192
>>>>> [000011df](05)  e88efdffff call 00000f72
>>>>> [000011e4](03)  83c408     add esp,+08
>>>>> [000011e7](01)  50         push eax
>>>>> [000011e8](05)  68a3040000 push 000004a3
>>>>> [000011ed](05)  e800f3ffff call 000004f2
>>>>> [000011f2](03)  83c408     add esp,+08
>>>>> [000011f5](02)  33c0       xor eax,eax
>>>>> [000011f7](01)  5d         pop ebp
>>>>> [000011f8](01)  c3         ret
>>>>> Size in bytes:(0039) [000011f8]
>>>>>
>>>>>     machine   stack     stack     machine    assembly
>>>>>     address   address   data      code       language
>>>>>     ========  ========  ========  =========  =============
>>>>> [000011d2][00101f7f][00000000] 55         push ebp
>>>>> [000011d3][00101f7f][00000000] 8bec       mov ebp,esp
>>>>> [000011d5][00101f7b][00001192] 6892110000 push 00001192
>>>>> [000011da][00101f77][00001192] 6892110000 push 00001192
>>>>> [000011df][00101f73][000011e4] e88efdffff call 00000f72
>>>>>
>>>>> H: Begin Simulation   Execution Trace Stored at:11202b
>>>>> Address_of_H:f72
>>>>> [00001192][00112017][0011201b] 55         push ebp
>>>>> [00001193][00112017][0011201b] 8bec       mov ebp,esp
>>>>> [00001195][00112017][0011201b] 8b4508     mov eax,[ebp+08]
>>>>> [00001198][00112013][00001192] 50         push eax      // push Px
>>>>> [00001199][00112013][00001192] 8b4d08     mov ecx,[ebp+08]
>>>>> [0000119c][0011200f][00001192] 51         push ecx      // push Px
>>>>> [0000119d][0011200b][000011a2] e8d0fdffff call 00000f72 // call
>>>>> H(Px,Px) H: Infinitely Recursive Simulation Detected Simulation
>>>>> Stopped
>>>>>
>>>>> H knows its own machine address and on this basis it can easily
>>>>> examine its stored execution_trace of Px (see above) to determine:
>>>>> (a) Px is calling H with the same arguments that H was called with.
>>>>> (b) No instructions in Px could possibly escape this otherwise
>>>>> infinitely recursive emulation.

On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>
> *This general principle refutes conventional halting problem proofs*
>
> Every simulating halt decider that correctly simulates its input until
> it correctly predicts that this simulated input would never reach its
> final state, correctly rejects this input as non-halting.
>
This "general principle is" a trivial definition: A simulation of a
called routine that stops when it can predict that the routine
will never return is called a halt decider.

In words of one syllable - so what?

On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>
>> *This general principle refutes conventional halting problem proofs*
>>
>> Every simulating halt decider that correctly simulates its input until
>> it correctly predicts that this simulated input would never reach its
>> final state, correctly rejects this input as non-halting.
>>
> This "general principle is" a trivial definition: A simulation of a
> called routine that stops when it can predict that the routine
> will never return is called a halt decider.
>
> In words of one syllable - so what?

*it refutes conventional halting problem proofs*

--
Copyright 2022 Pete Olcott

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

On 7/3/22 3:51 PM, olcott wrote:
> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>
>>> *This general principle refutes conventional halting problem proofs*
>>>
>>> Every simulating halt decider that correctly simulates its input until
>>> it correctly predicts that this simulated input would never reach its
>>> final state, correctly rejects this input as non-halting.
>>>
>> This "general principle is" a trivial definition: A simulation of a
>> called routine that stops when it can predict that the routine
>> will never return is called a halt decider.
>>
>> In words of one syllable - so what?
>
> *it refutes conventional halting problem proofs*
>
>

Only if you actually prove that you CAN correctly detect that the input
will never halt, and do so in finite time.

The problem, of course, is that H can't get arround the fact that if H
decides to return a 0 for H(P,P) then P(P) will Halt, so the answer is
wrong.

The ACTUAL behavior, is that an H that refuses to be wrong, just won't
answer, since ANY answer it gives will be wrong. This of course means if
fails to be a decider, so still ends up being wrong.

You seem to have the mistaken idea that it is allowed to presume the
impossible as done, but that technique leads to inconssistent logic systems.

On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
> > On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
> >>
> >> *This general principle refutes conventional halting problem proofs*
> >>
> >> Every simulating halt decider that correctly simulates its input until
> >> it correctly predicts that this simulated input would never reach its
> >> final state, correctly rejects this input as non-halting.
> >>
> > This "general principle is" a trivial definition: A simulation of a
> > called routine that stops when it can predict that the routine
> > will never return is called a halt decider.
> >
> > In words of one syllable - so what?
>
> It refutes conventional halting problem proofs
>
It might if any such halt deciders existed. You need to prove such "halt
deciders" exist.

On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>>
>>>> *This general principle refutes conventional halting problem proofs*
>>>>
>>>> Every simulating halt decider that correctly simulates its input until
>>>> it correctly predicts that this simulated input would never reach its
>>>> final state, correctly rejects this input as non-halting.
>>>>
>>> This "general principle is" a trivial definition: A simulation of a
>>> called routine that stops when it can predict that the routine
>>> will never return is called a halt decider.
>>>
>>> In words of one syllable - so what?
>>
>> It refutes conventional halting problem proofs
>>
> It might if any such halt deciders existed. You need to prove such "halt
> deciders" exist.

You can't keep ignoring my paper and claiming that I have not proved my
point.

*Halting problem proofs refuted on the basis of software engineering*

https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering

--
Copyright 2022 Pete Olcott

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

On 7/3/22 8:44 PM, olcott wrote:
> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>>>
>>>>> *This general principle refutes conventional halting problem proofs*
>>>>>
>>>>> Every simulating halt decider that correctly simulates its input until
>>>>> it correctly predicts that this simulated input would never reach its
>>>>> final state, correctly rejects this input as non-halting.
>>>>>
>>>> This "general principle is" a trivial definition: A simulation of a
>>>> called routine that stops when it can predict that the routine
>>>> will never return is called a halt decider.
>>>>
>>>> In words of one syllable - so what?
>>>
>>> It refutes conventional halting problem proofs
>>>
>> It might if any such halt deciders existed. You need to prove such "halt
>> deciders" exist.
>
>
> You can't keep ignoring my paper and claiming that I have not proved my
> point.
>
> *Halting problem proofs refuted on the basis of software engineering*
>
> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>
>
>
>

Rule (b) is incorrect.

FAIL.

On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
> > On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
> >> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
> >>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
> >>>>
> >>>> *This general principle refutes conventional halting problem proofs*
> >>>>
> >>>> Every simulating halt decider that correctly simulates its input until
> >>>> it correctly predicts that this simulated input would never reach its
> >>>> final state, correctly rejects this input as non-halting.
> >>>>
> >>> This "general principle is" a trivial definition: A simulation of a
> >>> called routine that stops when it can predict that the routine
> >>> will never return is called a halt decider.
> >>>
> >>> In words of one syllable - so what?
> >>
> >> It refutes conventional halting problem proofs
> >>
> > It might if any such halt deciders existed. You need to prove such "halt
> > deciders" exist.
>
> You can't keep ignoring my paper and claiming that I have not proved my
> point.
> *Halting problem proofs refuted on the basis of software engineering*
>
> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>
Your paper is not acceptable as a proof of anything. But that is to
be expected because my standard is mathematical proof and
you don't even pretend to be doing mathematics.

On 7/4/2022 11:36 AM, dklei...@gmail.com wrote:
> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>>>>
>>>>>> *This general principle refutes conventional halting problem proofs*
>>>>>>
>>>>>> Every simulating halt decider that correctly simulates its input until
>>>>>> it correctly predicts that this simulated input would never reach its
>>>>>> final state, correctly rejects this input as non-halting.
>>>>>>
>>>>> This "general principle is" a trivial definition: A simulation of a
>>>>> called routine that stops when it can predict that the routine
>>>>> will never return is called a halt decider.
>>>>>
>>>>> In words of one syllable - so what?
>>>>
>>>> It refutes conventional halting problem proofs
>>>>
>>> It might if any such halt deciders existed. You need to prove such "halt
>>> deciders" exist.
>>
>> You can't keep ignoring my paper and claiming that I have not proved my
>> point.
>> *Halting problem proofs refuted on the basis of software engineering*
>>
>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>>
> Your paper is not acceptable as a proof of anything. But that is to
> be expected because my standard is mathematical proof and
> you don't even pretend to be doing mathematics.

When we construe the x86 language and its associated semantics as a
formal language with formal semantics then this becomes a formal proof:

From a purely software engineering perspective (anchored in the
semantics of the x86 language) it is proven that H(P,P) correctly
predicts that its correct and complete x86 emulation of its input would
never reach the "ret" instruction (final state) of this input.

--
Copyright 2022 Pete Olcott

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

On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:
> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote:
> > On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
> >> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
> >>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
> >>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
> >>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
> >>>>>>
> >>>>>> *This general principle refutes conventional halting problem proofs*
> >>>>>>
> >>>>>> Every simulating halt decider that correctly simulates its input until
> >>>>>> it correctly predicts that this simulated input would never reach its
> >>>>>> final state, correctly rejects this input as non-halting.
> >>>>>>
> >>>>> This "general principle is" a trivial definition: A simulation of a
> >>>>> called routine that stops when it can predict that the routine
> >>>>> will never return is called a halt decider.
> >>>>>
> >>>>> In words of one syllable - so what?
> >>>>
> >>>> It refutes conventional halting problem proofs
> >>>>
> >>> It might if any such halt deciders existed. You need to prove such "halt
> >>> deciders" exist.
> >>
> >> You can't keep ignoring my paper and claiming that I have not proved my
> >> point.
> >> *Halting problem proofs refuted on the basis of software engineering*
> >> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
> >>
> > Your paper is not acceptable as a proof of anything. But that is to
> > be expected because my standard is mathematical proof and
> > you don't even pretend to be doing mathematics.
>
> When we construe the x86 language and its associated semantics as a
> formal language with formal semantics then this becomes a formal proof:
>
There is a great deal more to a mathematical proof than a formal
language. I believe that you do not have training in mathematics and you
do show little sympathy for the concerns of the mathematical
community. What you call "software engineering" is essentially hostile to
classical mathematics.

Moreover if you wish us to take you seriously you must do more than
"construing". You must exhibit the x86 "language" as a formal system
and show how it is used in a formal proof.

On 7/4/22 12:57 PM, olcott wrote:
> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote:
>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>>>>>
>>>>>>> *This general principle refutes conventional halting problem proofs*
>>>>>>>
>>>>>>> Every simulating halt decider that correctly simulates its input
>>>>>>> until
>>>>>>> it correctly predicts that this simulated input would never reach
>>>>>>> its
>>>>>>> final state, correctly rejects this input as non-halting.
>>>>>>>
>>>>>> This "general principle is" a trivial definition: A simulation of a
>>>>>> called routine that stops when it can predict that the routine
>>>>>> will never return is called a halt decider.
>>>>>>
>>>>>> In words of one syllable - so what?
>>>>>
>>>>> It refutes conventional halting problem proofs
>>>>>
>>>> It might if any such halt deciders existed. You need to prove such
>>>> "halt
>>>> deciders" exist.
>>>
>>> You can't keep ignoring my paper and claiming that I have not proved my
>>> point.
>>> *Halting problem proofs refuted on the basis of software engineering*
>>>
>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>>>
>>>
>> Your paper is not acceptable as a proof of anything. But that is to
>> be expected because my standard is mathematical proof and
>> you don't even pretend to be doing mathematics.
>
> When we construe the x86 language and its associated semantics as a
> formal language with formal semantics then this becomes a formal proof:
>
> From a purely software engineering perspective (anchored in the
> semantics of the x86 language) it is proven that H(P,P) correctly
> predicts that its correct and complete x86 emulation of its input would
> never reach the "ret" instruction (final state) of this input.
>

YOU LIE.

You arguement requries you to NOT look at the actual x86 behavior of
your H, and your proof is based on your misunderstanding of the principles.

You are just proving your ignorance of even basic software engineering.

On 7/4/2022 1:42 PM, dklei...@gmail.com wrote:
> On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:
>> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote:
>>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
>>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
>>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
>>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>>>>>>
>>>>>>>> *This general principle refutes conventional halting problem proofs*
>>>>>>>>
>>>>>>>> Every simulating halt decider that correctly simulates its input until
>>>>>>>> it correctly predicts that this simulated input would never reach its
>>>>>>>> final state, correctly rejects this input as non-halting.
>>>>>>>>
>>>>>>> This "general principle is" a trivial definition: A simulation of a
>>>>>>> called routine that stops when it can predict that the routine
>>>>>>> will never return is called a halt decider.
>>>>>>>
>>>>>>> In words of one syllable - so what?
>>>>>>
>>>>>> It refutes conventional halting problem proofs
>>>>>>
>>>>> It might if any such halt deciders existed. You need to prove such "halt
>>>>> deciders" exist.
>>>>
>>>> You can't keep ignoring my paper and claiming that I have not proved my
>>>> point.
>>>> *Halting problem proofs refuted on the basis of software engineering*
>>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>>>>
>>> Your paper is not acceptable as a proof of anything. But that is to
>>> be expected because my standard is mathematical proof and
>>> you don't even pretend to be doing mathematics.
>>
>> When we construe the x86 language and its associated semantics as a
>> formal language with formal semantics then this becomes a formal proof:
>>
> There is a great deal more to a mathematical proof than a formal
> language. I believe that you do not have training in mathematics and you
> do show little sympathy for the concerns of the mathematical
> community. What you call "software engineering" is essentially hostile to
> classical mathematics.
>
> Moreover if you wish us to take you seriously you must do more than
> "construing". You must exhibit the x86 "language" as a formal system
> and show how it is used in a formal proof.

What more is there to the essence of any formal proof besides applying
the formal semantics specified by a formal language as a sequence of
truth preserving steps?

Instead of premises a computation has an initial state.
Instead of a conclusion premises a computation has a final state.

*Curry–Howard correspondence*
In programming language theory and proof theory, the Curry–Howard
correspondence (also known as the Curry–Howard isomorphism or
equivalence, or the proofs-as-programs and propositions- or
formulae-as-types interpretation) is the direct relationship between
computer programs and mathematical proofs.

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

--
Copyright 2022 Pete Olcott

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

On 7/4/2022 2:17 PM, olcott wrote:
> On 7/4/2022 1:42 PM, dklei...@gmail.com wrote:
>> On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:
>>> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote:
>>>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
>>>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
>>>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
>>>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>>>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>>>>>>>
>>>>>>>>> *This general principle refutes conventional halting problem
>>>>>>>>> proofs*
>>>>>>>>>
>>>>>>>>> Every simulating halt decider that correctly simulates its
>>>>>>>>> input until
>>>>>>>>> it correctly predicts that this simulated input would never
>>>>>>>>> reach its
>>>>>>>>> final state, correctly rejects this input as non-halting.
>>>>>>>>>
>>>>>>>> This "general principle is" a trivial definition: A simulation of a
>>>>>>>> called routine that stops when it can predict that the routine
>>>>>>>> will never return is called a halt decider.
>>>>>>>>
>>>>>>>> In words of one syllable - so what?
>>>>>>>
>>>>>>> It refutes conventional halting problem proofs
>>>>>>>
>>>>>> It might if any such halt deciders existed. You need to prove such
>>>>>> "halt
>>>>>> deciders" exist.
>>>>>
>>>>> You can't keep ignoring my paper and claiming that I have not
>>>>> proved my
>>>>> point.
>>>>> *Halting problem proofs refuted on the basis of software engineering*
>>>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>>>>>
>>>>>
>>>> Your paper is not acceptable as a proof of anything. But that is to
>>>> be expected because my standard is mathematical proof and
>>>> you don't even pretend to be doing mathematics.
>>>
>>> When we construe the x86 language and its associated semantics as a
>>> formal language with formal semantics then this becomes a formal proof:
>>>
>> There is a great deal more to a mathematical proof than a formal
>> language. I believe that you do not have training in mathematics and you
>> do show little sympathy for the concerns of the mathematical
>> community. What you call "software engineering" is essentially hostile to
>> classical mathematics.
>>
>> Moreover if you wish us to take you seriously you must do more than
>> "construing". You must exhibit the x86 "language" as a formal system
>> and show how it is used in a formal proof.
>
> What more is there to the essence of any formal proof besides applying
> the formal semantics specified by a formal language as a sequence of
> truth preserving steps?
>
> Instead of premises a computation has an initial state.
> Instead of a conclusion premises a computation has a final state.

Instead of a conclusion a computation has a final state.

>
> *Curry–Howard correspondence*
> In programming language theory and proof theory, the Curry–Howard
> correspondence (also known as the Curry–Howard isomorphism or
> equivalence, or the proofs-as-programs and propositions- or
> formulae-as-types interpretation) is the direct relationship between
> computer programs and mathematical proofs.
>
> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
>

--
Copyright 2022 Pete Olcott

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

On 7/4/2022 1:42 PM, dklei...@gmail.com wrote:
> On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:
>> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote:
>>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
>>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
>>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
>>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>>>>>>
>>>>>>>> *This general principle refutes conventional halting problem proofs*
>>>>>>>>
>>>>>>>> Every simulating halt decider that correctly simulates its input until
>>>>>>>> it correctly predicts that this simulated input would never reach its
>>>>>>>> final state, correctly rejects this input as non-halting.
>>>>>>>>
>>>>>>> This "general principle is" a trivial definition: A simulation of a
>>>>>>> called routine that stops when it can predict that the routine
>>>>>>> will never return is called a halt decider.
>>>>>>>
>>>>>>> In words of one syllable - so what?
>>>>>>
>>>>>> It refutes conventional halting problem proofs
>>>>>>
>>>>> It might if any such halt deciders existed. You need to prove such "halt
>>>>> deciders" exist.
>>>>
>>>> You can't keep ignoring my paper and claiming that I have not proved my
>>>> point.
>>>> *Halting problem proofs refuted on the basis of software engineering*
>>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>>>>
>>> Your paper is not acceptable as a proof of anything. But that is to
>>> be expected because my standard is mathematical proof and
>>> you don't even pretend to be doing mathematics.
>>
>> When we construe the x86 language and its associated semantics as a
>> formal language with formal semantics then this becomes a formal proof:
>>
> There is a great deal more to a mathematical proof than a formal
> language. I believe that you do not have training in mathematics and you
> do show little sympathy for the concerns of the mathematical
> community. What you call "software engineering" is essentially hostile to
> classical mathematics.
>
> Moreover if you wish us to take you seriously you must do more than
> "construing". You must exhibit the x86 "language" as a formal system
> and show how it is used in a formal proof.

It would seem that *Curry–Howard correspondence*
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
would allow the x86 language and its semantics to be construed as a
formal system such that the initial state and final state of a
computable function along with all of the state transitions between
could be construed as a formal proof.

--
Copyright 2022 Pete Olcott

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

On 2022-07-04 00:44:23 +0000, olcott said:

> You can't keep ignoring my paper and claiming that I have not proved my point.

In order to make your proof publishable, you should decrate every sentence
in the proof with the numbers of that sentence or those two sentences from
which the sentence is derived with truth preserving rules.

Mikko

On 7/5/2022 3:53 AM, Mikko wrote:
> On 2022-07-04 00:44:23 +0000, olcott said:
>
>> You can't keep ignoring my paper and claiming that I have not proved
>> my point.
>
> In order to make your proof publishable, you should decrate every sentence
> in the proof with the numbers of that sentence or those two sentences from
> which the sentence is derived with truth preserving rules.
>
> Mikko
>
>

The proof is (Curry/Howard Correspondence) between programs and proofs,
thus H has an initial state performs a sequence of state transitions and
ends in a final state rejecting its input as non-halting.

*Halting problem proofs refuted on the basis of software engineering*
https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering

--

--
Copyright 2022 Pete Olcott

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

On 7/5/2022 7:59 AM, olcott wrote:
> On 7/5/2022 3:53 AM, Mikko wrote:
>> On 2022-07-04 00:44:23 +0000, olcott said:
>>
>>> You can't keep ignoring my paper and claiming that I have not proved
>>> my point.
>>
>> In order to make your proof publishable, you should decrate every
>> sentence
>> in the proof with the numbers of that sentence or those two sentences
>> from
>> which the sentence is derived with truth preserving rules.
>>
>> Mikko
>>
>>
>
> The proof is (Curry/Howard Correspondence) between programs and proofs,
> thus H has an initial state performs a sequence of state transitions and
> ends in a final state rejecting its input as non-halting.
>
> *Halting problem proofs refuted on the basis of software engineering*
> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>
>

From a purely software engineering perspective (anchored in the
semantics of the x86 language) it is proven that H(P,P) correctly
predicts that its correct and complete x86 emulation of its input would
never reach the "ret" instruction (final state) of this input.

--
Copyright 2022 Pete Olcott

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

On Monday, July 4, 2022 at 4:08:12 PM UTC-7, olcott wrote:
> On 7/4/2022 1:42 PM, dklei...@gmail.com wrote:
> > On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:
> >> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote:
> >>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
> >>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
> >>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
> >>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
> >>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
> >>>>>>>>
> >>>>>>>> *This general principle refutes conventional halting problem proofs*
> >>>>>>>>
> >>>>>>>> Every simulating halt decider that correctly simulates its input until
> >>>>>>>> it correctly predicts that this simulated input would never reach its
> >>>>>>>> final state, correctly rejects this input as non-halting.
> >>>>>>>>
> >>>>>>> This "general principle is" a trivial definition: A simulation of a
> >>>>>>> called routine that stops when it can predict that the routine
> >>>>>>> will never return is called a halt decider.
> >>>>>>>
> >>>>>>> In words of one syllable - so what?
> >>>>>>
> >>>>>> It refutes conventional halting problem proofs
> >>>>>>
> >>>>> It might if any such halt deciders existed. You need to prove such "halt
> >>>>> deciders" exist.
> >>>>
> >>>> You can't keep ignoring my paper and claiming that I have not proved my
> >>>> point.
> >>>> *Halting problem proofs refuted on the basis of software engineering*
> >>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
> >>>>
> >>> Your paper is not acceptable as a proof of anything. But that is to
> >>> be expected because my standard is mathematical proof and
> >>> you don't even pretend to be doing mathematics.
> >>
> >> When we construe the x86 language and its associated semantics as a
> >> formal language with formal semantics then this becomes a formal proof:
> >>
> > There is a great deal more to a mathematical proof than a formal
> > language. I believe that you do not have training in mathematics and you
> > do show little sympathy for the concerns of the mathematical
> > community. What you call "software engineering" is essentially hostile to
> > classical mathematics.
> >
> > Moreover if you wish us to take you seriously you must do more than
> > "construing". You must exhibit the x86 "language" as a formal system
> > and show how it is used in a formal proof.
> It would seem that *Curry–Howard correspondence*
> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
> would allow the x86 language and its semantics to be construed as a
> formal system such that the initial state and final state of a
> computable function along with all of the state transitions between
> could be construed as a formal proof.

I am afraid you don't see mathematical proof like a mathematician
might. A good and simple example is the theorem that proves all
Burnside three groups are finite.

But if you do want to use the Curry-Howard correspondence as a
proof method you must either reference the formal x86 language
formulation or yourself supply such a formal language description.

Your task would be much easier were you to use C as the formal
language. And much easier to follow.

On 7/5/2022 1:50 PM, dklei...@gmail.com wrote:
> On Monday, July 4, 2022 at 4:08:12 PM UTC-7, olcott wrote:
>> On 7/4/2022 1:42 PM, dklei...@gmail.com wrote:
>>> On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:
>>>> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote:
>>>>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
>>>>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
>>>>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
>>>>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>>>>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>>>>>>>>
>>>>>>>>>> *This general principle refutes conventional halting problem proofs*
>>>>>>>>>>
>>>>>>>>>> Every simulating halt decider that correctly simulates its input until
>>>>>>>>>> it correctly predicts that this simulated input would never reach its
>>>>>>>>>> final state, correctly rejects this input as non-halting.
>>>>>>>>>>
>>>>>>>>> This "general principle is" a trivial definition: A simulation of a
>>>>>>>>> called routine that stops when it can predict that the routine
>>>>>>>>> will never return is called a halt decider.
>>>>>>>>>
>>>>>>>>> In words of one syllable - so what?
>>>>>>>>
>>>>>>>> It refutes conventional halting problem proofs
>>>>>>>>
>>>>>>> It might if any such halt deciders existed. You need to prove such "halt
>>>>>>> deciders" exist.
>>>>>>
>>>>>> You can't keep ignoring my paper and claiming that I have not proved my
>>>>>> point.
>>>>>> *Halting problem proofs refuted on the basis of software engineering*
>>>>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>>>>>>
>>>>> Your paper is not acceptable as a proof of anything. But that is to
>>>>> be expected because my standard is mathematical proof and
>>>>> you don't even pretend to be doing mathematics.
>>>>
>>>> When we construe the x86 language and its associated semantics as a
>>>> formal language with formal semantics then this becomes a formal proof:
>>>>
>>> There is a great deal more to a mathematical proof than a formal
>>> language. I believe that you do not have training in mathematics and you
>>> do show little sympathy for the concerns of the mathematical
>>> community. What you call "software engineering" is essentially hostile to
>>> classical mathematics.
>>>
>>> Moreover if you wish us to take you seriously you must do more than
>>> "construing". You must exhibit the x86 "language" as a formal system
>>> and show how it is used in a formal proof.
>> It would seem that *Curry–Howard correspondence*
>> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
>> would allow the x86 language and its semantics to be construed as a
>> formal system such that the initial state and final state of a
>> computable function along with all of the state transitions between
>> could be construed as a formal proof.
>
> I am afraid you don't see mathematical proof like a mathematician
> might. A good and simple example is the theorem that proves all
> Burnside three groups are finite.
>
> But if you do want to use the Curry-Howard correspondence as a
> proof method you must either reference the formal x86 language
> formulation or yourself supply such a formal language description.
>

I already provided this:
x86 Instruction Set Reference
https://c9x.me/x86/

> Your task would be much easier were you to use C as the formal
> language. And much easier to follow.

If we use C as the formal language then we have to translate it into its
corresponding directed graph of control flow ourselves or the computer
will not be able to process it.

I use C/x86 together so the human can examine the C and the machine can
examine the machine code and the human can see the bijection between the
C and the machine code as assembly language generated from the C.

void P(u32 x)
{ if (H(x, x))
HERE: goto HERE;
return;
}

_P()
[00001202](01) 55 push ebp
[00001203](02) 8bec mov ebp,esp
[00001205](03) 8b4508 mov eax,[ebp+08]
[00001208](01) 50 push eax
[00001209](03) 8b4d08 mov ecx,[ebp+08]
[0000120c](01) 51 push ecx
[0000120d](05) e820feffff call 00001032
[00001212](03) 83c408 add esp,+08
[00001215](02) 85c0 test eax,eax
[00001217](02) 7402 jz 0000121b
[00001219](02) ebfe jmp 00001219
[0000121b](01) 5d pop ebp
[0000121c](01) c3 ret
Size in bytes:(0027) [0000121c]

--
Copyright 2022 Pete Olcott

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

On 2022-07-05 12:50, dklei...@gmail.com wrote:
> On Monday, July 4, 2022 at 4:08:12 PM UTC-7, olcott wrote:
>> On 7/4/2022 1:42 PM, dklei...@gmail.com wrote:
>>> On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:
>>>> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote:
>>>>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
>>>>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
>>>>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
>>>>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>>>>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>>>>>>>>
>>>>>>>>>> *This general principle refutes conventional halting problem proofs*
>>>>>>>>>>
>>>>>>>>>> Every simulating halt decider that correctly simulates its input until
>>>>>>>>>> it correctly predicts that this simulated input would never reach its
>>>>>>>>>> final state, correctly rejects this input as non-halting.
>>>>>>>>>>
>>>>>>>>> This "general principle is" a trivial definition: A simulation of a
>>>>>>>>> called routine that stops when it can predict that the routine
>>>>>>>>> will never return is called a halt decider.
>>>>>>>>>
>>>>>>>>> In words of one syllable - so what?
>>>>>>>>
>>>>>>>> It refutes conventional halting problem proofs
>>>>>>>>
>>>>>>> It might if any such halt deciders existed. You need to prove such "halt
>>>>>>> deciders" exist.
>>>>>>
>>>>>> You can't keep ignoring my paper and claiming that I have not proved my
>>>>>> point.
>>>>>> *Halting problem proofs refuted on the basis of software engineering*
>>>>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>>>>>>
>>>>> Your paper is not acceptable as a proof of anything. But that is to
>>>>> be expected because my standard is mathematical proof and
>>>>> you don't even pretend to be doing mathematics.
>>>>
>>>> When we construe the x86 language and its associated semantics as a
>>>> formal language with formal semantics then this becomes a formal proof:
>>>>
>>> There is a great deal more to a mathematical proof than a formal
>>> language. I believe that you do not have training in mathematics and you
>>> do show little sympathy for the concerns of the mathematical
>>> community. What you call "software engineering" is essentially hostile to
>>> classical mathematics.
>>>
>>> Moreover if you wish us to take you seriously you must do more than
>>> "construing". You must exhibit the x86 "language" as a formal system
>>> and show how it is used in a formal proof.
>> It would seem that *Curry–Howard correspondence*
>> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
>> would allow the x86 language and its semantics to be construed as a
>> formal system such that the initial state and final state of a
>> computable function along with all of the state transitions between
>> could be construed as a formal proof.
>
> I am afraid you don't see mathematical proof like a mathematician
> might. A good and simple example is the theorem that proves all
> Burnside three groups are finite.
>
> But if you do want to use the Curry-Howard correspondence as a
> proof method you must either reference the formal x86 language
> formulation or yourself supply such a formal language description.
>
> Your task would be much easier were you to use C as the formal
> language. And much easier to follow.

If he really wants to use (and if he actually understood) Curry-Howard,
he'd be better off using Scheme or Haskell or something like that...

But it wouldn't make a difference. He has not provided an actual proof
NOR an actual program, so talking about some alleged correspondence
between two imaginary entities is hardly going to enlighten anyone.

André

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

On 7/5/2022 3:24 PM, André G. Isaak wrote:
> On 2022-07-05 12:50, dklei...@gmail.com wrote:
>> On Monday, July 4, 2022 at 4:08:12 PM UTC-7, olcott wrote:
>>> On 7/4/2022 1:42 PM, dklei...@gmail.com wrote:
>>>> On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:
>>>>> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote:
>>>>>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
>>>>>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
>>>>>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
>>>>>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>>>>>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>>>>>>>>>
>>>>>>>>>>> *This general principle refutes conventional halting problem
>>>>>>>>>>> proofs*
>>>>>>>>>>>
>>>>>>>>>>> Every simulating halt decider that correctly simulates its
>>>>>>>>>>> input until
>>>>>>>>>>> it correctly predicts that this simulated input would never
>>>>>>>>>>> reach its
>>>>>>>>>>> final state, correctly rejects this input as non-halting.
>>>>>>>>>>>
>>>>>>>>>> This "general principle is" a trivial definition: A simulation
>>>>>>>>>> of a
>>>>>>>>>> called routine that stops when it can predict that the routine
>>>>>>>>>> will never return is called a halt decider.
>>>>>>>>>>
>>>>>>>>>> In words of one syllable - so what?
>>>>>>>>>
>>>>>>>>> It refutes conventional halting problem proofs
>>>>>>>>>
>>>>>>>> It might if any such halt deciders existed. You need to prove
>>>>>>>> such "halt
>>>>>>>> deciders" exist.
>>>>>>>
>>>>>>> You can't keep ignoring my paper and claiming that I have not
>>>>>>> proved my
>>>>>>> point.
>>>>>>> *Halting problem proofs refuted on the basis of software
>>>>>>> engineering*
>>>>>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>>>>>>>
>>>>>>>
>>>>>> Your paper is not acceptable as a proof of anything. But that is to
>>>>>> be expected because my standard is mathematical proof and
>>>>>> you don't even pretend to be doing mathematics.
>>>>>
>>>>> When we construe the x86 language and its associated semantics as a
>>>>> formal language with formal semantics then this becomes a formal
>>>>> proof:
>>>>>
>>>> There is a great deal more to a mathematical proof than a formal
>>>> language. I believe that you do not have training in mathematics and
>>>> you
>>>> do show little sympathy for the concerns of the mathematical
>>>> community. What you call "software engineering" is essentially
>>>> hostile to
>>>> classical mathematics.
>>>>
>>>> Moreover if you wish us to take you seriously you must do more than
>>>> "construing". You must exhibit the x86 "language" as a formal system
>>>> and show how it is used in a formal proof.
>>> It would seem that *Curry–Howard correspondence*
>>> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
>>> would allow the x86 language and its semantics to be construed as a
>>> formal system such that the initial state and final state of a
>>> computable function along with all of the state transitions between
>>> could be construed as a formal proof.
>>
>> I am afraid you don't see mathematical proof like a mathematician
>> might. A good and simple example is the theorem that proves all
>> Burnside three groups are finite.
>>
>> But if you do want to use the Curry-Howard correspondence as a
>> proof method you must either reference the formal x86 language
>> formulation or yourself supply such a formal language description.
>>
>> Your task would be much easier were you to use C as the formal
>> language. And much easier to follow.
>
> If he really wants to use (and if he actually understood) Curry-Howard,
> he'd be better off using Scheme or Haskell or something like that...
>
> But it wouldn't make a difference. He has not provided an actual proof
> NOR an actual program, so talking about some alleged correspondence
> between two imaginary entities is hardly going to enlighten anyone.
>
> André
>

Welcome back you are one of my competent reviewers.

*My most recent paper provides complete proof of this*

From a purely software engineering perspective (anchored in the
semantics of the x86 language) it is proven that H(P,P) correctly
predicts that its correct and complete x86 emulation of its input would
never reach the "ret" instruction (final state) of this input.

*Halting problem proofs refuted on the basis of software engineering*
https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering

*Only to those having the required software engineering prerequisites*

The start state, state transitions inbetween and the final state of a
computation can be construed as a formal proof from premises to conclusion.

--
Copyright 2022 Pete Olcott

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

On Tuesday, July 5, 2022 at 12:31:47 PM UTC-7, olcott wrote:
> On 7/5/2022 1:50 PM, dklei...@gmail.com wrote:
> >
> > But if you do want to use the Curry-Howard correspondence as a
> > proof method you must either reference the formal x86 language
> > formulation or yourself supply such a formal language description.
> >
> I already provided this:
> x86 Instruction Set Reference
> https://c9x.me/x86/
..>
We have been here before. A list of op-codes is not a formal language
description.
>
> > Your task would be much easier were you to use C as the formal
> > language. And much easier to follow.
>
>> If we use C as the formal language then we have to translate it into its
> corresponding directed graph of control flow ourselves or the computer
> will not be able to process it.
>
You don't need to compile. The readers whom you want to convince can
read and follow C. That's the level mathematics is done at.
>
> I use C/x86 together so the human can examine the C and the machine can
> examine the machine code and the human can see the bijection between the
> C and the machine code as assembly language generated from the C.
..>
Nobody cares about that "bijection" and messing with it wastes everybody's
time.

On 7/5/22 4:42 PM, olcott wrote:
> On 7/5/2022 3:24 PM, André G. Isaak wrote:
>> On 2022-07-05 12:50, dklei...@gmail.com wrote:
>>> On Monday, July 4, 2022 at 4:08:12 PM UTC-7, olcott wrote:
>>>> On 7/4/2022 1:42 PM, dklei...@gmail.com wrote:
>>>>> On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:
>>>>>> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote:
>>>>>>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
>>>>>>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
>>>>>>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
>>>>>>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>>>>>>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>>>>>>>>>>
>>>>>>>>>>>> *This general principle refutes conventional halting problem
>>>>>>>>>>>> proofs*
>>>>>>>>>>>>
>>>>>>>>>>>> Every simulating halt decider that correctly simulates its
>>>>>>>>>>>> input until
>>>>>>>>>>>> it correctly predicts that this simulated input would never
>>>>>>>>>>>> reach its
>>>>>>>>>>>> final state, correctly rejects this input as non-halting.
>>>>>>>>>>>>
>>>>>>>>>>> This "general principle is" a trivial definition: A
>>>>>>>>>>> simulation of a
>>>>>>>>>>> called routine that stops when it can predict that the routine
>>>>>>>>>>> will never return is called a halt decider.
>>>>>>>>>>>
>>>>>>>>>>> In words of one syllable - so what?
>>>>>>>>>>
>>>>>>>>>> It refutes conventional halting problem proofs
>>>>>>>>>>
>>>>>>>>> It might if any such halt deciders existed. You need to prove
>>>>>>>>> such "halt
>>>>>>>>> deciders" exist.
>>>>>>>>
>>>>>>>> You can't keep ignoring my paper and claiming that I have not
>>>>>>>> proved my
>>>>>>>> point.
>>>>>>>> *Halting problem proofs refuted on the basis of software
>>>>>>>> engineering*
>>>>>>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>>>>>>>>
>>>>>>>>
>>>>>>> Your paper is not acceptable as a proof of anything. But that is to
>>>>>>> be expected because my standard is mathematical proof and
>>>>>>> you don't even pretend to be doing mathematics.
>>>>>>
>>>>>> When we construe the x86 language and its associated semantics as a
>>>>>> formal language with formal semantics then this becomes a formal
>>>>>> proof:
>>>>>>
>>>>> There is a great deal more to a mathematical proof than a formal
>>>>> language. I believe that you do not have training in mathematics
>>>>> and you
>>>>> do show little sympathy for the concerns of the mathematical
>>>>> community. What you call "software engineering" is essentially
>>>>> hostile to
>>>>> classical mathematics.
>>>>>
>>>>> Moreover if you wish us to take you seriously you must do more than
>>>>> "construing". You must exhibit the x86 "language" as a formal system
>>>>> and show how it is used in a formal proof.
>>>> It would seem that *Curry–Howard correspondence*
>>>> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
>>>> would allow the x86 language and its semantics to be construed as a
>>>> formal system such that the initial state and final state of a
>>>> computable function along with all of the state transitions between
>>>> could be construed as a formal proof.
>>>
>>> I am afraid you don't see mathematical proof like a mathematician
>>> might. A good and simple example is the theorem that proves all
>>> Burnside three groups are finite.
>>>
>>> But if you do want to use the Curry-Howard correspondence as a
>>> proof method you must either reference the formal x86 language
>>> formulation or yourself supply such a formal language description.
>>>
>>> Your task would be much easier were you to use C as the formal
>>> language. And much easier to follow.
>>
>> If he really wants to use (and if he actually understood)
>> Curry-Howard, he'd be better off using Scheme or Haskell or something
>> like that...
>>
>> But it wouldn't make a difference. He has not provided an actual proof
>> NOR an actual program, so talking about some alleged correspondence
>> between two imaginary entities is hardly going to enlighten anyone.
>>
>> André
>>
>
> Welcome back you are one of my competent reviewers.
>
> *My most recent paper provides complete proof of this*
>
> From a purely software engineering perspective (anchored in the
> semantics of the x86 language) it is proven that H(P,P) correctly
> predicts that its correct and complete x86 emulation of its input would
> never reach the "ret" instruction (final state) of this input.
>
> *Halting problem proofs refuted on the basis of software engineering*
> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>
>
> *Only to those having the required software engineering prerequisites*
>
> The start state, state transitions inbetween and the final state of a
> computation can be construed as a formal proof from premises to conclusion.
>
>

Except that H doesn't actually look at the input as an actual program,
but replaces the call to H with parameters P,P with something that acts
differently then the actual call to H(P,P) from "main", so fails to meet
the requirements of Curly-Howard.

Note, your rule (b) is incorrect as you use it, which is a core fault
with your "proof".