Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

I've looked at the listing, and it's right! -- Joel Halpern


computers / comp.ai.philosophy / Concise refutation of halting problem proofs V13

SubjectAuthor
o Concise refutation of halting problem proofs V13olcott

1
Subject: Concise refutation of halting problem proofs V13
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, sci.logic, sci.math
Followup: comp.theory
Date: Sun, 14 Nov 2021 19:17 UTC
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 14 Nov 2021 13:17:03 -0600
Date: Sun, 14 Nov 2021 13:17:01 -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,comp.ai.philosophy,sci.logic,sci.math
Content-Language: en-US
Followup-To: comp.theory
From: NoO...@NoWhere.com (olcott)
Subject: Concise refutation of halting problem proofs V13
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <9-SdnVXt2voy_Qz8nZ2dnUU7-cPNnZ2d@giganews.com>
Lines: 87
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-19yP7sfkL7MvYN+VdkU+tR8bxWrYCmzkrP8FaFIeEIz8j68g1jwC7K3p9cXq/Lg3KNtbTCoc5V2UL0t!I1wQ0WbiFu7fy92iJXYox8GYYwag1NFgmzqiPdXXvhRCCfCyFkFRLsZS5LXW6L1WxPNqKL8amxA2!lA==
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: 4056
View all headers
computation that halts
a computation is said to halt whenever it enters a final state. (Linz:1990:234)

computer science decider
a decider is a machine that accepts or rejects inputs.
https://cs.stackexchange.com/questions/84433/what-is-decider

halt decider
A halt decider accepts or rejects inputs on the basis of the actual behavior specified by these inputs. Whenever the direct execution or pure simulation of an input would never reach
its final state this input is correctly decided as not halting.

#include <stdint.h>
typedef void (*ptr)();

int H(ptr x, ptr y)
{
   x(y);  // direct execution of P(P)
   return 1;
}

// Minimal essence of Linz(1990) Ĥ
// and Strachey(1965) P
void P(ptr x)
{
   H(x, x);
}

int main(void)
{
   H(P, P);
}

Proof that H(P,P)==0 is correct for every possible H at machine address 00001a7e that simulates or executes the precise byte sequence shown below:

_P()
[00001a5e](01)  55              push ebp
[00001a5f](02)  8bec            mov ebp,esp
[00001a61](03)  8b4508          mov eax,[ebp+08]
[00001a64](01)  50              push eax        // push P
[00001a65](03)  8b4d08          mov ecx,[ebp+08]
[00001a68](01)  51              push ecx        // push P
[00001a69](05)  e810000000      call 00001a7e   // call H
[00001a6e](03)  83c408          add esp,+08
[00001a71](01)  5d              pop ebp
[00001a72](01)  c3              ret
Size in bytes:(0021) [00001a72]

P is defined as the above precise byte sequence.
The x86 language is the entire inference basis.

For every possible H  defined at machine address 00001a7e that has input (P,P) when the input to H(P,P) is executed or simulated this input is either infinitely recursive or aborted at some point. In no case does the input ever reach its final state of 00001a72.

Now that we have verified that the input to H(P,P) never halts we know that the correct return value for any correct halt decider H(P,P) must be 0.

To determine the correct halt status of the input to H(P,P) H merely needs to simulate its input one instruction at a time until H sees P call itself with the same parameters that it was called with. When H sees this H correctly returns 0 for not halting.


Strachey, C 1965.  An impossible program The Computer Journal, Volume 7, Issue 4, January 1965, Page 313, https://doi.org/10.1093/comjnl/7.4.313

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


Halting problem undecidability and infinitely nested simulation (V2)
November 2021 PL Olcott

https://www.researchgate.net/publication/356105750_Halting_problem_undecidability_and_infinitely_nested_simulation_V2

--
Copyright 2021 Pete Olcott

Talent hits a target no one else can hit;
Genius hits a target no one else can see.
Arthur Schopenhauer


1
rocksolid light 0.7.2
clearneti2ptor