Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

With your bare hands?!?


computers / comp.ai.philosophy / Concise refutation of halting problem proofs V6 [ pure function ]

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

1
Subject: Concise refutation of halting problem proofs V6 [ pure function ]
From: olcott
Newsgroups: comp.theory, sci.logic, sci.math, comp.ai.philosophy
Followup: comp.theory
Date: Thu, 11 Nov 2021 01:25 UTC
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
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
Thunderbird/91.3.0
Newsgroups: comp.theory,sci.logic,sci.math,comp.ai.philosophy
Content-Language: en-US
From: NoO...@NoWhere.com (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: <lI6dnb9sRP2d7BH8nZ2dnUU7-anNnZ2d@giganews.com>
Lines: 95
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-syhHD6eA5gebxM1ENNupxSBSXqBCWHN6AijdmEzykU7rqsA/k9muVhlPDSbWFIYjBwGuMcwTEdWoonL!LYP1zd14oBOtvB7FyazGwxFra1USXKM2oQRtYMdkqDfcjlvA2xufHOGs9OK/ZZFrU5wM9/h5hX9D!7Q==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
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));
}

_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. https://en.wikipedia.org/wiki/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


1
rocksolid light 0.7.2
clearneti2ptor