Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

A programming language is low level when its programs require attention to the irrelevant.


computers / comp.ai.philosophy / Re: Definition of primitive recursive function (wiki) [ H(P,P)==0 is always correct ]

SubjectAuthor
o Re: Definition of primitive recursive function (wiki) [ H(P,P)==0 is alwayolcott

1
Subject: Re: Definition of primitive recursive function (wiki) [ H(P,P)==0 is always correct ]
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng, sci.math.symbolic
Date: Mon, 2 Aug 2021 16:54 UTC
References: 1
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!news.uzoreto.com!feeder.usenetexpress.com!tr1.eu1.usenetexpress.com!newsfeed.xs4all.nl!newsfeed9.news.xs4all.nl!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer03.ams1!peer.ams1.xlned.com!news.xlned.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: Mon, 02 Aug 2021 11:54:12 -0500
Subject: Re: Definition of primitive recursive function (wiki) [ H(P,P)==0 is always correct ]
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng,sci.math.symbolic
References: <dc26feeb-de3d-4114-ba3f-77f7d58ced8fn@googlegroups.com>
From: NoO...@NoWhere.com (olcott)
Date: Mon, 2 Aug 2021 11:54:11 -0500
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.12.0
MIME-Version: 1.0
In-Reply-To: <dc26feeb-de3d-4114-ba3f-77f7d58ced8fn@googlegroups.com>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 7bit
Message-ID: <9uOdnegjBMOpvpX8nZ2dnUU7-b3NnZ2d@giganews.com>
Lines: 191
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-yjE6nWnRzMLluxY/4tzM+RmPV/YbQcAGgaNHHMchxVDqFgoVTbCJWo9Rvbtu7huzsQ5S+eeO8y9/K8I!JNugNCexh6tmpNLJQ6qEDrXYLGWp3PLRXN3TYgG0Q+fg9xLLka5RdgUqorFMHXoKtZLpGUrAWg==
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: 9282
X-Received-Bytes: 9492
View all headers
On 8/2/2021 9:01 AM, Charlie-Boo wrote:
wiki: "a primitive recursive function is a function that can be computed by a computer program [for which] an upper bound [on] the number of iterations of every loop can be determined before entering the loop."

About both the wording and the technical soundness of its intent:

1. You can perform calculations equivalent to "entering the loop" so that's inconsequential.

2. You can always simulate that loop to see the actual number of iterations.  Is that ok even though it doesn't terminate if applied to a program that doesn't meet this criteria?

3. Since it calculates a total function it halts and you can prove everything about it because you can simulate its complete execution.

4. Is this actually equivalent to "provably halts" but then that is equivalent to "halts" since halt <=> provably halts?

C-B


Provably halting is simply a pure simulation that reaches a final state. Proving never halting is proving that the final state can never be reached. Below is proof that P(P) halts and the input to H(P,P) never halts.

There may be a very high tendency to reject this latter claim out-of-hand without sufficient review through the human fallibility of bias. If no error exists in steps (a)(b)(c) then we know that H(P,P)==0 is the correct halt status of the input to the input to H(P,P).

If P(P) halts and H(P,P)==0 is the correct halt status of the input to the input to H(P,P) then we have a paradox rather than a contradiction.

Because H only acts as a pure simulator of its input until after its halt status decision has been made it has no behavior that can possibly effect the behavior of its input. Because of this H screens out its own address range in every execution trace that it examines. This is why we never see any instructions of H in any execution trace after an input calls H.

Once we fully understand all of the above we can see from the execution trace of H(P,P):

(1) The execution trace is correct because it corresponds to the x86 source-code of P.

(2) The execution trace of the simulation of P(P) cannot possibly ever reach its final state whether or not this simulation is aborted.

int Simulate(u32 P, u32 I)
{
   ((int(*)(int))P)(I);
   return 1;
}

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

void P()
{
   if(PSR_Decider((u32)P, (u32)P)==0)
     if(H1((u32)P, (u32)P))
       HERE: goto HERE;
}

int main()
{
   Output("Input_Halts = ", Simulate((u32)P, (u32)P));
}

(a) Whether or not H aborts its simulation of this input the input to H(P,P) cannot possibly ever reach its final state (proved by the x86 execution trace shown below).

(b) Because input to H(P,P) cannot possibly ever reach its final state
we know that it never halts.

(c) Because it never halts we know that H(P,P) correctly returns 0 indicating that its input never halts.

(d) P reaches its final state.

_Simulate()
[00000ce2](01)  55          push ebp
[00000ce3](02)  8bec        mov ebp,esp
[00000ce5](03)  8b450c      mov eax,[ebp+0c]
[00000ce8](01)  50          push eax
[00000ce9](03)  ff5508      call dword [ebp+08]
[00000cec](03)  83c404      add esp,+04
[00000cef](05)  b801000000  mov eax,00000001
[00000cf4](01)  5d          pop ebp
[00000cf5](01)  c3          ret
Size in bytes:(0020) [00000cf5]

_P()
[00000d02](01)  55          push ebp
[00000d03](02)  8bec        mov ebp,esp
[00000d05](03)  8b4508      mov eax,[ebp+08]
[00000d08](01)  50          push eax
[00000d09](03)  8b4d08      mov ecx,[ebp+08]
[00000d0c](01)  51          push ecx
[00000d0d](05)  e870feffff  call 00000b82
[00000d12](03)  83c408      add esp,+08
[00000d15](02)  85c0        test eax,eax
[00000d17](02)  7402        jz 00000d1b
[00000d19](02)  ebfe        jmp 00000d19
[00000d1b](01)  5d          pop ebp
[00000d1c](01)  c3          ret
Size in bytes:(0027) [00000d1c]

_main()
[00000d22](01)  55          push ebp
[00000d23](02)  8bec        mov ebp,esp
[00000d25](05)  68020d0000  push 00000d02
[00000d2a](05)  68020d0000  push 00000d02
[00000d2f](05)  e8aeffffff  call 00000ce2
[00000d34](03)  83c408      add esp,+08
[00000d37](01)  50          push eax
[00000d38](05)  6823030000  push 00000323
[00000d3d](05)  e810f6ffff  call 00000352
[00000d42](03)  83c408      add esp,+08
[00000d45](02)  33c0        xor eax,eax
[00000d47](01)  5d          pop ebp
[00000d48](01)  c3          ret
Size in bytes:(0039) [00000d48]

  machine   stack     stack     machine    assembly
  address   address   data      code       language
  ========  ========  ========  =========  =============
....[00000d22][00101851][00000000] 55          push ebp
....[00000d23][00101851][00000000] 8bec        mov ebp,esp
....[00000d25][0010184d][00000d02] 68020d0000  push 00000d02
....[00000d2a][00101849][00000d02] 68020d0000  push 00000d02
....[00000d2f][00101845][00000d34] e8aeffffff  call 00000ce2
....[00000ce2][00101841][00101851] 55          push ebp
....[00000ce3][00101841][00101851] 8bec        mov ebp,esp
....[00000ce5][00101841][00101851] 8b450c      mov eax,[ebp+0c]
....[00000ce8][0010183d][00000d02] 50          push eax
Calling:_P()
....[00000ce9][00101839][00000cec] ff5508      call dword [ebp+08]
....[00000d02][00101835][00101841] 55          push ebp
....[00000d03][00101835][00101841] 8bec        mov ebp,esp
....[00000d05][00101835][00101841] 8b4508      mov eax,[ebp+08]
....[00000d08][00101831][00000d02] 50          push eax
....[00000d09][00101831][00000d02] 8b4d08      mov ecx,[ebp+08]
....[00000d0c][0010182d][00000d02] 51          push ecx
....[00000d0d][00101829][00000d12] e870feffff  call 00000b82

Begin Local Halt Decider Simulation at Machine Address:d02
....[00000d02][002118f1][002118f5] 55          push ebp
....[00000d03][002118f1][002118f5] 8bec        mov ebp,esp
....[00000d05][002118f1][002118f5] 8b4508      mov eax,[ebp+08]
....[00000d08][002118ed][00000d02] 50          push eax
....[00000d09][002118ed][00000d02] 8b4d08      mov ecx,[ebp+08]
....[00000d0c][002118e9][00000d02] 51          push ecx
....[00000d0d][002118e5][00000d12] e870feffff  call 00000b82
....[00000d02][0025c319][0025c31d] 55          push ebp
....[00000d03][0025c319][0025c31d] 8bec        mov ebp,esp
....[00000d05][0025c319][0025c31d] 8b4508      mov eax,[ebp+08]
....[00000d08][0025c315][00000d02] 50          push eax
....[00000d09][0025c315][00000d02] 8b4d08      mov ecx,[ebp+08]
....[00000d0c][0025c311][00000d02] 51          push ecx
....[00000d0d][0025c30d][00000d12] e870feffff  call 00000b82
Local Halt Decider: Infinite Recursion Detected Simulation Stopped

....[00000d12][00101835][00101841] 83c408      add esp,+08
....[00000d15][00101835][00101841] 85c0        test eax,eax
....[00000d17][00101835][00101841] 7402        jz 00000d1b
....[00000d1b][00101839][00000cec] 5d          pop ebp
....[00000d1c][0010183d][00000d02] c3          ret
....[00000cec][00101841][00101851] 83c404      add esp,+04
....[00000cef][00101841][00101851] b801000000  mov eax,00000001
....[00000cf4][00101845][00000d34] 5d          pop ebp
....[00000cf5][00101849][00000d02] c3          ret
....[00000d34][00101851][00000000] 83c408      add esp,+08
....[00000d37][0010184d][00000001] 50          push eax
....[00000d38][00101849][00000323] 6823030000  push 00000323
---[00000d3d][00101849][00000323] e810f6ffff  call 00000352
Input_Halts = 1
....[00000d42][00101851][00000000] 83c408      add esp,+08
....[00000d45][00101851][00000000] 33c0        xor eax,eax
....[00000d47][00101855][00100000] 5d          pop ebp
....[00000d48][00101859][000000bc] c3          ret
Number_of_User_Instructions(48)

Click here to read the complete article
1
rocksolid light 0.7.2
clearneti2ptor