Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

With your bare hands?!?

computers / / Concise refutation of halting problem proofs V6 [ pure function ]

o Concise refutation of halting problem proofs V6 [ pure function ]olcott

Subject: Concise refutation of halting problem proofs V6 [ pure function ]
From: olcott
Newsgroups: comp.theory, sci.logic, sci.math,
Followup: comp.theory
Date: Thu, 11 Nov 2021 01:25 UTC
NNTP-Posting-Date: Wed, 10 Nov 2021 19:25:20 -0600
Date: Wed, 10 Nov 2021 19:25:18 -0600
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Newsgroups: comp.theory,sci.logic,sci.math,
Content-Language: en-US
From: (olcott)
Subject: Concise refutation of halting problem proofs V6 [ pure function ]
Followup-To: comp.theory
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <>
Lines: 95
X-Trace: sv3-syhHD6eA5gebxM1ENNupxSBSXqBCWHN6AijdmEzykU7rqsA/k9muVhlPDSbWFIYjBwGuMcwTEdWoonL!LYP1zd14oBOtvB7FyazGwxFra1USXKM2oQRtYMdkqDfcjlvA2xufHOGs9OK/ZZFrU5wM9/h5hX9D!7Q==
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 4949
View all headers
Within the definition of the x86 language H(P,P)==0 is a necessary consequence for every simulating halt decider H.

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

int main()
   Output("Input_Halts = ", H((u32)P, (u32)P));

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

  machine   stack     stack     machine    assembly
  address   address   data      code       language
  ========  ========  ========  =========  =============
[00000c56][0010172a][00000000] 55          push ebp
[00000c57][0010172a][00000000] 8bec        mov ebp,esp
[00000c59][00101726][00000c36] 68360c0000  push 00000c36 // push P
[00000c5e][00101722][00000c36] 68360c0000  push 00000c36 // push P
[00000c63][0010171e][00000c68] e8fefcffff  call 00000966 // call H(P,P)

Begin Local Halt Decider Simulation at Machine Address:c36
[00000c36][002117ca][002117ce] 55          push ebp
[00000c37][002117ca][002117ce] 8bec        mov ebp,esp
[00000c39][002117ca][002117ce] 8b4508      mov eax,[ebp+08]
[00000c3c][002117c6][00000c36] 50          push eax       // push P
[00000c3d][002117c6][00000c36] 8b4d08      mov ecx,[ebp+08]
[00000c40][002117c2][00000c36] 51          push ecx       // push P
[00000c41][002117be][00000c46] e820fdffff  call 00000966  // call H(P,P)

As Flibble pointed out the first time that the simulated P calls H(P,P) would seem to indicate infinite recursion because the currently running H is being called again with identical parameters.

Flibble's comment caused me to accept the truth  these words that I had previously written: (Before his comment I was not quite sure)

    Because H knows that it is a simulating halt decider it can
    know that the first time that its input calls itself with
    the same parameters this would be infinitely nested simulation.

[Olcott wrong about infinite recursion] comp.theory
On 11/10/2021 3:53 PM, Mr Flibble wrote:
 > Olcott is barking up the wrong tree re infinite recursion: there
 > is only a need to detect a single recursive call into the halt decider
 > and signal an exception.  Why?  Because infinite recursion is valid
 > program behavior.
 > /Flibble

This halt deciding criteria can also be equally applied when P is invoking H with a copy of its input. The only difference is that string_compare is invoked instead of integer compare.

Because the call is aborted before the next level simulation is initiated there is no need for static local data, thus this H is a pure function.

H uses the NumParams system to provide the number of parameters required by any function of the COFF object file. H finds that the NumParams("H") is 2. H then compares the top two elements pf P's stack its own parameters. If it has a match then its [abort and decide not halting] criteria have been met.

There is no need to maintain any static data across nested simulations because no nested simulation are ever created.

Copyright 2021 Pete Olcott

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

rocksolid light 0.7.2