-4
$\begingroup$

Does H correctly decide that P never halts?
(The C/x86 source-code for P is provided below)

Halting problem undecidability and infinitely nested simulation
The x86utm operating system was created so that the halting problem could be examined concretely in the high level language of C. H is a function written in C that analyzes the x86 machine language of other functions written in C. H recognizes simple cases of infinite recursion and infinite loops. The conventional halting problem proof counter-example template is shown to simply be an input that does not halt.

H simulates its input with an x86 emulator until it determines that its input would never halt. As soon as H recognizes that its input would never halt it stops simulating this input and returns 0. For inputs that do halt H acts exactly as if it was an x86 emulator and simply runs its input to completion and then returns 1.

Halting computation: is any computation that eventually reaches its own final state.

Pathological Input to a halt decider is stipulated to mean any input that was defined to do the opposite of whatever its corresponding halt decider decides as Sipser describes:

Now we construct a new Turing machine D with H as a subroutine. This new TM calls H to determine what M does when the input to M is its own description ⟨M⟩. Once D has determined this information, it does the opposite. (Sipser:1997:165)

This question can only be correctly answered after the pathology has been removed. When a halt decider only acts as a pure simulator of its input until after its halt status decision is made there is no feedback loop of back channel communication between the halt decider and its input that can prevent a correct halt status decision.

The standard pseudo-code halting problem template "proved" that the halting problem could never be solved on the basis that neither value of true (halting) nor false (not halting) could be correctly returned form the halt decider to the confounding input.

procedure compute_g(i):  // (Wikipedia:Halting Problem) 
  if f(i, i) == 0 then   // adapted from (Strachey, C 1965) 
    return 0             // originally written in CPL 
  else                   // ancestor of the BCPL, B and C
    loop forever         // programming languages

This problem is overcome on the basis that a simulating halt decider would abort the simulation of its input before ever returning any value to this input. It aborts the simulation of its input on the basis that its input specifies what is essentially infinite recursion (infinitely nested simulation) to any simulating halt decider.

H analyzes the (currently updated) stored execution trace of its x86 emulation of P(P) after it simulates each instruction of input (P, P). As soon as a non-halting behavior pattern is matched H aborts the simulation of its input and decides that its input does not halt.

The verifiably correct x86 execution trace of the simulation of the input to H(P,P) proves that this input cannot possibly reach its final state while H acts as a pure x86 emulator of this input. This unequivocally proves that H does correctly decide that its input never halts.

// Simplified Linz Ĥ (Linz:1990:319)
// Strachey(1965) CPL translated to C
void P(u32 x) 
{
  if (H(x, x)) 
    HERE: goto HERE; 
} 

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

_P()
[00000c36](01)  55          push ebp
[00000c37](02)  8bec        mov ebp,esp
[00000c39](03)  8b4508      mov eax,[ebp+08] // 2nd Param
[00000c3c](01)  50          push eax
[00000c3d](03)  8b4d08      mov ecx,[ebp+08] // 1st Param
[00000c40](01)  51          push ecx
[00000c41](05)  e820fdffff  call 00000966    // call H
[00000c46](03)  83c408      add esp,+08
[00000c49](02)  85c0        test eax,eax
[00000c4b](02)  7402        jz 00000c4f
[00000c4d](02)  ebfe        jmp 00000c4d
[00000c4f](01)  5d          pop ebp
[00000c50](01)  c3          ret
Size in bytes:(0027) [00000c50]

_main()
[00000c56](01)  55          push ebp
[00000c57](02)  8bec        mov ebp,esp
[00000c59](05)  68360c0000  push 00000c36
[00000c5e](05)  68360c0000  push 00000c36
[00000c63](05)  e8fefcffff  call 00000966
[00000c68](03)  83c408      add esp,+08
[00000c6b](01)  50          push eax
[00000c6c](05)  6857030000  push 00000357
[00000c71](05)  e810f7ffff  call 00000386
[00000c76](03)  83c408      add esp,+08
[00000c79](02)  33c0        xor eax,eax
[00000c7b](01)  5d          pop ebp
[00000c7c](01)  c3          ret
Size in bytes:(0039) [00000c7c]

 machine   stack     stack     machine    assembly 
 address   address   data      code       language
 ========  ========  ========  =========  =============
Begin Local Halt Decider Simulation at Machine Address:c36
[00000c36][002117ca][002117ce] 55          push ebp
[00000c37][002117ca][002117ce] 8bec        mov ebp,esp
[00000c39][002117ca][002117ce] 8b4508      mov eax,[ebp+08]
[00000c3c][002117c6][00000c36] 50          push eax       // push P
[00000c3d][002117c6][00000c36] 8b4d08      mov ecx,[ebp+08]
[00000c40][002117c2][00000c36] 51          push ecx       // push P
[00000c41][002117be][00000c46] e820fdffff  call 00000966  // call H(P,P)

