Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Adapt. Enjoy. Survive.


computers / comp.ai.philosophy / Re: How do we know H(P,P)==0 is the correct halt status for the input to H?

Re: How do we know H(P,P)==0 is the correct halt status for the input to H?

<CbSdnazsjJLf6IP8nZ2dnUU7-KfNnZ2d@giganews.com>

  copy mid

https://www.novabbs.com/computers/article-flat.php?id=7263&group=comp.ai.philosophy#7263

  copy link   Newsgroups: comp.theory comp.ai.philosophy comp.software-eng sci.math.symbolic
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!peer03.ams4!peer.am4.highwinds-media.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 19 Aug 2021 10:14:10 -0500
Subject: Re: How do we know H(P,P)==0 is the correct halt status for the input
to H?
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng,sci.math.symbolic
References: <3YOdnecvDsA5Q4r8nZ2dnUU7-TXNnZ2d@giganews.com>
<87im06wiup.fsf@bsb.me.uk> <DJGdncQOXNbfHYT8nZ2dnUU7-dPNnZ2d@giganews.com>
<874kbqw62q.fsf@bsb.me.uk> <W7udnRlZduvgdof8nZ2dnUU7-IPNnZ2d@giganews.com>
<87h7fpuf5v.fsf@bsb.me.uk> <AsSdnUXVrYJ5nYb8nZ2dnUU7-VnNnZ2d@giganews.com>
<875yw4v08g.fsf@bsb.me.uk> <oKidneawW_dWu4H8nZ2dnUU7-emdnZ2d@giganews.com>
<8735r7u3ab.fsf@bsb.me.uk> <ufKdnZfZ0sUP3YH8nZ2dnUU7-SXNnZ2d@giganews.com>
<87wnojsjqd.fsf@bsb.me.uk> <ReKdnb2pB4SVyoH8nZ2dnUU7-SvNnZ2d@giganews.com>
<87o89usfll.fsf@bsb.me.uk> <uqadnd39oqwW-ID8nZ2dnUU7-amdnZ2d@giganews.com>
<87sfz6qpk9.fsf@bsb.me.uk> <PeqdnehLhMapOYD8nZ2dnUU7-YXNnZ2d@giganews.com>
<87k0kiqlmm.fsf@bsb.me.uk> <GPidnScbL8UfLoD8nZ2dnUU7-ROdnZ2d@giganews.com>
<875yw2qkfb.fsf@bsb.me.uk> <2q6dnZ-dGIzeIYD8nZ2dnUU7-ffNnZ2d@giganews.com>
<87r1eppoe5.fsf@bsb.me.uk>
From: NoO...@NoWhere.com (olcott)
Date: Thu, 19 Aug 2021 10:14:09 -0500
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.13.0
MIME-Version: 1.0
In-Reply-To: <87r1eppoe5.fsf@bsb.me.uk>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 7bit
Message-ID: <CbSdnazsjJLf6IP8nZ2dnUU7-KfNnZ2d@giganews.com>
Lines: 278
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-j7n6qSCQ+KjERO56FtgClylSvFV12xbkC4IM4+FeDJ7KMr8ydj1MF+DL+ptxnCi96DGfS7Ygg/EuW3M!YSLhTL00aw7pYv+esOHfQOaji76ujeqXdljjFxNm2PGpi0uA1D7XW/2Ee3hAUaz4FdxqG3vL9JKq!6qI=
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: 13751
X-Received-Bytes: 13964
 by: olcott - Thu, 19 Aug 2021 15:14 UTC

