Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

This system will self-destruct in five minutes.


devel / comp.theory / Re: How do we know that H correctly decides that P will never halt?

SubjectAuthor
* How do we know that H correctly decides that P will never halt?olcott
`- How do we know that H correctly decides that P will never halt?Richard Damon

1
How do we know that H correctly decides that P will never halt?

<B7mdnRoMatDLlkv9nZ2dnUU7-Q3NnZ2d@giganews.com>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=17198&group=comp.theory#17198

  copy link   Newsgroups: comp.theory comp.ai.philosophy comp.software-eng comp.lang.c
Followup: comp.theory
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!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: Fri, 25 Jun 2021 11:59:02 -0500
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng,comp.lang.c
X-Mozilla-News-Host: news://news.giganews.com:119
From: NoO...@NoWhere.com (olcott)
Subject: How do we know that H correctly decides that P will never halt?
Followup-To: comp.theory
Date: Fri, 25 Jun 2021 11:59:32 -0500
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.11.0
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 7bit
Message-ID: <B7mdnRoMatDLlkv9nZ2dnUU7-Q3NnZ2d@giganews.com>
Lines: 158
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-OO3SFdBd5A5q5Aza0wmVYv/pJrHelpSX6QmF7ReAc3D4Gy3J+W69SNQ6qAAIyTHL3E8fiSL148JTCZP!pH0SfDzgsOi61zivh6hK82Bqbl93xc10zuEmwk4d1GEnC2u1eJAICGnoCNkvDCcLxdekWu+hCTw=
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: 7968
 by: olcott - Fri, 25 Jun 2021 16:59 UTC

Of every possible (correct or incorrect) encoding of simulating partial
halt decider H that can possibly exist H either aborts the simulation of
its input or does not abort the simulation of its input.

If the computation P(P) never halts if H never aborts its simulation of
P then we can know for sure that the computation P(P) specifies an
infinite chain of invocations that must be aborted at some point.

Premise(1) (axiom) Every computation that never halts unless its
simulation is aborted is a computation that never halts. This verified
as true on the basis of the meaning of its words.

Premise(2) (verified fact) The simulation of the input to H(P,P) never
halts without being aborted is a verified fact on the basis of its x86
execution trace. (shown below).

Conclusion(3) From the above true premises it necessarily follows that
simulating halt decider H correctly reports that its input: (P,P) never
halts.

void P(u32 x)
{ u32 Input_Halts = H(x, x);
if (Input_Halts)
HERE: goto HERE;
}

int main()
{ P((u32)P);
}

_P()
[00000b25](01) 55 push ebp
[00000b26](02) 8bec mov ebp,esp
[00000b28](01) 51 push ecx
[00000b29](03) 8b4508 mov eax,[ebp+08]
[00000b2c](01) 50 push eax
[00000b2d](03) 8b4d08 mov ecx,[ebp+08]
[00000b30](01) 51 push ecx
[00000b31](05) e81ffeffff call 00000955
[00000b36](03) 83c408 add esp,+08
[00000b39](03) 8945fc mov [ebp-04],eax
[00000b3c](04) 837dfc00 cmp dword [ebp-04],+00
[00000b40](02) 7402 jz 00000b44
[00000b42](02) ebfe jmp 00000b42
[00000b44](02) 8be5 mov esp,ebp
[00000b46](01) 5d pop ebp
[00000b47](01) c3 ret
Size in bytes:(0035) [00000b47]

_main()
[00000c05](01) 55 push ebp
[00000c06](02) 8bec mov ebp,esp
[00000c08](05) 68250b0000 push 00000b25
[00000c0d](05) e813ffffff call 00000b25
[00000c12](03) 83c404 add esp,+04
[00000c15](02) 33c0 xor eax,eax
[00000c17](01) 5d pop ebp
[00000c18](01) c3 ret
Size in bytes:(0020) [00000c18]

Columns
(1) Machine address of instruction
(2) Machine address of top of stack
(3) Value of top of stack after instruction executed
(4) Machine language bytes
(5) Assembly language text
===============================
....[00000c05][0010165e][00000000](01) 55 push ebp
....[00000c06][0010165e][00000000](02) 8bec mov ebp,esp
....[00000c08][0010165a][00000b25](05) 68250b0000 push 00000b25
....[00000c0d][00101656][00000c12](05) e813ffffff call 00000b25
....[00000b25][00101652][0010165e](01) 55 push ebp
....[00000b26][00101652][0010165e](02) 8bec mov ebp,esp
....[00000b28][0010164e][00000000](01) 51 push ecx
....[00000b29][0010164e][00000000](03) 8b4508 mov eax,[ebp+08]
....[00000b2c][0010164a][00000b25](01) 50 push eax
....[00000b2d][0010164a][00000b25](03) 8b4d08 mov ecx,[ebp+08]
....[00000b30][00101646][00000b25](01) 51 push ecx
....[00000b31][00101642][00000b36](05) e81ffeffff call 00000955

Begin Local Halt Decider Simulation at Machine Address:b25
....[00000b25][002116fe][00211702](01) 55 push ebp
....[00000b26][002116fe][00211702](02) 8bec mov ebp,esp
....[00000b28][002116fa][002016ce](01) 51 push ecx
....[00000b29][002116fa][002016ce](03) 8b4508 mov eax,[ebp+08]
....[00000b2c][002116f6][00000b25](01) 50 push eax
....[00000b2d][002116f6][00000b25](03) 8b4d08 mov ecx,[ebp+08]
....[00000b30][002116f2][00000b25](01) 51 push ecx
....[00000b31][002116ee][00000b36](05) e81ffeffff call 00000955
....[00000b25][0025c126][0025c12a](01) 55 push ebp
....[00000b26][0025c126][0025c12a](02) 8bec mov ebp,esp
....[00000b28][0025c122][0024c0f6](01) 51 push ecx
....[00000b29][0025c122][0024c0f6](03) 8b4508 mov eax,[ebp+08]
....[00000b2c][0025c11e][00000b25](01) 50 push eax
....[00000b2d][0025c11e][00000b25](03) 8b4d08 mov ecx,[ebp+08]
....[00000b30][0025c11a][00000b25](01) 51 push ecx
....[00000b31][0025c116][00000b36](05) e81ffeffff call 00000955
Local Halt Decider: Infinite Recursion Detected Simulation Stopped
....[00000b36][0010164e][00000000](03) 83c408 add esp,+08
....[00000b39][0010164e][00000000](03) 8945fc mov [ebp-04],eax
....[00000b3c][0010164e][00000000](04) 837dfc00 cmp dword
[ebp-04],+00
....[00000b40][0010164e][00000000](02) 7402 jz 00000b44
....[00000b44][00101652][0010165e](02) 8be5 mov esp,ebp
....[00000b46][00101656][00000c12](01) 5d pop ebp
....[00000b47][0010165a][00000b25](01) c3 ret
....[00000c12][0010165e][00000000](03) 83c404 add esp,+04
....[00000c15][0010165e][00000000](02) 33c0 xor eax,eax
....[00000c17][00101662][00100000](01) 5d pop ebp
....[00000c18][00101666][00000098](01) c3 ret
Number_of_User_Instructions(39)
Number of Instructions Executed(26459)

In the computation P(P) if any invocation of the infinite chain of
invocations must be aborted to prevent the infinite execution of this
chain then we know that the computation: P(P) does specify an infinite
chain of invocations.

Whenever P calls H(P,P) H must abort its simulation of P. The above
computation P(P) calls H(P,P) which is the first invocation of an
infinite sequence of invocations.

It is common knowledge that any invocation of an infinite sequence of
invocations (such as infinite recursion or infinitely nested simulation)
is terminated then the entire sequence halts.

In the computation P(P) the third element of the infinite sequence of
invocations is terminated.

The only reason that any P ever halts is that some H aborted some P.
This proves (axiomatically) that P(P) really does specify an infinite
invocation chain.

(Axiom) Every computation that never halts unless its simulation is
aborted is a computation that never halts. This verified as true on the
basis of the meaning of its words.

Halting problem undecidability and infinitely nested
https://www.researchgate.net/publication/351947980_Halting_problem_undecidability_and_infinitely_nested_simulation

--
Copyright 2021 Pete Olcott

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

Re: How do we know that H correctly decides that P will never halt?

<LpoBI.263$al1.225@fx26.iad>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=17200&group=comp.theory#17200

  copy link   Newsgroups: comp.theory
Path: i2pn2.org!i2pn.org!paganini.bofh.team!news.dns-netz.com!news.freedyn.net!newsfeed.xs4all.nl!newsfeed7.news.xs4all.nl!peer02.ams4!peer.am4.highwinds-media.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx26.iad.POSTED!not-for-mail
Subject: Re: How do we know that H correctly decides that P will never halt?
Newsgroups: comp.theory
References: <B7mdnRoMatDLlkv9nZ2dnUU7-Q3NnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:78.0)
Gecko/20100101 Thunderbird/78.11.0
MIME-Version: 1.0
In-Reply-To: <B7mdnRoMatDLlkv9nZ2dnUU7-Q3NnZ2d@giganews.com>
Content-Type: text/plain; charset=utf-8
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Lines: 207
Message-ID: <LpoBI.263$al1.225@fx26.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Fri, 25 Jun 2021 13:31:24 -0400
X-Received-Bytes: 10882
 by: Richard Damon - Fri, 25 Jun 2021 17:31 UTC

On 6/25/21 12:59 PM, olcott wrote:
> Of every possible (correct or incorrect) encoding of simulating partial
> halt decider H that can possibly exist H either aborts the simulation of
> its input or does not abort the simulation of its input.
>
> If the computation P(P) never halts if H never aborts its simulation of
> P then we can know for sure that the computation P(P) specifies an
> infinite chain of invocations that must be aborted at some point.
>

Problem in definition. Each possible H has its own P, so this logic
doesn't follow.

Yes, an H that doesn't abort P will create a P that is non-halting, but
that H can't say that as it will be non-halting itself.

The fact that H can abort its simulation of P, now has a different P
than all of the above cases, so the conclusion we got from that doesn't
apply.

You are neglecting the fact that P is dependent on the definition of H.
>
>
>
> Premise(1) (axiom) Every computation that never halts unless its
> simulation is aborted is a computation that never halts. This verified
> as true on the basis of the meaning of its words.
>

And this means that if the GIVEN INSTANCE of the simulation doesn't
terminate the simulation of a computation, and then the computation
doesn't end, that shows that that computaiton is non-halting.

Since the case we are looking at presumes that H will answer the
question H(P,P), then we can show that if we change just that top level
simulation to not halt (so we keep the computation the same) that this
computation DOES halt, thus this Premise doesn't activate.

This premise can only activate for Hs that never abort their simulation
of P, and those Hs will never answer H(P,P) and thus never are
candidates that need to be refuted.

> Premise(2) (verified fact) The simulation of the input to H(P,P) never
> halts without being aborted is a verified fact on the basis of its x86
> execution trace. (shown below).

FAUTY INTERPRETATION OF THE TRACE.

This trace actually shows that P(P) DOES HALT. That actual invocation of
P was never aborted, only a simulation of it inside its logic, and the
trace shows that P then does come to a stop in a finite number of steps,
which is the DEFINITION of Halting.

Thus H given an input of P,P decided incorrectly that P would never end,
and then gives that answer to P and it ends.

The fundamental issue is that H doesn't analysis the trace correctly
because it is built using faulty rules that ignore the action of the H
that is part of the computation under simulation. Faulty tracing leads
to faulty decisions. The actual trace needs to either actually trace the
operation of H within the simulated P, or include the fact that there is
a conditional operation here that might be able to abort the operation here.

Failure to do this leads to an incorrect determination of infinite
recursion.

One side note, in computation theory there is no distinction between
'User Instructions' and 'Instructions' Everything inside a computation
is the instructions for the computation. You don't 'leave' the
computation in the middle of it for some 'non-user' operation.

>
> Conclusion(3) From the above true premises it necessarily follows that
> simulating halt decider H correctly reports that its input: (P,P) never
> halts.
>
> void P(u32 x)
> {
>   u32 Input_Halts = H(x, x);
>   if (Input_Halts)
>     HERE: goto HERE;
> }
>
> int main()
> {
>   P((u32)P);
> }
>
> _P()
> [00000b25](01)  55              push ebp
> [00000b26](02)  8bec            mov ebp,esp
> [00000b28](01)  51              push ecx
> [00000b29](03)  8b4508          mov eax,[ebp+08]
> [00000b2c](01)  50              push eax
> [00000b2d](03)  8b4d08          mov ecx,[ebp+08]
> [00000b30](01)  51              push ecx
> [00000b31](05)  e81ffeffff      call 00000955
> [00000b36](03)  83c408          add esp,+08
> [00000b39](03)  8945fc          mov [ebp-04],eax
> [00000b3c](04)  837dfc00        cmp dword [ebp-04],+00
> [00000b40](02)  7402            jz 00000b44
> [00000b42](02)  ebfe            jmp 00000b42
> [00000b44](02)  8be5            mov esp,ebp
> [00000b46](01)  5d              pop ebp
> [00000b47](01)  c3              ret
> Size in bytes:(0035) [00000b47]
>
> _main()
> [00000c05](01)  55              push ebp
> [00000c06](02)  8bec            mov ebp,esp
> [00000c08](05)  68250b0000      push 00000b25
> [00000c0d](05)  e813ffffff      call 00000b25
> [00000c12](03)  83c404          add esp,+04
> [00000c15](02)  33c0            xor eax,eax
> [00000c17](01)  5d              pop ebp
> [00000c18](01)  c3              ret
> Size in bytes:(0020) [00000c18]
>
> Columns
> (1) Machine address of instruction
> (2) Machine address of top of stack
> (3) Value of top of stack after instruction executed
> (4) Machine language bytes
> (5) Assembly language text
> ===============================
> ...[00000c05][0010165e][00000000](01)  55              push ebp
> ...[00000c06][0010165e][00000000](02)  8bec            mov ebp,esp
> ...[00000c08][0010165a][00000b25](05)  68250b0000      push 00000b25
> ...[00000c0d][00101656][00000c12](05)  e813ffffff      call 00000b25
> ...[00000b25][00101652][0010165e](01)  55              push ebp
> ...[00000b26][00101652][0010165e](02)  8bec            mov ebp,esp
> ...[00000b28][0010164e][00000000](01)  51              push ecx
> ...[00000b29][0010164e][00000000](03)  8b4508          mov eax,[ebp+08]
> ...[00000b2c][0010164a][00000b25](01)  50              push eax
> ...[00000b2d][0010164a][00000b25](03)  8b4d08          mov ecx,[ebp+08]
> ...[00000b30][00101646][00000b25](01)  51              push ecx
> ...[00000b31][00101642][00000b36](05)  e81ffeffff      call 00000955
>
>
>
>
>
> Begin Local Halt Decider Simulation at Machine Address:b25
> ...[00000b25][002116fe][00211702](01)  55              push ebp
> ...[00000b26][002116fe][00211702](02)  8bec            mov ebp,esp
> ...[00000b28][002116fa][002016ce](01)  51              push ecx
> ...[00000b29][002116fa][002016ce](03)  8b4508          mov eax,[ebp+08]
> ...[00000b2c][002116f6][00000b25](01)  50              push eax
> ...[00000b2d][002116f6][00000b25](03)  8b4d08          mov ecx,[ebp+08]
> ...[00000b30][002116f2][00000b25](01)  51              push ecx
> ...[00000b31][002116ee][00000b36](05)  e81ffeffff      call 00000955
> ...[00000b25][0025c126][0025c12a](01)  55              push ebp
> ...[00000b26][0025c126][0025c12a](02)  8bec            mov ebp,esp
> ...[00000b28][0025c122][0024c0f6](01)  51              push ecx
> ...[00000b29][0025c122][0024c0f6](03)  8b4508          mov eax,[ebp+08]
> ...[00000b2c][0025c11e][00000b25](01)  50              push eax
> ...[00000b2d][0025c11e][00000b25](03)  8b4d08          mov ecx,[ebp+08]
> ...[00000b30][0025c11a][00000b25](01)  51              push ecx
> ...[00000b31][0025c116][00000b36](05)  e81ffeffff      call 00000955
> Local Halt Decider: Infinite Recursion Detected Simulation Stopped
> ...[00000b36][0010164e][00000000](03)  83c408          add esp,+08
> ...[00000b39][0010164e][00000000](03)  8945fc          mov [ebp-04],eax
> ...[00000b3c][0010164e][00000000](04)  837dfc00        cmp dword
> [ebp-04],+00
> ...[00000b40][0010164e][00000000](02)  7402            jz 00000b44
> ...[00000b44][00101652][0010165e](02)  8be5            mov esp,ebp
> ...[00000b46][00101656][00000c12](01)  5d              pop ebp
> ...[00000b47][0010165a][00000b25](01)  c3              ret
> ...[00000c12][0010165e][00000000](03)  83c404          add esp,+04
> ...[00000c15][0010165e][00000000](02)  33c0            xor eax,eax
> ...[00000c17][00101662][00100000](01)  5d              pop ebp
> ...[00000c18][00101666][00000098](01)  c3              ret
> Number_of_User_Instructions(39)
> Number of Instructions Executed(26459)
>
>
> In the computation P(P) if any invocation of the infinite chain of
> invocations must be aborted to prevent the infinite execution of this
> chain then we know that the computation: P(P) does specify an infinite
> chain of invocations.
>
> Whenever P calls H(P,P) H must abort its simulation of P. The above
> computation P(P) calls H(P,P) which is the first invocation of an
> infinite sequence of invocations.
>
> It is common knowledge that any invocation of an infinite sequence of
> invocations (such as infinite recursion or infinitely nested simulation)
> is terminated then the entire sequence halts.
>
> In the computation P(P) the third element of the infinite sequence of
> invocations is terminated.
>
> The only reason that any P ever halts is that some H aborted some P.
> This proves (axiomatically) that P(P) really does specify an infinite
> invocation chain.
>
> (Axiom) Every computation that never halts unless its simulation is
> aborted is a computation that never halts. This verified as true on the
> basis of the meaning of its words.
>
>
> Halting problem undecidability and infinitely nested
> https://www.researchgate.net/publication/351947980_Halting_problem_undecidability_and_infinitely_nested_simulation
>
>
>


Click here to read the complete article

devel / comp.theory / Re: How do we know that H correctly decides that P will never halt?

1
server_pubkey.txt

rocksolid light 0.9.81
clearnet tor