[00000c36][0025c1f2][0025c1f6] 55          push ebp
[00000c37][0025c1f2][0025c1f6] 8bec        mov ebp,esp
[00000c39][0025c1f2][0025c1f6] 8b4508      mov eax,[ebp+08]
[00000c3c][0025c1ee][00000c36] 50          push eax       // push P
[00000c3d][0025c1ee][00000c36] 8b4d08      mov ecx,[ebp+08]
[00000c40][0025c1ea][00000c36] 51          push ecx       // push P
[00000c41][0025c1e6][00000c46] e820fdffff  call 00000966  // call H(P,P)
Local Halt Decider: Infinite Recursion Detected Simulation Stopped 

In the above 14 instructions of the simulation of P(P) we can see that the first 7 instructions of P are repeated. The end of this sequence of 7 instructions P calls H with its own machine address as the parameters to H(P,P). Because H only examines the behavior of its inputs and ignores its own behavior when H(P,P) is called we only see the first instruction of P being simulated.

Anyone knowing the x86 language well enough can see that none of these 7 simulated instructions of P have any escape from their infinitely repeating behavior pattern. When H recognizes this infinitely repeating pattern it aborts its simulation of P(P) and reports that its input: (P,P) never reaches its final state of 0xc50.

[00000c68][0010172a][00000000] 83c408      add esp,+08
[00000c6b][00101726][00000000] 50          push eax
[00000c6c][00101722][00000357] 6857030000  push 00000357
[00000c71][00101722][00000357] e810f7ffff  call 00000386
Input_Halts = 0
[00000c76][0010172a][00000000] 83c408      add esp,+08
[00000c79][0010172a][00000000] 33c0        xor eax,eax
[00000c7b][0010172e][00100000] 5d          pop ebp
[00000c7c][00101732][00000068] c3          ret
Number_of_User_Instructions(27)
Number of Instructions Executed(23721)

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)

Sipser, Michael 1997. Introduction to the Theory of Computation. Boston: PWS Publishing Company (165-167)

Much more details are provided in the paper:
Halting problem undecidability and infinitely nested simulation

$\endgroup$
15
  • 1
    $\begingroup$ What are you actually trying to prove? What is H? Have you written a function H? Do you want to show it's possible to write it, or that it is impossible? $\endgroup$ – gnasher729 Jun 25 at 17:44
  • $\begingroup$ @gnasher729 H is a partial halt decider written in C and executed in the x86utm operating system. It seems that H correctly decides that its input P never halts on its input P. This is the result of 2.5 years worth of work since 2018 and many thousands of reviews. $\endgroup$ – polcott Jun 25 at 18:42
  • 1
    $\begingroup$ A halt decider that only works for one particular function is pretty useless. So does it work for all functions, or some particular functions, or what? $\endgroup$ – gnasher729 Jun 25 at 22:47
  • $\begingroup$ @gnasher729 It only works for the one "impossible" input that "proved" halting problem undecidability. This took me 2.5 years since 2018. After thousands of reviews in the last six months no one has pointed out a single error. $\endgroup$ – polcott Jun 26 at 0:06
  • 1
    $\begingroup$ I'm having trouble understanding "simulating halt deciders." Suppose we have an SHD H, a function F and an input x, and F(x) never halts and never produces the "simple cases of infinite recursion and infinite loops" that H can recognize. Does H((u32)F, x) return a value at some point, or does it keep simulating F(x) indefinitely? $\endgroup$ – Ilkka Törmä Jul 7 at 7:23
-4
$\begingroup$
_P()
[00000b1a](01)  55              push ebp
[00000b1b](02)  8bec            mov ebp,esp
[00000b1d](01)  51              push ecx
[00000b1e](03)  8b4508          mov eax,[ebp+08]
[00000b21](01)  50              push eax       // 2nd Param
[00000b22](03)  8b4d08          mov ecx,[ebp+08]
[00000b25](01)  51              push ecx       // 1st Param
[00000b26](05)  e81ffeffff      call 0000094a  // call H
[00000b2b](03)  83c408          add esp,+08
[00000b2e](03)  8945fc          mov [ebp-04],eax
[00000b31](04)  837dfc00        cmp dword [ebp-04],+00
[00000b35](02)  7402            jz 00000b39
[00000b37](02)  ebfe            jmp 00000b37
[00000b39](02)  8be5            mov esp,ebp
[00000b3b](01)  5d              pop ebp
[00000b3c](01)  c3              ret
Size in bytes:(0035) [00000b3c]