On 8/19/2021 8:14 AM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> On 8/18/2021 8:42 PM, Ben Bacarisse wrote:
>>> olcott <NoOne@NoWhere.com> writes:
>>>
>>>> On 8/18/2021 8:16 PM, Ben Bacarisse wrote:
>
>>>>> Yes. I cut them because they are not the specification of the function
>>>>> that I will challenge you to write.
>>>>
>>>> That is out-of-scope and you know it.
>>>
>>> Not in my opinion, no. A function that that shows there are undecidable
>>> sets should worry you, but for some reason you prefer to stick with
>>> talking about your H that does something entirely unsurprising and
>>> uninteresting.
>>
>> So when I correctly refute the halting problem proofs you say no I did
>> not refute every proof in the universe and the halting problem proof
>> is one of these proofs therefore I did not refute the halting problem
>> proof.
>
> No, I'm not saying that.
>
> Anyway, in case you are interested, here is the specification of the
> function you can't write:
>
> The computational model is C code with no memory restrictions. Of
> course, if you don't actually hit the memory limits of a C
> implementation it's just actual C code. I'd be happy to say more about
> this model of computation if you think the details will matter to your
> solution.
>
> The problem is that of deciding if a function would return if called
> from main. A "return decider" (in this model) is a C function returning
> _Bool that always returns a value to the expression in which it was
> called. A return decider always returns the same value for any
> arguments that represnet the same function call expression.
>
> Your mission, should you chose to accept it, is to write a return
> decider B with this prototype
>
> typedef uintptr_t data;
> typedef void (*function)(data);
>
> extern _Bool B(function, data);
>
> such that B(f, d) returns true if and only if a call of f from main with
> argument d returns to main. The two arguments, f and d, are said to
> represenet the call expression f(d).
>
> If, rather than just thinking you can do this, you have actual C code,
> you should provide either source or a compiled translation unit that can
> be linked with this one:
>
> #include <stdint.h>
> #include <stdio.h>
>
> typedef uintptr_t data;
> typedef void (*function)(data);
>
> extern _Bool B(function, data);
>
> void B_hat(data x) { if (B((function)x, x)) while (1); }
>
> int main(void)
> {
> printf("%d\n", B(B_hat, (data)B_hat));
> fflush(stdout);
> B_hat((data)B_hat);
> puts("returned");
> }
>
> The output should be either
>
> 1
> returned
>
> or
>
> 0
>
> with no further output. Of course you could always just agree that no
> such function B can be written.
>

The x86utm operating system cannot call any C functions.
Good job on the use of C. My own use of unsigned integers as function
pointers is unconventional and not as portable. I did this on purpose so
that x86utm would have a single standard tape element type.

#include <stdint.h>
#include <stdio.h>

typedef uintptr_t data;
typedef void (*function)(data);

extern _Bool B(function, data);

void B_hat(data x) { if (H((u32)x, (u32)x)) while (1); }

int main2()
{ OutputHex(H((u32)B_hat, (u32)B_hat));
B_hat((u32)B_hat);
OutputString("returned");
}

_B_hat()
[00000efc](01) 55 push ebp
[00000efd](02) 8bec mov ebp,esp
[00000eff](03) 8b4508 mov eax,[ebp+08]
[00000f02](01) 50 push eax
[00000f03](03) 8b4d08 mov ecx,[ebp+08]
[00000f06](01) 51 push ecx
[00000f07](05) e850feffff call 00000d5c
[00000f0c](03) 83c408 add esp,+08
[00000f0f](02) 85c0 test eax,eax
[00000f11](02) 740b jz 00000f1e
[00000f13](05) ba01000000 mov edx,00000001
[00000f18](02) 85d2 test edx,edx
[00000f1a](02) 7402 jz 00000f1e
[00000f1c](02) ebf5 jmp 00000f13
[00000f1e](01) 5d pop ebp
[00000f1f](01) c3 ret
Size in bytes:(0036) [00000f1f]

