Forums before death by AOL, social media and spammers... "We can't have nice things"
| comp.lang.asm.x86 | Ahh, the lost art of x86 assembly | 4,675 messages |
[ << oldest | < older | list | newer > | newest >> ]
| Message 4,222 of 4,675 |
| olcott to wolfgang kern |
| Re: Refuting the {Linz, Sipser and Kozen |
| 16 Dec 20 19:40:50 |
From: NoOne@nospicedham.NoWhere.com
On 12/15/2020 3:05 AM, wolfgang kern wrote:
> removed theory etc.
>
> On 14.12.2020 22:56, olcott wrote and cyted:
>
> A LOT of useless HLL lines.
> please don't bother us here with this, it's an assembler group.
> __
> wolfgang
>
That last message was sent by mistake.
This is the only one that might be relevant to this group:
I refuted the halting problem proofs by building a universal Turing
machine that has the x86 language as its machine description language.
The key aspect of this proof is the x86 execution trace at the bottom of
this message.
If you have a good understanding of:
(a) software engineering,
(b) The C programming language
(c) The x86 programming language
You will be able to easily verify that Halts() does correctly decide the
halt status of H_Hat().
The x86utm operating system provides the operating environment to
execute virtual machines computationally equivalent to universal Turing
machines having the x86 language as their machine description language.
x86utm executes the COFF object file output of the Microsoft C compiler.
The x86utm operating system is based on a world class x86 emulator that
has been developed and tested for decades.
x86 language ≡ von Neumann architecture ≡ UTM ≡ RASP Machine
It is common knowledge that all x86 based programs are computationally
equivalent to UTMs for every computation that does not require more
memory than they have.
This is the generic halt deciding criteria:
On Saturday, November 28, 2020 at 2:00:28 PM UTC-8, olcott wrote:
> Every computation that would not halt if its simulation
> were not halted is by logical necessity a non-halting computation.
We can verify that the following execution trace of the computational
equivalent of:
(a) {Peter Linz: H, Michael Sipser: H, Dexter Kozen: K}
Correctly decides halting on the the computational equivalent of:
(b) {Peter Linz: Ĥ, Michael Sipser: D, Dexter Kozen: N}
The following execution trace can be verified as correctly deciding the
halting status of its input with only these three prerequisites and
nothing more:
(a) An elementary understanding of software engineering, such things as:
(a) infinite loops do not have a fixed number of iterations and (b)
infinitely recursive invocations never return any value to their caller.
(b) A basic understanding of how the C programming language maps to x86
instructions. This is used to verify that the translations of the "C"
functions into their x86 equivalents are correct. It is also used to
verifiy that the execution trace of these x86 functions is correct.
(c) An understanding of one very elementary infinite recursion detection
algorithm: Whenever an execution trace shows a second call to the same
function from the same machine address with no control flow instructions
in-between this second invocation is always an instance of infinite
recursion. From this it is very easy to see that the halt decider did
apply this simple criteria in its halt deciding decision, thus meeting
he generic criteria shown above.
Actual debug trace of Halts() deciding halting on H_Hat()
#define HALT __asm hlt
void H_Hat(u32 P)
{
u32 Input_Halts = Halts(P, P);
if (Input_Halts)
HERE: goto HERE;
else
HALT
}
int main()
{
u32 Input_Would_Halt = Halts((u32)H_Hat, (u32)H_Hat);
Output_Debug_Trace();
Output("Input_Would_Halt =", Input_Would_Halt);
HALT;
}
_H_Hat()
[000005e6](01) 55 push ebp
[000005e7](02) 8bec mov ebp,esp
[000005e9](01) 51 push ecx
[000005ea](03) 8b4508 mov eax,[ebp+08]
[000005ed](01) 50 push eax
[000005ee](03) 8b4d08 mov ecx,[ebp+08]
[000005f1](01) 51 push ecx
[000005f2](05) e8effdffff call 000003e6
[000005f7](03) 83c408 add esp,+08
[000005fa](03) 8945fc mov [ebp-04],eax
[000005fd](04) 837dfc00 cmp dword [ebp-04],+00
[00000601](02) 7404 jz 00000607
[00000603](02) ebfe jmp 00000603
[00000605](02) eb01 jmp 00000608
[00000607](01) f4 hlt
[00000608](02) 8be5 mov esp,ebp
[0000060a](01) 5d pop ebp
[0000060b](01) c3 ret
_main()
[00000616](01) 55 push ebp
[00000617](02) 8bec mov ebp,esp
[00000619](01) 51 push ecx
[0000061a](05) 68e6050000 push 000005e6
[0000061f](05) 68e6050000 push 000005e6
[00000624](05) e8bdfdffff call 000003e6
[00000629](03) 83c408 add esp,+08
[0000062c](03) 8945fc mov [ebp-04],eax
[0000062f](05) e8f2fcffff call 00000326
[00000634](03) 8b45fc mov eax,[ebp-04]
[00000637](01) 50 push eax
[00000638](05) 68a3020000 push 000002a3
[0000063d](05) e894fcffff call 000002d6
[00000642](03) 83c408 add esp,+08
[00000645](01) f4 hlt
[00000646](02) 8be5 mov esp,ebp
[00000648](01) 5d pop ebp
[00000649](01) c3 ret
Output_Debug_Trace() Trace_List.size(24)
---[00000616](01) 55 push ebp
---[00000617](02) 8bec mov ebp,esp
---[00000619](01) 51 push ecx
---[0000061a](05) 68e6050000 push 000005e6
---[0000061f](05) 68e6050000 push 000005e6
---[00000624](05) e8bdfdffff call 000003e6 --CALL [000003e6]
---[000005e6](01) 55 push ebp
---[000005e7](02) 8bec mov ebp,esp
---[000005e9](01) 51 push ecx
---[000005ea](03) 8b4508 mov eax,[ebp+08]
---[000005ed](01) 50 push eax
---[000005ee](03) 8b4d08 mov ecx,[ebp+08]
---[000005f1](01) 51 push ecx
---[000005f2](05) e8effdffff call 000003e6 --CALL [000003e6]
---[000005e6](01) 55 push ebp
---[000005e7](02) 8bec mov ebp,esp
---[000005e9](01) 51 push ecx
---[000005ea](03) 8b4508 mov eax,[ebp+08]
---[000005ed](01) 50 push eax
---[000005ee](03) 8b4d08 mov ecx,[ebp+08]
---[000005f1](01) 51 push ecx
---[000005f2](05) e8effdffff call 000003e6 --CALL [000003e6]
Input Aborted because of INFINITE RECURSION from [000005f2] to [000003e6]
[continued in next message]
--- SoupGate-Win32 v1.05
* Origin: you cannot sedate... all the things you hate (1:229/2)
|
(c) 1994, bbs@darkrealms.ca