_main()
[00000bda](01)  55              push ebp
[00000bdb](02)  8bec            mov ebp,esp
[00000bdd](01)  51              push ecx
[00000bde](05)  681a0b0000      push 00000b1a  // push address of P
[00000be3](05)  681a0b0000      push 00000b1a  // push address of P
[00000be8](05)  e85dfdffff      call 0000094a  // call H
[00000bed](03)  83c408          add esp,+08
[00000bf0](03)  8945fc          mov [ebp-04],eax
[00000bf3](03)  8b45fc          mov eax,[ebp-04]
[00000bf6](01)  50              push eax
[00000bf7](05)  683b030000      push 0000033b
[00000bfc](05)  e869f7ffff      call 0000036a
[00000c01](03)  83c408          add esp,+08
[00000c04](02)  33c0            xor eax,eax
[00000c06](02)  8be5            mov esp,ebp
[00000c08](01)  5d              pop ebp
[00000c09](01)  c3              ret
Size in bytes:(0048) [00000c09]

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  
===============================
[00000bda][00101647][00000000] 55         push ebp
[00000bdb][00101647][00000000] 8bec       mov ebp,esp
[00000bdd][00101643][00000000] 51         push ecx
[00000bde][0010163f][00000b1a] 681a0b0000 push 00000b1a // push P
[00000be3][0010163b][00000b1a] 681a0b0000 push 00000b1a // push P
[00000be8][00101637][00000bed] e85dfdffff call 0000094a // call H

Begin Local Halt Decider Simulation at Machine Address:b1a
[00000b1a][002116e7][002116eb] 55         push ebp
[00000b1b][002116e7][002116eb] 8bec       mov ebp,esp
[00000b1d][002116e3][002016b7] 51         push ecx
[00000b1e][002116e3][002016b7] 8b4508     mov eax,[ebp+08]
[00000b21][002116df][00000b1a] 50         push eax      // push P
[00000b22][002116df][00000b1a] 8b4d08     mov ecx,[ebp+08]
[00000b25][002116db][00000b1a] 51         push ecx      // push P
[00000b26][002116d7][00000b2b] e81ffeffff call 0000094a // call H
[00000b1a][0025c10f][0025c113] 55         push ebp
[00000b1b][0025c10f][0025c113] 8bec       mov ebp,esp
[00000b1d][0025c10b][0024c0df] 51         push ecx      
[00000b1e][0025c10b][0024c0df] 8b4508     mov eax,[ebp+08]
[00000b21][0025c107][00000b1a] 50         push eax      // push P
[00000b22][0025c107][00000b1a] 8b4d08     mov ecx,[ebp+08]
[00000b25][0025c103][00000b1a] 51         push ecx      // push P
[00000b26][0025c0ff][00000b2b] e81ffeffff call 0000094a // call H
Local Halt Decider: Infinite Recursion Detected Simulation Stopped 

In the above 16 instructions of the simulation of P(P) we can see that the first 8 instructions of P are repeated. The end of this sequence of 8 instructions P calls H with its own machine address as the parameters to H: H(P,P). Because H only examines the behavior of its inputs and ignores its own behavior when H(P,P) is called we only see the first instruction of P being simulated.

Anyone knowing the x86 language well enough can see that none of these 8 simulated instructions of P have any escape from their infinitely repeating behavior pattern. When H recognizes this infinitely repeating pattern it aborts its simulation of P(P) and reports that its input: (P,P) would never halt on its input.

[00000bed][00101643][00000000] 83c408     add esp,+08
[00000bf0][00101643][00000000] 8945fc     mov [ebp-04],eax
[00000bf3][00101643][00000000] 8b45fc     mov eax,[ebp-04]
[00000bf6][0010163f][00000000] 50         push eax
[00000bf7][0010163b][0000033b] 683b030000 push 0000033b
[00000bfc][0010163b][0000033b] e869f7ffff call 0000036a
Input_Halts = 0
[00000c01][00101643][00000000] 83c408     add esp,+08
[00000c04][00101643][00000000] 33c0       xor eax,eax
[00000c06][00101647][00000000] 8be5       mov esp,ebp
[00000c08][0010164b][00100000] 5d         pop ebp
[00000c09][0010164f][00000080] c3         ret
Number_of_User_Instructions(33)

This is the sound deductive inference (proof) that H(P,P)==0 is correct.

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 above).

When the simulator determines whether or not it must abort the simulation of its input based on the behavior of its input the simulator only acts as an x86 emulator thus has no effect on the behavior of its input. This allows the simulator to always ignore its own behavior.

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

$\endgroup$
2

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.