_main2()
[00000f2c](01) 55 push ebp
[00000f2d](02) 8bec mov ebp,esp
[00000f2f](05) 68fc0e0000 push 00000efc
[00000f34](05) 68fc0e0000 push 00000efc
[00000f39](05) e81efeffff call 00000d5c
[00000f3e](03) 83c408 add esp,+08
[00000f41](01) 50 push eax
[00000f42](05) e8e5f3ffff call 0000032c
[00000f47](03) 83c404 add esp,+04
[00000f4a](05) 68fc0e0000 push 00000efc
[00000f4f](05) e8a8ffffff call 00000efc
[00000f54](03) 83c404 add esp,+04
[00000f57](05) 6823030000 push 00000323
[00000f5c](05) e8dbf3ffff call 0000033c
[00000f61](03) 83c404 add esp,+04
[00000f64](01) 5d pop ebp
[00000f65](01) c3 ret
Size in bytes:(0058) [00000f65]

_main()
[00000f6c](01) 55 push ebp
[00000f6d](02) 8bec mov ebp,esp
[00000f6f](05) e8b8ffffff call 00000f2c
[00000f74](02) 33c0 xor eax,eax
[00000f76](01) 5d pop ebp
[00000f77](01) c3 ret
Size in bytes:(0012) [00000f77]

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
....[00000f6c][00101c0a][00000000] 55 push ebp
....[00000f6d][00101c0a][00000000] 8bec mov ebp,esp
....[00000f6f][00101c06][00000f74] e8b8ffffff call 00000f2c
....[00000f2c][00101c02][00101c0a] 55 push ebp
....[00000f2d][00101c02][00101c0a] 8bec mov ebp,esp
....[00000f2f][00101bfe][00000efc] 68fc0e0000 push 00000efc
....[00000f34][00101bfa][00000efc] 68fc0e0000 push 00000efc
....[00000f39][00101bf6][00000f3e] e81efeffff call 00000d5c

Begin Local Halt Decider Simulation at Machine Address:efc
....[00000efc][00211caa][00211cae] 55 push ebp
....[00000efd][00211caa][00211cae] 8bec mov ebp,esp
....[00000eff][00211caa][00211cae] 8b4508 mov eax,[ebp+08]
....[00000f02][00211ca6][00000efc] 50 push eax
....[00000f03][00211ca6][00000efc] 8b4d08 mov ecx,[ebp+08]
....[00000f06][00211ca2][00000efc] 51 push ecx
....[00000f07][00211c9e][00000f0c] e850feffff call 00000d5c
....[00000efc][0025c6d2][0025c6d6] 55 push ebp
....[00000efd][0025c6d2][0025c6d6] 8bec mov ebp,esp
....[00000eff][0025c6d2][0025c6d6] 8b4508 mov eax,[ebp+08]
....[00000f02][0025c6ce][00000efc] 50 push eax
....[00000f03][0025c6ce][00000efc] 8b4d08 mov ecx,[ebp+08]
....[00000f06][0025c6ca][00000efc] 51 push ecx
....[00000f07][0025c6c6][00000f0c] e850feffff call 00000d5c
Local Halt Decider: Infinite Recursion Detected Simulation Stopped
....[00000f3e][00101c02][00101c0a] 83c408 add esp,+08
....[00000f41][00101bfe][00000000] 50 push eax
---[00000f42][00101bfe][00000000] e8e5f3ffff call 0000032c
0 ....[00000f47][00101c02][00101c0a] 83c404 add esp,+04
....[00000f4a][00101bfe][00000efc] 68fc0e0000 push 00000efc
....[00000f4f][00101bfa][00000f54] e8a8ffffff call 00000efc
....[00000efc][00101bf6][00101c02] 55 push ebp
....[00000efd][00101bf6][00101c02] 8bec mov ebp,esp
....[00000eff][00101bf6][00101c02] 8b4508 mov eax,[ebp+08]
....[00000f02][00101bf2][00000efc] 50 push eax
....[00000f03][00101bf2][00000efc] 8b4d08 mov ecx,[ebp+08]
....[00000f06][00101bee][00000efc] 51 push ecx
....[00000f07][00101bea][00000f0c] e850feffff call 00000d5c

