Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.theory > #50254

Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]

Show all headers | View raw

On 5/11/22 10:24 AM, olcott wrote:
> On 5/11/2022 8:21 AM, Ben wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> On 5/10/2022 10:50 AM, Ben wrote:
>>>> olcott <NoOne@NoWhere.com> writes:
>>>>
>>>>> (a) Verify that the execution trace of P by H is correct by comparing
>>>>> this execution trace to the ax86 source-code of P.
>>>>
>>>> P called with what argument?  I assume P.
>>
>> You won't even correct a trivial point.
>>
>>>>> (b) Verify that this execution trace shows that P is stuck in
>>>>> infinitely nested simulation (a non-halting behavior).
>>>>
>>>> Something is wrong in your code if P(P), or a simulation of P(P), does
>>>> not halt, since you told us that it does.  Post the code and someone
>>>> will help you find the bug.
>>
>> Don't you want to know what's wrong with your code?  Your trace shows
>> that you are not even nesting any simulations so that's one error right
>> there.  But there are clearly others.
>>
> 
> Here is the same trace that also shows the recursive simulation memory 
> allocations. I erase them because they are distracting.
> 
> _main()
> [00001372](01)  55              push ebp
> [00001373](02)  8bec            mov ebp,esp
> [00001375](05)  6852130000      push 00001352
> [0000137a](05)  6852130000      push 00001352
> [0000137f](05)  e81efeffff      call 000011a2
> [00001384](03)  83c408          add esp,+08
> [00001387](01)  50              push eax
> [00001388](05)  6823040000      push 00000423
> [0000138d](05)  e8e0f0ffff      call 00000472
> [00001392](03)  83c408          add esp,+08
> [00001395](02)  33c0            xor eax,eax
> [00001397](01)  5d              pop ebp
> [00001398](01)  c3              ret
> Size in bytes:(0039) [00001398]
> 
>   machine   stack     stack     machine    assembly
>   address   address   data      code       language
>   ========  ========  ========  =========  =============
> ...[00001372][0010229e][00000000] 55              push ebp
> ...[00001373][0010229e][00000000] 8bec            mov ebp,esp
> ...[00001375][0010229a][00001352] 6852130000      push 00001352
> ...[0000137a][00102296][00001352] 6852130000      push 00001352
> ...[0000137f][00102292][00001384] e81efeffff      call 000011a2
> --Allocation[002022b2](00000018)
> --Allocation[002022d2](00000034)
> --Allocation[0020230e](00000034)
> --Allocation[0020234a](00010000)
> New slave_stack @20234a
> --Allocation[00212352](0003a980)
> 
> Begin Local Halt Decider Simulation   Execution Trace Stored at:212352
> H_Root:1
> ...[00001352][0021233e][00212342] 55              push ebp
> ...[00001353][0021233e][00212342] 8bec            mov ebp,esp
> ...[00001355][0021233e][00212342] 8b4508          mov eax,[ebp+08]
> ...[00001358][0021233a][00001352] 50              push eax
> ...[00001359][0021233a][00001352] 8b4d08          mov ecx,[ebp+08]
> ...[0000135c][00212336][00001352] 51              push ecx
> ...[0000135d][00212332][00001362] e840feffff      call 000011a2
> --Allocation[0024ccda](00000018)
> --Allocation[0024ccfa](00000034)
> --Allocation[0024cd36](00000034)
> --Allocation[0024cd72](00010000)
> New slave_stack @24cd72

So, is the following execution now UNCONDITIONAL, or is there an implied 
condition between each instruction as the simulator decides if it is 
going to continue.

Note, that the operation of converting a trace of a simulation into a 
trace of the simulated machine is only valid for UNCONDITIONAL 
simulation. If the simulation is conditional, at a minimum you need to 
mark the conditional or interprete with the implied conditionals.



> H_Root:0
> ...[00001352][0025cd66][0025cd6a] 55              push ebp
> ...[00001353][0025cd66][0025cd6a] 8bec            mov ebp,esp
> ...[00001355][0025cd66][0025cd6a] 8b4508          mov eax,[ebp+08]
> ...[00001358][0025cd62][00001352] 50              push eax
> ...[00001359][0025cd62][00001352] 8b4d08          mov ecx,[ebp+08]
> ...[0000135c][0025cd5e][00001352] 51              push ecx
> ...[0000135d][0025cd5a][00001362] e840feffff      call 000011a2
> Local Halt Decider: Infinite Recursion Detected Simulation Stopped

Which, is invalid since it is ignoring the implied conditionals between 
all of the above instructions.

UNSOUND LOGIC.

