Halting problem proofs refuted on the basis of software engineering V2

30 views
Skip to first unread message

olcott

unread,
Jul 4, 2022, 10:46:05 AMJul 4
to
No one can provide any "rebuttal" of my paper on any other basis
than

(1) disagreeing with the semantics of the x86 language
*x86 Instruction Set Reference* https://c9x.me/x86/

*or disagreeing with this necessarily true principle*
(2) A halt decider must compute the mapping from its inputs to an accept
or reject state on the basis of the actual behavior that is actually
specified by these inputs.



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(P,P) correctly determines that its input never halts

typedef void (*ptr)();

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

int main()
{
Output("Input_Halts = ", H(P, 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


*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

Paul N

unread,
Jul 5, 2022, 9:47:35 AMJul 5
to
On Monday, July 4, 2022 at 3:46:05 PM UTC+1, olcott wrote:
> No one can provide any "rebuttal" of my paper on any other basis
> than

You're the one disagreeing with these!

> (1) disagreeing with the semantics of the x86 language
> *x86 Instruction Set Reference* https://c9x.me/x86/

You've said numerous times that a "correct emulation" of P(P) does not halt, whereas P(P) actually halts. You're clearly failing to emulate correctly.

> *or disagreeing with this necessarily true principle*
> (2) A halt decider must compute the mapping from its inputs to an accept
> or reject state on the basis of the actual behavior that is actually
> specified by these inputs.

Likewise, you've said numerous times that your halt decider decides P(P) does not halt, whereas P(P) actually halts.

Paul N

unread,
Jul 5, 2022, 9:49:26 AMJul 5
to
Apologies all (especially Keith), I forgot I was not in comp.theory!

olcott

unread,
Jul 5, 2022, 10:13:54 AMJul 5
to
The correctly emulated input to H(P,P) is an entirely different sequence
of configurations than the directly executed P(P). This is conclusively
proved by the provably correct execution trace of each.

olcott

unread,
Jul 5, 2022, 10:23:16 AMJul 5
to
On 7/5/2022 8:47 AM, Paul N wrote:
The correctly emulated input to H(P,P) is an entirely different sequence
of configurations than the directly executed P(P). This is conclusively
proved by the provably correct execution trace of each.

Example 04: P(P) halts because H(P,P) correctly determines that its
input never halts

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

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

_P()
[000011f0](01) 55 push ebp
[000011f1](02) 8bec mov ebp,esp
[000011f3](03) 8b4508 mov eax,[ebp+08]
[000011f6](01) 50 push eax
[000011f7](03) 8b4d08 mov ecx,[ebp+08]
[000011fa](01) 51 push ecx
[000011fb](05) e820feffff call 00001020
[00001200](03) 83c408 add esp,+08
[00001203](02) 85c0 test eax,eax
[00001205](02) 7402 jz 00001209
[00001207](02) ebfe jmp 00001207
[00001209](01) 5d pop ebp
[0000120a](01) c3 ret
Size in bytes:(0027) [0000120a]

_main()
[00001210](01) 55 push ebp
[00001211](02) 8bec mov ebp,esp
[00001213](05) 68f0110000 push 000011f0
[00001218](05) e8d3ffffff call 000011f0
[0000121d](03) 83c404 add esp,+04
[00001220](02) 33c0 xor eax,eax
[00001222](01) 5d pop ebp
[00001223](01) c3 ret
Size in bytes:(0020) [00001223]

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
[00001210][00101fba][00000000] 55 push ebp
[00001211][00101fba][00000000] 8bec mov ebp,esp
[00001213][00101fb6][000011f0] 68f0110000 push 000011f0 // push P
[00001218][00101fb2][0000121d] e8d3ffffff call 000011f0 // call P
[000011f0][00101fae][00101fba] 55 push ebp // enter executed P
[000011f1][00101fae][00101fba] 8bec mov ebp,esp
[000011f3][00101fae][00101fba] 8b4508 mov eax,[ebp+08]
[000011f6][00101faa][000011f0] 50 push eax // push P
[000011f7][00101faa][000011f0] 8b4d08 mov ecx,[ebp+08]
[000011fa][00101fa6][000011f0] 51 push ecx // push P
[000011fb][00101fa2][00001200] e820feffff call 00001020 // call H

Begin Simulation Execution Trace Stored at:21206e
Address_of_H:1020
[000011f0][0021205a][0021205e] 55 push ebp // enter emulated P
[000011f1][0021205a][0021205e] 8bec mov ebp,esp
[000011f3][0021205a][0021205e] 8b4508 mov eax,[ebp+08]
[000011f6][00212056][000011f0] 50 push eax // push P
[000011f7][00212056][000011f0] 8b4d08 mov ecx,[ebp+08]
[000011fa][00212052][000011f0] 51 push ecx // push P
[000011fb][0021204e][00001200] e820feffff call 00001020 // call emulated 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 P (see above) to determine:
(a) P is calling H with the same arguments that H was called with.
(b) No instructions in P could possibly escape this otherwise infinitely
recursive emulation.
(c) H aborts its emulation of P before its call to H is emulated.

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.

[00001200][00101fae][00101fba] 83c408 add esp,+08 // return to
executed P
[00001203][00101fae][00101fba] 85c0 test eax,eax
[00001205][00101fae][00101fba] 7402 jz 00001209
[00001209][00101fb2][0000121d] 5d pop ebp
[0000120a][00101fb6][000011f0] c3 ret // return from
executed P
[0000121d][00101fba][00000000] 83c404 add esp,+04
[00001220][00101fba][00000000] 33c0 xor eax,eax
[00001222][00101fbe][00100000] 5d pop ebp
[00001223][00101fc2][00000000] c3 ret // ret from main
Number of Instructions Executed(878) / 67 = 13 pages

olcott

unread,
Jul 5, 2022, 10:36:56 AMJul 5
to
The post that you replied to already had followup to comp.theory
you must have changed this to comp.lang.c

Richard Damon

unread,
Jul 5, 2022, 10:31:26 PMJul 5
to

On 7/5/22 10:13 AM, olcott wrote:
> On 7/5/2022 8:47 AM, Paul N wrote:
>> On Monday, July 4, 2022 at 3:46:05 PM UTC+1, olcott wrote:
>>> No one can provide any "rebuttal" of my paper on any other basis
>>> than
>>
>> You're the one disagreeing with these!
>>
>>> (1) disagreeing with the semantics of the x86 language
>>> *x86 Instruction Set Reference* https://c9x.me/x86/
>>
>> You've said numerous times that a "correct emulation" of P(P) does not
>> halt, whereas P(P) actually halts. You're clearly failing to emulate
>> correctly.
>>
>>> *or disagreeing with this necessarily true principle*
>>> (2) A halt decider must compute the mapping from its inputs to an accept
>>> or reject state on the basis of the actual behavior that is actually
>>> specified by these inputs.
>>
>> Likewise, you've said numerous times that your halt decider decides
>> P(P) does not halt, whereas P(P) actually halts.
>
> The correctly emulated input to H(P,P) is an entirely different sequence
> of configurations than the directly executed P(P). This is conclusively
> proved by the provably correct execution trace of each.
>

Then P isn't the correct P, as P is defined to call H to decide on P(P),
so if H(P,P) isn't representing P(P), then P is wrong, and you need to
tell us what P needs to do to even ask about P(P) or H fails to be able
to be asked the needed qudstion and thus can't give the correct answer
to be the claimed counter example.
Reply all
Reply to author
Forward
0 new messages