Begin Local Halt Decider Simulation at Machine Address:efc
....[00000efc][0026c772][0026c776] 55 push ebp
....[00000efd][0026c772][0026c776] 8bec mov ebp,esp
....[00000eff][0026c772][0026c776] 8b4508 mov eax,[ebp+08]
....[00000f02][0026c76e][00000efc] 50 push eax
....[00000f03][0026c76e][00000efc] 8b4d08 mov ecx,[ebp+08]
....[00000f06][0026c76a][00000efc] 51 push ecx
....[00000f07][0026c766][00000f0c] e850feffff call 00000d5c
....[00000efc][002b719a][002b719e] 55 push ebp
....[00000efd][002b719a][002b719e] 8bec mov ebp,esp
....[00000eff][002b719a][002b719e] 8b4508 mov eax,[ebp+08]
....[00000f02][002b7196][00000efc] 50 push eax
....[00000f03][002b7196][00000efc] 8b4d08 mov ecx,[ebp+08]
....[00000f06][002b7192][00000efc] 51 push ecx
....[00000f07][002b718e][00000f0c] e850feffff call 00000d5c
Local Halt Decider: Infinite Recursion Detected Simulation Stopped
....[00000f0c][00101bf6][00101c02] 83c408 add esp,+08
....[00000f0f][00101bf6][00101c02] 85c0 test eax,eax
....[00000f11][00101bf6][00101c02] 740b jz 00000f1e
....[00000f1e][00101bfa][00000f54] 5d pop ebp
....[00000f1f][00101bfe][00000efc] c3 ret
....[00000f54][00101c02][00101c0a] 83c404 add esp,+04
....[00000f57][00101bfe][00000323] 6823030000 push 00000323
---[00000f5c][00101bfe][00000323] e8dbf3ffff call 0000033c
returned
....[00000f61][00101c02][00101c0a] 83c404 add esp,+04
....[00000f64][00101c06][00000f74] 5d pop ebp
....[00000f65][00101c0a][00000000] c3 ret
....[00000f74][00101c0a][00000000] 33c0 xor eax,eax
....[00000f76][00101c0e][00100000] 5d pop ebp
....[00000f77][00101c12][00000008] c3 ret
Number_of_User_Instructions(2)
Number of Instructions Executed(47451)

The paradox is that H does correctly decide that its simulation of
_B_hat() on _B_hat() never halts and the execution of _B_hat() on
_B_hat() does halt. This paradox is explained by the fact these two
computations are not computationally equivalent to each other even
though intuition would seem to say that they are.

The key difference seems to be that there is a one-way dependency of
_B_hat() on H that is not a mutual dependency. H is free to do as it
chooses in deciding the halt status of its input. _B_hat() is a slave to
whatever value that H returns.

the Turing machine halting problem. Simply stated, the problem
is: given the description of a Turing machine M and an input w,
does M, when started in the initial configuration q0w, perform a
computation that eventually halts? (Linz:1990:317).

In computability theory, the halting problem is the problem of
determining, from a description of an arbitrary computer program
and an input, whether the program will finish running, or continue
to run forever. https://en.wikipedia.org/wiki/Halting_problem

Since it can be independently verified that H does correctly decide that
its input will never stop running unless it aborts its simulation of
this input we have met the halting problem burden of correctly deciding
the halt status of the input description of a machine/program.

The fact that the direct execution of P(P) halts does not contradict the
fact that H(P,P) correctly decides that its input never halts because
these two computations are not computationally equivalent.

The key difference seems to be the dependency of the execution of P(P)
on the return value of H(P,P) such that the execution of P(P) is a slave
to whatever value that H(P,P) returns. There is no corresponding reverse
dependency proving that these two computations are not computationally
equivalent.

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

SubjectRepliesAuthor
o How do we know H(P,P)==0 is the correct halt status for the input to

By: olcott on Sat, 14 Aug 2021

29olcott
server_pubkey.txt

rocksolid light 0.9.8
clearnet tor