Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

Yes I have a Machintosh, please don't scream at me. -- Larry Blumette on linux-kernel


programming / comp.lang.asm.x86 / Re: Refuting the {Linz, Sipser and Kozen} HP Proofs (deciders within

Subject: Re: Refuting the {Linz, Sipser and Kozen} HP Proofs (deciders within
From: olcott
Newsgroups: comp.lang.asm.x86
Organization: A noiseless patient Spider
Date: Thu, 17 Dec 2020 01:40 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: NoO...@nospicedham.NoWhere.com (olcott)
Newsgroups: comp.lang.asm.x86
Subject: Re: Refuting the {Linz, Sipser and Kozen} HP Proofs (deciders within
Date: Wed, 16 Dec 2020 19:40:50 -0600
Organization: A noiseless patient Spider
Lines: 198
Approved: fbkotler@myfairpoint.net - comp.lang.asm.x86 moderation team.
Message-ID: <U9GdnYVTzZu-KkfCnZ2dnUU7-TPNnZ2d@giganews.com>
References: <3JSdnRrpiNHInV3CnZ2dnUU7-YHNnZ2d@giganews.com>
<rr2oq2$ao3$1@dont-email.me> <35OdnezHsPxac0nCnZ2dnUU7-YvNnZ2d@giganews.com>
<rr2tlk$c32$1@dont-email.me> <zp6dnf8CEZuHnUjCnZ2dnUU7-SfNnZ2d@giganews.com>
<rr2vb1$mhs$1@dont-email.me> <SrSdnbIYprUrnEjCnZ2dnUU7-U2dnZ2d@giganews.com>
<rr30u4$2ba$1@dont-email.me> <BcSdnZTygJfElkjCnZ2dnUU7-UednZ2d@giganews.com>
<rr340r$l9i$1@dont-email.me> <bo2dnRdK_KDeiEjCnZ2dnUU7-UnNnZ2d@giganews.com>
<rr34ok$rof$1@dont-email.me> <oaedncLQ-96MhEjCnZ2dnUU7-WnNnZ2d@giganews.com>
<rr36c2$7dk$1@dont-email.me> <-LCdnQjCJqk1vEjCnZ2dnUU7-eXNnZ2d@giganews.com>
<rr39me$tev$1@dont-email.me> <IdGdnS9EruNl6ErCnZ2dnUU7-QvNnZ2d@giganews.com>
<rr7tvl$h7a$1@dont-email.me> <DLCdnTdFDrYoHErCnZ2dnUU7-e3NnZ2d@giganews.com>
<7fbe5f35-e17b-4964-888d-ef038a6a2126n@googlegroups.com>
<NuydnecrJuqQL0rCnZ2dnUU7-RHNnZ2d@giganews.com>
<20201214113311.509@kylheku.com>
<kcqdnSuH7702QkrCnZ2dnUU7-VvNnZ2d@giganews.com>
<rr9uag$1j0n$1@gioia.aioe.org>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Info: reader02.eternal-september.org; posting-host="4a23faa1200c6b29da9d0c80fbd9723f";
logging-data="6814"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+yBajPmD3YWPzl1odPtC+EoO1zLbNkh+s="
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.1
Cancel-Lock: sha1:irpPWYWAJvJ5LRFkpHtBTgw9His=
View all headers
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]
---[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
Input_Would_Halt = 0
.....[00000642](03)  83c408              add esp,+08
.....[00000645](01)  f4                  hlt

Every time that the same function is called from the same machine address a second time without any control flow instructions in-between is a case of infinite recursion.
This is shown at execution trace lines 14-22 above.

http://www.liarparadox.org/Peter_Linz_HP(Pages_315-320).pdf

Linz, Peter 1990. An Introduction to Formal Languages and Automata. Lexington/Toronto: D. C. Heath and Company.

http://www.liarparadox.org/sipser_165.pdf

Sipser, Michael 1997. Introduction to the Theory of Computation. Boston: PWS Publishing Company (165-167)

http://www.liarparadox.org/kozen_233.pdf

The Kozen computation is identical to the Peter Linz computation merely swapping function names Linz.H is swapped for Kozen.K and Linz.Ĥ is swapped for Kozen.N

Kozen, Dexter 1997. Automata and Computability. New York: Springer-Verlag. (231-234).


--
Copyright 2020 Pete Olcott

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



SubjectRepliesAuthor
o Re: Refuting the {Linz, Sipser and Kozen} HP Proofs (deciders within

By: olcott on Mon, 14 Dec 2020

25olcott
rocksolid light 0.7.2
clearneti2ptor