> ...[00001384][0010229e][00000000] 83c408          add esp,+08
> ...[00001387][0010229a][00000000] 50              push eax
> ...[00001388][00102296][00000423] 6823040000      push 00000423
> ---[0000138d][00102296][00000423] e8e0f0ffff      call 00000472
> Input_Halts = 0
> ...[00001392][0010229e][00000000] 83c408          add esp,+08
> ...[00001395][0010229e][00000000] 33c0            xor eax,eax
> ...[00001397][001022a2][00100000] 5d              pop ebp
> ...[00001398][001022a6][00000004] c3              ret
> Number_of_User_Instructions(1)
> Number of Instructions Executed(15892)
> 
> 
> 
>>>>> #include <stdint.h>
>>>>> #define u32 uint32_t
>>>>>
>>>>> void P(u32 x)
>>>>> {
>>>>>     if (H(x, x))
>>>>>       HERE: goto HERE;
>>>>>     return;
>>>>> }
>>>>>
>>>>> int main()
>>>>> {
>>>>>     Output("Input_Halts = ", H((u32)P, (u32)P));
>>>>> }
>>>>
>>>> Unless you are retracting any of the facts you have previously stated,
>>>> we know (because you've told us) that H(P,P) returns 0 and we know
>>>> (because you've told us) that P(P) halts.  The trace of the execution
>>>> will either confirm this, or the trace is faulty.  Nothing new can come
>>>> from looking at traces of mystery code.
>>
>> Are you retracting any of the facts you have previously stated?  If not,
>> you are, as you no doubt know by now, wrong by definition.
>>
>>> (a) The trace is verifiably correct if one has the technical skill.
>>
>> A trace is neither correct not incorrect. 
> 
> That seems to be a weasel worded way to attempt to derive a fake 
> rebuttal. The trace of the repeated first seven instructions of the 
> simulated P corresponds to the behavior specified by these first seven 
> instructions in the x86 source code of P.

WRONG. You have an incorrect trace unless H UNCONDITIONAL executes the 
input, but it can't since it is shown to abort,

Thus YOU LIE about the trace.

> 
>>  It just shows a (partial)
>> program execution.  It "correctly" shows that H is not doing what you
>> claim (it shows no nested simulation) so maybe that means it's
>> "incorrect"?
>>
> 
> I added the nested simulation memory allocation details.

But not the actual nested simulation details

You imply unconditional simulation, when it is conditional.

> 
>>> (b) The trace is proved non-halting if one has the technical skill.
>>> You simply don't seem to have the technical skill.
>>
>> The trace shows H not doing what you claim.  The fact that don't address
>> this gross misdirection on your part make it more a lie than an error.
>>
> 
> The trace conclusively proves that H does correctly simulate two of the 
> nested simulations that the x86 source-code of P specifies.

Nope, it proves it INCORRECTLY simulates the nested simulation.

> 
>>> I PUT BACK IN THE MANDATORY DETAILS THAT PROVE MY POINT THAT YOU
>>> ERASED.
>>
>> There's no point in repeatedly posting a trace that it at best the wrong
>> one and at worst a lie. 
> 
> That you say it is wrong or a lie without understanding it is itself 
> wholly dishonest. If you don't understand it then you have no basis to 
> say that it is wrong. The most that you can honestly say is that you 
> don't understand how it could be correct.

Nope, shows you don't understand how nested simulations actually works.

> 
>>  The right trace to post (again) would be the
>> one showing P(P) halting.
>>
>> Obviously, you'd like people to talk about something other than the bald
>> fact that you are wrong by definition: H(P,P) == false "even though P(P)
>> halts" (your words).
>>
> 
> (a) The correct simulation of the input to H(P,P) never halts.

WRONG.

> (b) The correct simulation of the input to H1(P,P) halts.

SAME INPUT, thus differing simulations prove that one is wrong.

> (c) The direct execution of P(P) halts.

Which proves what the CORRECT simulation must do.

> 
> (b) and (c) are computationally equivalent.
> (a) and (b) are NOT computationally equivalent.
> 

Thus H is NOT a Halt Decider, but just a POOP decider.

(H1 isn't one either, as it will fail the same way for a P1 built on H1 
instead of H).

Back to comp.theory | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] olcott <NoOne@NoWhere.com> - 2022-05-10 07:26 -0500
  Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] wij <wyniijj2@gmail.com> - 2022-05-10 07:55 -0700
  Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] Ben <ben.usenet@bsb.me.uk> - 2022-05-10 16:50 +0100
    Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] olcott <NoOne@NoWhere.com> - 2022-05-10 23:47 -0500
      Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] Richard Damon <Richard@Damon-Family.org> - 2022-05-11 07:16 -0400
      Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] Ben <ben.usenet@bsb.me.uk> - 2022-05-11 14:21 +0100
        Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] olcott <NoOne@NoWhere.com> - 2022-05-11 09:24 -0500
          Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] Ben <ben.usenet@bsb.me.uk> - 2022-05-11 20:51 +0100
          Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] Richard Damon <Richard@Damon-Family.org> - 2022-05-11 19:42 -0400
    Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] olcott <NoOne@NoWhere.com> - 2022-05-11 09:07 -0500
      Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] Ben <ben.usenet@bsb.me.uk> - 2022-05-11 20:54 +0100
        Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] olcott <NoOne@NoWhere.com> - 2022-05-11 16:35 -0500
          Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] Ben <ben.usenet@bsb.me.uk> - 2022-05-12 01:25 +0100
            Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] olcott <NoOne@NoWhere.com> - 2022-05-11 19:38 -0500
              Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] Richard Damon <Richard@Damon-Family.org> - 2022-05-11 20:59 -0400
              Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] Ben <ben.usenet@bsb.me.uk> - 2022-05-12 02:24 +0100
                Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]( will keep repeating until understood ) olcott <NoOne@NoWhere.com> - 2022-05-11 21:46 -0500
                Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]( will keep repeating until understood ) Richard Damon <Richard@Damon-Family.org> - 2022-05-11 23:10 -0400
                Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]( will keep repeating until understood ) Ben <ben.usenet@bsb.me.uk> - 2022-05-12 21:32 +0100
  Re: Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ] wij <wyniijj2@gmail.com> - 2022-05-13 12:38 -0700

csiph-web