Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

Re: Solution To The Halting Problem [ H based on UTM ]( correct answer )

19 views
Skip to first unread message

olcott

unread,
May 6, 2021, 12:03:05 PM5/6/21
to
On 5/6/2021 10:52 AM, André G. Isaak wrote:
> On 2021-05-05 22:03, olcott wrote:
>> On 5/5/2021 10:45 PM, André G. Isaak wrote:
>
> <snippage>
>
>>> The problem here is that your Halts(H_Hat, H_Hat) doesn't meet the
>>> above specification, at least not if we take your claims about how
>>> this works seriously.
>>>
>>
>> Whether or not the current code meets the above specification (I
>> believe that it does) the above specification does provide the
>> criterion measure to determine infinitely nested simulation, stop this
>> simulation on this basis and report non-halting.
>>
>>> You have Halts() simulating H_Hat, which in turn calls Halts(), but
>>> that latter halts isn't going to be at the same machine address
>>
>> As a matter of objective fact it <is> at the same address and that it
>> is at the same address is the way that the same code can serve
>> multiple clients. In the bad old days of the internet code was
>> duplicated to serve multiple clients.
>
> Then you're using the term 'simulation' in a very unorthodox manner...
>
> But let's put that aside for the moment. You justify the fact that H_Hat
> calls the *same* version of Halts() as the outermost halt on the grounds
> that you are doing this 'The Sipser Way'.
>
> Let's imagine, just for sake of argument, that your interpretation of
> Sipser is actually correct, and that Sipser *doesn't* embed a copy of
> Halts within his D.
>
> That would mean that the Sipser proof and the Linz proof are
> fundamentally different proofs (they're not, but I did say 'imagine'),
> and Linz's H_Hat and Sipser's D are constructed in entirely different
> manners.
>

Page 4 indicates exactly how all three proofs are related by a key element.
http://www.liarparadox.org/Halting_problem_undecidability_and_infinite_recursion.pdf

> But from the outset you claimed your goal was to 'disprove' the
> 'conventional halting proofs'. Now I have no idea how you decide which
> proofs are conventional and which are not, or why only the
> 'conventional' proofs matter, but if you had actually found some fatal
> flaw in Sipser's proof, that wouldn't magically make the Linz proof go
> away.
>
> You still need to show how your 'decider' manages to correctly decide
> Linz's H_Hat, where a *copy* of H is embedded in H_Hat. If you can't do
> that, Linz's proof still stands, and your 'recursion pattern' which is
> based on comparing addresses is *not* going to work for Linz's H_Hat.
>
> That you *think* you've found a way of defeating Sipser's D has no
> bearing on the halting problem when there are other proofs which your
> approach can't deal with. And you can't deal with Linz.
>

Linz H decides not halting on Linz Ĥ on the basis of infinitely nested
simulation:

http://www.liarparadox.org/Peter_Linz_HP(Pages_315-320).pdf

For every at least partial halt decider H that bases its halting
decision on simulating its input unless H decides infinitely nested
simulation (not halting), stops simulating Ĥ(Ĥ), and decides not halting
the alternative is that H never returns and Ĥ remains in infinitely
nested simulation.

This proves that my concept is sound even on the original Linz proof.
The correct answer is infinitely nested simulation (not halting), only
the path to arrive at this correct answer varies.

>>> as the outer halts since it is part of the simulation. Similarly,
>>> subsequent calls to halts will be to simulations of simulations of
>>> Halts(), and so forth.
>>>
>>> You can't meaningfully compare machine addresses from an actual call
>>> and a simulation of that call, or a simulation [...] of a simulation
>>> of that call.
>>>
>>> Moreover, there *are* conditional branches between calls to each
>>> successive level of simulation since your 'decider' needs to
>>> determine whether to abort a given simulation. That's going to
>>> involve a conditional.
>>>
>>> André
>>>
>>
>> There are conditional branches in the halt decider when the halt
>> decider decides that the above infinite loop would never halt,
>> none-the-less its decision is correct. The key basis is whether or not
>> the infinite
>
> But then you're not following the pattern which you claim to be
> following since you are ignoring some conditional branches. How do you
> decide which conditional branches are ignorable and which are not?
>
> André
>


--
Copyright 2021 Pete Olcott

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

olcott

unread,
May 7, 2021, 1:44:24 PM5/7/21
to
On 5/6/2021 6:53 PM, Kaz Kylheku wrote:
> On 2021-05-06, olcott <No...@NoWhere.com> wrote:
>> On 5/6/2021 4:31 PM, Kaz Kylheku wrote:
>>> On 2021-05-06, olcott <No...@NoWhere.com> wrote:
>>>> I don't have nothing. I have the correct return value for H(Ĥ, Ĥ).
>>>> I also have a method for deciding a computationally equivalent instance.
>>>
>>> Can you prove that your Halts always returns the same answer for
>>> the same parameters, as required?
>> It is your mistake that this is required.
>>
>> When-so-ever Halts() is called in the equivalent of infinite recursion
>> it can't possibly return anything until after it terminates this
>> infinite simulation nesting.
>
> Sorry, yes, right; I forgot something important in the pseudo code! My
> apologies.
>
> Please use this one. (It is the same as the previous, except for
> differences in the main function):
>
> Please integrate this, and provide execution trace. Thx!
>
> #define NRES 4
>
> // Cached results from calling Halts
>
> struct HaltResult {
> U32 P, I, H;
> } res[4];
>
> // Wrapper for calling Halts.
>
> U32 HaltsProxy(U32 P, U32 I)
> {
> int i;
> U32 H = Halts(P, I); // call real Halts
>
> for (i = 0; i < NRES; i++) {
> struct HaltResult *r = &res[i];
>
> if (r->P == 0 && r->I == 0 && r->H == 0) {
> // Blank spot in array: enter result here
> r->P = P;
> r->I = I;
> r->H = H;
> break;
> } else if (r->P == P && r->I == I) {
> // Repeat call for same P, I.
>
> if (r->H != H) {
> // Halts has returned a different value
> Output("Halt decider is not an algorithm!");
> loop0: goto loop0;
> }
>
> // Same value; we are done checking.
> break;
> }
>
> if (i >= NRES) {
> // Array has filled up, what? We only call this twice.
> Output("Unexpected excess calls to HaltsProxy!");
> loop1: goto loop1;
> }
> }
>
> return H;
> }
>
> void H_Hat(u32 P)
> {
> if (HaltsProxy(P, P)) {
> loop: goto loop;
> }
> }
>
> int main(void)
> {
> U32 H = HaltsProxy((u32) H_hat, (u32) H_Hat);
> Output("Input halts = ", H);
> H_Hat((u32) H_Hat);
> Output("Halt returned");
> return 0;
> }
>

Below is the corrrected source code, assembly language and complete
exuection trace.


#define NRES 4

struct HaltResult
{
u32 P, I, H;
};

struct HaltResult res[4] = {{1,1,1},{2,2,2},{3,3,3},{4,4,4}};


void H_Hat(u32 P)
{
if (HaltsProxy(P, P))
loop: goto loop;
}

void Init_res()
{
u32 P = (u32)H_Hat, I = (u32)H_Hat;
u32 H = Halts(P, I);
for (u32 N = 0; N < NRES; N++)
{
res[N].P = P;
res[N].I = I;
res[N].H = H;
}
}


u32 HaltsProxy(u32 P, u32 I)
{
int i;
u32 H = Halts(P, I); // call real Halts
for (i = 0; i < NRES; i++)
{
struct HaltResult *r = &res[i];

if (r->P == P && r->I == I)
{
// Repeat call for same P, I.
H = Halts(P, I); // call real Halts
if (r->H != H)
{
// Halts has returned a different value
OutputString("Halt decider is not an algorithm!");
loop0: goto loop0;
}
// Same value; we are done checking.
break;
}
if (i >= NRES)
{
// Array has filled up, what? We only call this twice.
OutputString("Unexpected excess calls to HaltsProxy!");
loop1: goto loop1;
}
}
return H;
}



int main()
{
Init_res();
u32 H = HaltsProxy((u32) H_Hat, (u32) H_Hat);
Output("Input halts = ", H);
H_Hat((u32) H_Hat);
OutputString("Halt returned");
return 0;
}


_H_Hat()
[00000bf5](01) 55 push ebp
[00000bf6](02) 8bec mov ebp,esp
[00000bf8](03) 8b4508 mov eax,[ebp+08]
[00000bfb](01) 50 push eax
[00000bfc](03) 8b4d08 mov ecx,[ebp+08]
[00000bff](01) 51 push ecx
[00000c00](05) e810000000 call 00000c15
[00000c05](03) 83c408 add esp,+08
[00000c08](02) 85c0 test eax,eax
[00000c0a](02) 7402 jz 00000c0e
[00000c0c](02) ebfe jmp 00000c0c
[00000c0e](01) 5d pop ebp
[00000c0f](01) c3 ret
Size in bytes:(0027) [00000c0f]

_HaltsProxy()
[00000c15](01) 55 push ebp
[00000c16](02) 8bec mov ebp,esp
[00000c18](03) 83ec0c sub esp,+0c
[00000c1b](03) 8b450c mov eax,[ebp+0c]
[00000c1e](01) 50 push eax
[00000c1f](03) 8b4d08 mov ecx,[ebp+08]
[00000c22](01) 51 push ecx
[00000c23](05) e8ddfdffff call 00000a05
[00000c28](03) 83c408 add esp,+08
[00000c2b](03) 8945f4 mov [ebp-0c],eax
[00000c2e](07) c745fc00000000 mov [ebp-04],00000000
[00000c35](02) eb09 jmp 00000c40
[00000c37](03) 8b55fc mov edx,[ebp-04]
[00000c3a](03) 83c201 add edx,+01
[00000c3d](03) 8955fc mov [ebp-04],edx
[00000c40](04) 837dfc04 cmp dword [ebp-04],+04
[00000c44](02) 7d67 jnl 00000cad
[00000c46](04) 6b45fc0c imul eax,[ebp-04],+0c
[00000c4a](05) 052f020000 add eax,0000022f
[00000c4f](03) 8945f8 mov [ebp-08],eax
[00000c52](03) 8b4df8 mov ecx,[ebp-08]
[00000c55](02) 8b11 mov edx,[ecx]
[00000c57](03) 3b5508 cmp edx,[ebp+08]
[00000c5a](02) 753a jnz 00000c96
[00000c5c](03) 8b45f8 mov eax,[ebp-08]
[00000c5f](03) 8b4804 mov ecx,[eax+04]
[00000c62](03) 3b4d0c cmp ecx,[ebp+0c]
[00000c65](02) 752f jnz 00000c96
[00000c67](03) 8b550c mov edx,[ebp+0c]
[00000c6a](01) 52 push edx
[00000c6b](03) 8b4508 mov eax,[ebp+08]
[00000c6e](01) 50 push eax
[00000c6f](05) e891fdffff call 00000a05
[00000c74](03) 83c408 add esp,+08
[00000c77](03) 8945f4 mov [ebp-0c],eax
[00000c7a](03) 8b4df8 mov ecx,[ebp-08]
[00000c7d](03) 8b5108 mov edx,[ecx+08]
[00000c80](03) 3b55f4 cmp edx,[ebp-0c]
[00000c83](02) 740f jz 00000c94
[00000c85](05) 687b030000 push 0000037b
[00000c8a](05) e866f7ffff call 000003f5
[00000c8f](03) 83c404 add esp,+04
[00000c92](02) ebfe jmp 00000c92
[00000c94](02) eb17 jmp 00000cad
[00000c96](04) 837dfc04 cmp dword [ebp-04],+04
[00000c9a](02) 7c0f jl 00000cab
[00000c9c](05) 689f030000 push 0000039f
[00000ca1](05) e84ff7ffff call 000003f5
[00000ca6](03) 83c404 add esp,+04
[00000ca9](02) ebfe jmp 00000ca9
[00000cab](02) eb8a jmp 00000c37
[00000cad](03) 8b45f4 mov eax,[ebp-0c]
[00000cb0](02) 8be5 mov esp,ebp
[00000cb2](01) 5d pop ebp
[00000cb3](01) c3 ret
Size in bytes:(0159) [00000cb3]

_Init_res()
[00000cb5](01) 55 push ebp
[00000cb6](02) 8bec mov ebp,esp
[00000cb8](03) 83ec10 sub esp,+10
[00000cbb](07) c745f8f50b0000 mov [ebp-08],00000bf5
[00000cc2](07) c745f4f50b0000 mov [ebp-0c],00000bf5
[00000cc9](03) 8b45f4 mov eax,[ebp-0c]
[00000ccc](01) 50 push eax
[00000ccd](03) 8b4df8 mov ecx,[ebp-08]
[00000cd0](01) 51 push ecx
[00000cd1](05) e82ffdffff call 00000a05
[00000cd6](03) 83c408 add esp,+08
[00000cd9](03) 8945f0 mov [ebp-10],eax
[00000cdc](07) c745fc00000000 mov [ebp-04],00000000
[00000ce3](02) eb09 jmp 00000cee
[00000ce5](03) 8b55fc mov edx,[ebp-04]
[00000ce8](03) 83c201 add edx,+01
[00000ceb](03) 8955fc mov [ebp-04],edx
[00000cee](04) 837dfc04 cmp dword [ebp-04],+04
[00000cf2](02) 7329 jnb 00000d1d
[00000cf4](04) 6b45fc0c imul eax,[ebp-04],+0c
[00000cf8](03) 8b4df8 mov ecx,[ebp-08]
[00000cfb](06) 89882f020000 mov [eax+0000022f],ecx
[00000d01](04) 6b55fc0c imul edx,[ebp-04],+0c
[00000d05](03) 8b45f4 mov eax,[ebp-0c]
[00000d08](06) 89822f020000 mov [edx+0000022f],eax
[00000d0e](04) 6b4dfc0c imul ecx,[ebp-04],+0c
[00000d12](03) 8b55f0 mov edx,[ebp-10]
[00000d15](06) 89912f020000 mov [ecx+0000022f],edx
[00000d1b](02) ebc8 jmp 00000ce5
[00000d1d](02) 8be5 mov esp,ebp
[00000d1f](01) 5d pop ebp
[00000d20](01) c3 ret
Size in bytes:(0108) [00000d20]

_main()
[00000d25](01) 55 push ebp
[00000d26](02) 8bec mov ebp,esp
[00000d28](01) 51 push ecx
[00000d29](05) e887ffffff call 00000cb5
[00000d2e](05) 68f50b0000 push 00000bf5
[00000d33](05) 68f50b0000 push 00000bf5
[00000d38](05) e8d8feffff call 00000c15
[00000d3d](03) 83c408 add esp,+08
[00000d40](03) 8945fc mov [ebp-04],eax
[00000d43](03) 8b45fc mov eax,[ebp-04]
[00000d46](01) 50 push eax
[00000d47](05) 68c7030000 push 000003c7
[00000d4c](05) e8b4f6ffff call 00000405
[00000d51](03) 83c408 add esp,+08
[00000d54](05) 68f50b0000 push 00000bf5
[00000d59](05) e897feffff call 00000bf5
[00000d5e](03) 83c404 add esp,+04
[00000d61](05) 68d7030000 push 000003d7
[00000d66](05) e88af6ffff call 000003f5
[00000d6b](03) 83c404 add esp,+04
[00000d6e](02) 33c0 xor eax,eax
[00000d70](02) 8be5 mov esp,ebp
[00000d72](01) 5d pop ebp
[00000d73](01) c3 ret
Size in bytes:(0079) [00000d73]

===============================
...[00000d25][001018e9][00000000](01) 55 push ebp
...[00000d26][001018e9][00000000](02) 8bec mov ebp,esp
...[00000d28][001018e5][00000000](01) 51 push ecx
...[00000d29][001018e1][00000d2e](05) e887ffffff call 00000cb5
...[00000cb5][001018dd][001018e9](01) 55 push ebp
...[00000cb6][001018dd][001018e9](02) 8bec mov ebp,esp
...[00000cb8][001018cd][90909090](03) 83ec10 sub esp,+10
...[00000cbb][001018cd][90909090](07) c745f8f50b0000 mov
[ebp-08],00000bf5
...[00000cc2][001018cd][90909090](07) c745f4f50b0000 mov
[ebp-0c],00000bf5
...[00000cc9][001018cd][90909090](03) 8b45f4 mov
eax,[ebp-0c]
...[00000ccc][001018c9][00000bf5](01) 50 push eax
...[00000ccd][001018c9][00000bf5](03) 8b4df8 mov
ecx,[ebp-08]
...[00000cd0][001018c5][00000bf5](01) 51 push ecx
...[00000cd1][001018c1][00000cd6](05) e82ffdffff call 00000a05
Begin Local Halt Decider Simulation at Machine Address:bf5
...[00000bf5][00211989][0021198d](01) 55 push ebp
...[00000bf6][00211989][0021198d](02) 8bec mov ebp,esp
...[00000bf8][00211989][0021198d](03) 8b4508 mov
eax,[ebp+08]
...[00000bfb][00211985][00000bf5](01) 50 push eax
...[00000bfc][00211985][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000bff][00211981][00000bf5](01) 51 push ecx
...[00000c00][0021197d][00000c05](05) e810000000 call 00000c15
...[00000c15][00211979][00211989](01) 55 push ebp
...[00000c16][00211979][00211989](02) 8bec mov ebp,esp
...[00000c18][0021196d][90909090](03) 83ec0c sub esp,+0c
...[00000c1b][0021196d][90909090](03) 8b450c mov
eax,[ebp+0c]
...[00000c1e][00211969][00000bf5](01) 50 push eax
...[00000c1f][00211969][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000c22][00211965][00000bf5](01) 51 push ecx
...[00000c23][00211961][00000c28](05) e8ddfdffff call 00000a05
...[00000bf5][0025c3b1][0025c3b5](01) 55 push ebp
...[00000bf6][0025c3b1][0025c3b5](02) 8bec mov ebp,esp
...[00000bf8][0025c3b1][0025c3b5](03) 8b4508 mov
eax,[ebp+08]
...[00000bfb][0025c3ad][00000bf5](01) 50 push eax
...[00000bfc][0025c3ad][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000bff][0025c3a9][00000bf5](01) 51 push ecx
...[00000c00][0025c3a5][00000c05](05) e810000000 call 00000c15
...[00000c15][0025c3a1][0025c3b1](01) 55 push ebp
...[00000c16][0025c3a1][0025c3b1](02) 8bec mov ebp,esp
...[00000c18][0025c395][90909090](03) 83ec0c sub esp,+0c
...[00000c1b][0025c395][90909090](03) 8b450c mov
eax,[ebp+0c]
...[00000c1e][0025c391][00000bf5](01) 50 push eax
...[00000c1f][0025c391][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000c22][0025c38d][00000bf5](01) 51 push ecx
...[00000c23][0025c389][00000c28](05) e8ddfdffff call 00000a05
Local Halt Decider: Infinite Recursion Detected Simulation Stopped
...[00000cd6][001018cd][90909090](03) 83c408 add esp,+08
...[00000cd9][001018cd][00000000](03) 8945f0 mov
[ebp-10],eax
...[00000cdc][001018cd][00000000](07) c745fc00000000 mov
[ebp-04],00000000
...[00000ce3][001018cd][00000000](02) eb09 jmp 00000cee
...[00000cee][001018cd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000cf2][001018cd][00000000](02) 7329 jnb 00000d1d
...[00000cf4][001018cd][00000000](04) 6b45fc0c imul
eax,[ebp-04],+0c
...[00000cf8][001018cd][00000000](03) 8b4df8 mov
ecx,[ebp-08]
...[00000cfb][001018cd][00000000](06) 89882f020000 mov
[eax+0000022f],ecx
...[00000d01][001018cd][00000000](04) 6b55fc0c imul
edx,[ebp-04],+0c
...[00000d05][001018cd][00000000](03) 8b45f4 mov
eax,[ebp-0c]
...[00000d08][001018cd][00000000](06) 89822f020000 mov
[edx+0000022f],eax
...[00000d0e][001018cd][00000000](04) 6b4dfc0c imul
ecx,[ebp-04],+0c
...[00000d12][001018cd][00000000](03) 8b55f0 mov
edx,[ebp-10]
...[00000d15][001018cd][00000000](06) 89912f020000 mov
[ecx+0000022f],edx
...[00000d1b][001018cd][00000000](02) ebc8 jmp 00000ce5
...[00000ce5][001018cd][00000000](03) 8b55fc mov
edx,[ebp-04]
...[00000ce8][001018cd][00000000](03) 83c201 add edx,+01
...[00000ceb][001018cd][00000000](03) 8955fc mov
[ebp-04],edx
...[00000cee][001018cd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000cf2][001018cd][00000000](02) 7329 jnb 00000d1d
...[00000cf4][001018cd][00000000](04) 6b45fc0c imul
eax,[ebp-04],+0c
...[00000cf8][001018cd][00000000](03) 8b4df8 mov
ecx,[ebp-08]
...[00000cfb][001018cd][00000000](06) 89882f020000 mov
[eax+0000022f],ecx
...[00000d01][001018cd][00000000](04) 6b55fc0c imul
edx,[ebp-04],+0c
...[00000d05][001018cd][00000000](03) 8b45f4 mov
eax,[ebp-0c]
...[00000d08][001018cd][00000000](06) 89822f020000 mov
[edx+0000022f],eax
...[00000d0e][001018cd][00000000](04) 6b4dfc0c imul
ecx,[ebp-04],+0c
...[00000d12][001018cd][00000000](03) 8b55f0 mov
edx,[ebp-10]
...[00000d15][001018cd][00000000](06) 89912f020000 mov
[ecx+0000022f],edx
...[00000d1b][001018cd][00000000](02) ebc8 jmp 00000ce5
...[00000ce5][001018cd][00000000](03) 8b55fc mov
edx,[ebp-04]
...[00000ce8][001018cd][00000000](03) 83c201 add edx,+01
...[00000ceb][001018cd][00000000](03) 8955fc mov
[ebp-04],edx
...[00000cee][001018cd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000cf2][001018cd][00000000](02) 7329 jnb 00000d1d
...[00000cf4][001018cd][00000000](04) 6b45fc0c imul
eax,[ebp-04],+0c
...[00000cf8][001018cd][00000000](03) 8b4df8 mov
ecx,[ebp-08]
...[00000cfb][001018cd][00000000](06) 89882f020000 mov
[eax+0000022f],ecx
...[00000d01][001018cd][00000000](04) 6b55fc0c imul
edx,[ebp-04],+0c
...[00000d05][001018cd][00000000](03) 8b45f4 mov
eax,[ebp-0c]
...[00000d08][001018cd][00000000](06) 89822f020000 mov
[edx+0000022f],eax
...[00000d0e][001018cd][00000000](04) 6b4dfc0c imul
ecx,[ebp-04],+0c
...[00000d12][001018cd][00000000](03) 8b55f0 mov
edx,[ebp-10]
...[00000d15][001018cd][00000000](06) 89912f020000 mov
[ecx+0000022f],edx
...[00000d1b][001018cd][00000000](02) ebc8 jmp 00000ce5
...[00000ce5][001018cd][00000000](03) 8b55fc mov
edx,[ebp-04]
...[00000ce8][001018cd][00000000](03) 83c201 add edx,+01
...[00000ceb][001018cd][00000000](03) 8955fc mov
[ebp-04],edx
...[00000cee][001018cd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000cf2][001018cd][00000000](02) 7329 jnb 00000d1d
...[00000cf4][001018cd][00000000](04) 6b45fc0c imul
eax,[ebp-04],+0c
...[00000cf8][001018cd][00000000](03) 8b4df8 mov
ecx,[ebp-08]
...[00000cfb][001018cd][00000000](06) 89882f020000 mov
[eax+0000022f],ecx
...[00000d01][001018cd][00000000](04) 6b55fc0c imul
edx,[ebp-04],+0c
...[00000d05][001018cd][00000000](03) 8b45f4 mov
eax,[ebp-0c]
...[00000d08][001018cd][00000000](06) 89822f020000 mov
[edx+0000022f],eax
...[00000d0e][001018cd][00000000](04) 6b4dfc0c imul
ecx,[ebp-04],+0c
...[00000d12][001018cd][00000000](03) 8b55f0 mov
edx,[ebp-10]
...[00000d15][001018cd][00000000](06) 89912f020000 mov
[ecx+0000022f],edx
...[00000d1b][001018cd][00000000](02) ebc8 jmp 00000ce5
...[00000ce5][001018cd][00000000](03) 8b55fc mov
edx,[ebp-04]
...[00000ce8][001018cd][00000000](03) 83c201 add edx,+01
...[00000ceb][001018cd][00000000](03) 8955fc mov
[ebp-04],edx
...[00000cee][001018cd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000cf2][001018cd][00000000](02) 7329 jnb 00000d1d
...[00000d1d][001018dd][001018e9](02) 8be5 mov esp,ebp
...[00000d1f][001018e1][00000d2e](01) 5d pop ebp
...[00000d20][001018e5][00000000](01) c3 ret
...[00000d2e][001018e1][00000bf5](05) 68f50b0000 push 00000bf5
...[00000d33][001018dd][00000bf5](05) 68f50b0000 push 00000bf5
...[00000d38][001018d9][00000d3d](05) e8d8feffff call 00000c15
...[00000c15][001018d5][001018e9](01) 55 push ebp
...[00000c16][001018d5][001018e9](02) 8bec mov ebp,esp
...[00000c18][001018c9][00000bf5](03) 83ec0c sub esp,+0c
...[00000c1b][001018c9][00000bf5](03) 8b450c mov
eax,[ebp+0c]
...[00000c1e][001018c5][00000bf5](01) 50 push eax
...[00000c1f][001018c5][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000c22][001018c1][00000bf5](01) 51 push ecx
...[00000c23][001018bd][00000c28](05) e8ddfdffff call 00000a05
Begin Local Halt Decider Simulation at Machine Address:bf5
...[00000bf5][0026c451][0026c455](01) 55 push ebp
...[00000bf6][0026c451][0026c455](02) 8bec mov ebp,esp
...[00000bf8][0026c451][0026c455](03) 8b4508 mov
eax,[ebp+08]
...[00000bfb][0026c44d][00000bf5](01) 50 push eax
...[00000bfc][0026c44d][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000bff][0026c449][00000bf5](01) 51 push ecx
...[00000c00][0026c445][00000c05](05) e810000000 call 00000c15
...[00000c15][0026c441][0026c451](01) 55 push ebp
...[00000c16][0026c441][0026c451](02) 8bec mov ebp,esp
...[00000c18][0026c435][90909090](03) 83ec0c sub esp,+0c
...[00000c1b][0026c435][90909090](03) 8b450c mov
eax,[ebp+0c]
...[00000c1e][0026c431][00000bf5](01) 50 push eax
...[00000c1f][0026c431][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000c22][0026c42d][00000bf5](01) 51 push ecx
...[00000c23][0026c429][00000c28](05) e8ddfdffff call 00000a05
...[00000bf5][002b6e79][002b6e7d](01) 55 push ebp
...[00000bf6][002b6e79][002b6e7d](02) 8bec mov ebp,esp
...[00000bf8][002b6e79][002b6e7d](03) 8b4508 mov
eax,[ebp+08]
...[00000bfb][002b6e75][00000bf5](01) 50 push eax
...[00000bfc][002b6e75][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000bff][002b6e71][00000bf5](01) 51 push ecx
...[00000c00][002b6e6d][00000c05](05) e810000000 call 00000c15
...[00000c15][002b6e69][002b6e79](01) 55 push ebp
...[00000c16][002b6e69][002b6e79](02) 8bec mov ebp,esp
...[00000c18][002b6e5d][90909090](03) 83ec0c sub esp,+0c
...[00000c1b][002b6e5d][90909090](03) 8b450c mov
eax,[ebp+0c]
...[00000c1e][002b6e59][00000bf5](01) 50 push eax
...[00000c1f][002b6e59][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000c22][002b6e55][00000bf5](01) 51 push ecx
...[00000c23][002b6e51][00000c28](05) e8ddfdffff call 00000a05
Local Halt Decider: Infinite Recursion Detected Simulation Stopped
...[00000c28][001018c9][00000bf5](03) 83c408 add esp,+08
...[00000c2b][001018c9][00000000](03) 8945f4 mov
[ebp-0c],eax
...[00000c2e][001018c9][00000000](07) c745fc00000000 mov
[ebp-04],00000000
...[00000c35][001018c9][00000000](02) eb09 jmp 00000c40
...[00000c40][001018c9][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c44][001018c9][00000000](02) 7d67 jnl 00000cad
...[00000c46][001018c9][00000000](04) 6b45fc0c imul
eax,[ebp-04],+0c
...[00000c4a][001018c9][00000000](05) 052f020000 add
eax,0000022f
...[00000c4f][001018c9][00000000](03) 8945f8 mov
[ebp-08],eax
...[00000c52][001018c9][00000000](03) 8b4df8 mov
ecx,[ebp-08]
...[00000c55][001018c9][00000000](02) 8b11 mov edx,[ecx]
...[00000c57][001018c9][00000000](03) 3b5508 cmp
edx,[ebp+08]
...[00000c5a][001018c9][00000000](02) 753a jnz 00000c96
...[00000c96][001018c9][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c9a][001018c9][00000000](02) 7c0f jl 00000cab
...[00000cab][001018c9][00000000](02) eb8a jmp 00000c37
...[00000c37][001018c9][00000000](03) 8b55fc mov
edx,[ebp-04]
...[00000c3a][001018c9][00000000](03) 83c201 add edx,+01
...[00000c3d][001018c9][00000000](03) 8955fc mov
[ebp-04],edx
...[00000c40][001018c9][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c44][001018c9][00000000](02) 7d67 jnl 00000cad
...[00000c46][001018c9][00000000](04) 6b45fc0c imul
eax,[ebp-04],+0c
...[00000c4a][001018c9][00000000](05) 052f020000 add
eax,0000022f
...[00000c4f][001018c9][00000000](03) 8945f8 mov
[ebp-08],eax
...[00000c52][001018c9][00000000](03) 8b4df8 mov
ecx,[ebp-08]
...[00000c55][001018c9][00000000](02) 8b11 mov edx,[ecx]
...[00000c57][001018c9][00000000](03) 3b5508 cmp
edx,[ebp+08]
...[00000c5a][001018c9][00000000](02) 753a jnz 00000c96
...[00000c96][001018c9][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c9a][001018c9][00000000](02) 7c0f jl 00000cab
...[00000cab][001018c9][00000000](02) eb8a jmp 00000c37
...[00000c37][001018c9][00000000](03) 8b55fc mov
edx,[ebp-04]
...[00000c3a][001018c9][00000000](03) 83c201 add edx,+01
...[00000c3d][001018c9][00000000](03) 8955fc mov
[ebp-04],edx
...[00000c40][001018c9][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c44][001018c9][00000000](02) 7d67 jnl 00000cad
...[00000c46][001018c9][00000000](04) 6b45fc0c imul
eax,[ebp-04],+0c
...[00000c4a][001018c9][00000000](05) 052f020000 add
eax,0000022f
...[00000c4f][001018c9][00000000](03) 8945f8 mov
[ebp-08],eax
...[00000c52][001018c9][00000000](03) 8b4df8 mov
ecx,[ebp-08]
...[00000c55][001018c9][00000000](02) 8b11 mov edx,[ecx]
...[00000c57][001018c9][00000000](03) 3b5508 cmp
edx,[ebp+08]
...[00000c5a][001018c9][00000000](02) 753a jnz 00000c96
...[00000c96][001018c9][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c9a][001018c9][00000000](02) 7c0f jl 00000cab
...[00000cab][001018c9][00000000](02) eb8a jmp 00000c37
...[00000c37][001018c9][00000000](03) 8b55fc mov
edx,[ebp-04]
...[00000c3a][001018c9][00000000](03) 83c201 add edx,+01
...[00000c3d][001018c9][00000000](03) 8955fc mov
[ebp-04],edx
...[00000c40][001018c9][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c44][001018c9][00000000](02) 7d67 jnl 00000cad
...[00000c46][001018c9][00000000](04) 6b45fc0c imul
eax,[ebp-04],+0c
...[00000c4a][001018c9][00000000](05) 052f020000 add
eax,0000022f
...[00000c4f][001018c9][00000000](03) 8945f8 mov
[ebp-08],eax
...[00000c52][001018c9][00000000](03) 8b4df8 mov
ecx,[ebp-08]
...[00000c55][001018c9][00000000](02) 8b11 mov edx,[ecx]
...[00000c57][001018c9][00000000](03) 3b5508 cmp
edx,[ebp+08]
...[00000c5a][001018c9][00000000](02) 753a jnz 00000c96
...[00000c96][001018c9][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c9a][001018c9][00000000](02) 7c0f jl 00000cab
...[00000cab][001018c9][00000000](02) eb8a jmp 00000c37
...[00000c37][001018c9][00000000](03) 8b55fc mov
edx,[ebp-04]
...[00000c3a][001018c9][00000000](03) 83c201 add edx,+01
...[00000c3d][001018c9][00000000](03) 8955fc mov
[ebp-04],edx
...[00000c40][001018c9][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c44][001018c9][00000000](02) 7d67 jnl 00000cad
...[00000cad][001018c9][00000000](03) 8b45f4 mov
eax,[ebp-0c]
...[00000cb0][001018d5][001018e9](02) 8be5 mov esp,ebp
...[00000cb2][001018d9][00000d3d](01) 5d pop ebp
...[00000cb3][001018dd][00000bf5](01) c3 ret
...[00000d3d][001018e5][00000000](03) 83c408 add esp,+08
...[00000d40][001018e5][00000000](03) 8945fc mov
[ebp-04],eax
...[00000d43][001018e5][00000000](03) 8b45fc mov
eax,[ebp-04]
...[00000d46][001018e1][00000000](01) 50 push eax
...[00000d47][001018dd][000003c7](05) 68c7030000 push 000003c7
...[00000d4c][001018d9][00000d51](05) e8b4f6ffff call 00000405
Input halts = 0
...[00000d51][001018e5][00000000](03) 83c408 add esp,+08
...[00000d54][001018e1][00000bf5](05) 68f50b0000 push 00000bf5
...[00000d59][001018dd][00000d5e](05) e897feffff call 00000bf5
...[00000bf5][001018d9][001018e9](01) 55 push ebp
...[00000bf6][001018d9][001018e9](02) 8bec mov ebp,esp
...[00000bf8][001018d9][001018e9](03) 8b4508 mov
eax,[ebp+08]
...[00000bfb][001018d5][00000bf5](01) 50 push eax
...[00000bfc][001018d5][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000bff][001018d1][00000bf5](01) 51 push ecx
...[00000c00][001018cd][00000c05](05) e810000000 call 00000c15
...[00000c15][001018c9][001018d9](01) 55 push ebp
...[00000c16][001018c9][001018d9](02) 8bec mov ebp,esp
...[00000c18][001018bd][00000c28](03) 83ec0c sub esp,+0c
...[00000c1b][001018bd][00000c28](03) 8b450c mov
eax,[ebp+0c]
...[00000c1e][001018b9][00000bf5](01) 50 push eax
...[00000c1f][001018b9][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000c22][001018b5][00000bf5](01) 51 push ecx
...[00000c23][001018b1][00000c28](05) e8ddfdffff call 00000a05
Begin Local Halt Decider Simulation at Machine Address:bf5
...[00000bf5][002c6f19][002c6f1d](01) 55 push ebp
...[00000bf6][002c6f19][002c6f1d](02) 8bec mov ebp,esp
...[00000bf8][002c6f19][002c6f1d](03) 8b4508 mov
eax,[ebp+08]
...[00000bfb][002c6f15][00000bf5](01) 50 push eax
...[00000bfc][002c6f15][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000bff][002c6f11][00000bf5](01) 51 push ecx
...[00000c00][002c6f0d][00000c05](05) e810000000 call 00000c15
...[00000c15][002c6f09][002c6f19](01) 55 push ebp
...[00000c16][002c6f09][002c6f19](02) 8bec mov ebp,esp
...[00000c18][002c6efd][90909090](03) 83ec0c sub esp,+0c
...[00000c1b][002c6efd][90909090](03) 8b450c mov
eax,[ebp+0c]
...[00000c1e][002c6ef9][00000bf5](01) 50 push eax
...[00000c1f][002c6ef9][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000c22][002c6ef5][00000bf5](01) 51 push ecx
...[00000c23][002c6ef1][00000c28](05) e8ddfdffff call 00000a05
...[00000bf5][00311941][00311945](01) 55 push ebp
...[00000bf6][00311941][00311945](02) 8bec mov ebp,esp
...[00000bf8][00311941][00311945](03) 8b4508 mov
eax,[ebp+08]
...[00000bfb][0031193d][00000bf5](01) 50 push eax
...[00000bfc][0031193d][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000bff][00311939][00000bf5](01) 51 push ecx
...[00000c00][00311935][00000c05](05) e810000000 call 00000c15
...[00000c15][00311931][00311941](01) 55 push ebp
...[00000c16][00311931][00311941](02) 8bec mov ebp,esp
...[00000c18][00311925][90909090](03) 83ec0c sub esp,+0c
...[00000c1b][00311925][90909090](03) 8b450c mov
eax,[ebp+0c]
...[00000c1e][00311921][00000bf5](01) 50 push eax
...[00000c1f][00311921][00000bf5](03) 8b4d08 mov
ecx,[ebp+08]
...[00000c22][0031191d][00000bf5](01) 51 push ecx
...[00000c23][00311919][00000c28](05) e8ddfdffff call 00000a05
Local Halt Decider: Infinite Recursion Detected Simulation Stopped
...[00000c28][001018bd][00000c28](03) 83c408 add esp,+08
...[00000c2b][001018bd][00000000](03) 8945f4 mov
[ebp-0c],eax
...[00000c2e][001018bd][00000000](07) c745fc00000000 mov
[ebp-04],00000000
...[00000c35][001018bd][00000000](02) eb09 jmp 00000c40
...[00000c40][001018bd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c44][001018bd][00000000](02) 7d67 jnl 00000cad
...[00000c46][001018bd][00000000](04) 6b45fc0c imul
eax,[ebp-04],+0c
...[00000c4a][001018bd][00000000](05) 052f020000 add
eax,0000022f
...[00000c4f][001018bd][00000000](03) 8945f8 mov
[ebp-08],eax
...[00000c52][001018bd][00000000](03) 8b4df8 mov
ecx,[ebp-08]
...[00000c55][001018bd][00000000](02) 8b11 mov edx,[ecx]
...[00000c57][001018bd][00000000](03) 3b5508 cmp
edx,[ebp+08]
...[00000c5a][001018bd][00000000](02) 753a jnz 00000c96
...[00000c96][001018bd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c9a][001018bd][00000000](02) 7c0f jl 00000cab
...[00000cab][001018bd][00000000](02) eb8a jmp 00000c37
...[00000c37][001018bd][00000000](03) 8b55fc mov
edx,[ebp-04]
...[00000c3a][001018bd][00000000](03) 83c201 add edx,+01
...[00000c3d][001018bd][00000000](03) 8955fc mov
[ebp-04],edx
...[00000c40][001018bd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c44][001018bd][00000000](02) 7d67 jnl 00000cad
...[00000c46][001018bd][00000000](04) 6b45fc0c imul
eax,[ebp-04],+0c
...[00000c4a][001018bd][00000000](05) 052f020000 add
eax,0000022f
...[00000c4f][001018bd][00000000](03) 8945f8 mov
[ebp-08],eax
...[00000c52][001018bd][00000000](03) 8b4df8 mov
ecx,[ebp-08]
...[00000c55][001018bd][00000000](02) 8b11 mov edx,[ecx]
...[00000c57][001018bd][00000000](03) 3b5508 cmp
edx,[ebp+08]
...[00000c5a][001018bd][00000000](02) 753a jnz 00000c96
...[00000c96][001018bd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c9a][001018bd][00000000](02) 7c0f jl 00000cab
...[00000cab][001018bd][00000000](02) eb8a jmp 00000c37
...[00000c37][001018bd][00000000](03) 8b55fc mov
edx,[ebp-04]
...[00000c3a][001018bd][00000000](03) 83c201 add edx,+01
...[00000c3d][001018bd][00000000](03) 8955fc mov
[ebp-04],edx
...[00000c40][001018bd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c44][001018bd][00000000](02) 7d67 jnl 00000cad
...[00000c46][001018bd][00000000](04) 6b45fc0c imul
eax,[ebp-04],+0c
...[00000c4a][001018bd][00000000](05) 052f020000 add
eax,0000022f
...[00000c4f][001018bd][00000000](03) 8945f8 mov
[ebp-08],eax
...[00000c52][001018bd][00000000](03) 8b4df8 mov
ecx,[ebp-08]
...[00000c55][001018bd][00000000](02) 8b11 mov edx,[ecx]
...[00000c57][001018bd][00000000](03) 3b5508 cmp
edx,[ebp+08]
...[00000c5a][001018bd][00000000](02) 753a jnz 00000c96
...[00000c96][001018bd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c9a][001018bd][00000000](02) 7c0f jl 00000cab
...[00000cab][001018bd][00000000](02) eb8a jmp 00000c37
...[00000c37][001018bd][00000000](03) 8b55fc mov
edx,[ebp-04]
...[00000c3a][001018bd][00000000](03) 83c201 add edx,+01
...[00000c3d][001018bd][00000000](03) 8955fc mov
[ebp-04],edx
...[00000c40][001018bd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c44][001018bd][00000000](02) 7d67 jnl 00000cad
...[00000c46][001018bd][00000000](04) 6b45fc0c imul
eax,[ebp-04],+0c
...[00000c4a][001018bd][00000000](05) 052f020000 add
eax,0000022f
...[00000c4f][001018bd][00000000](03) 8945f8 mov
[ebp-08],eax
...[00000c52][001018bd][00000000](03) 8b4df8 mov
ecx,[ebp-08]
...[00000c55][001018bd][00000000](02) 8b11 mov edx,[ecx]
...[00000c57][001018bd][00000000](03) 3b5508 cmp
edx,[ebp+08]
...[00000c5a][001018bd][00000000](02) 753a jnz 00000c96
...[00000c96][001018bd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c9a][001018bd][00000000](02) 7c0f jl 00000cab
...[00000cab][001018bd][00000000](02) eb8a jmp 00000c37
...[00000c37][001018bd][00000000](03) 8b55fc mov
edx,[ebp-04]
...[00000c3a][001018bd][00000000](03) 83c201 add edx,+01
...[00000c3d][001018bd][00000000](03) 8955fc mov
[ebp-04],edx
...[00000c40][001018bd][00000000](04) 837dfc04 cmp dword
[ebp-04],+04
...[00000c44][001018bd][00000000](02) 7d67 jnl 00000cad
...[00000cad][001018bd][00000000](03) 8b45f4 mov
eax,[ebp-0c]
...[00000cb0][001018c9][001018d9](02) 8be5 mov esp,ebp
...[00000cb2][001018cd][00000c05](01) 5d pop ebp
...[00000cb3][001018d1][00000bf5](01) c3 ret
...[00000c05][001018d9][001018e9](03) 83c408 add esp,+08
...[00000c08][001018d9][001018e9](02) 85c0 test eax,eax
...[00000c0a][001018d9][001018e9](02) 7402 jz 00000c0e
...[00000c0e][001018dd][00000d5e](01) 5d pop ebp
...[00000c0f][001018e1][00000bf5](01) c3 ret
...[00000d5e][001018e5][00000000](03) 83c404 add esp,+04
...[00000d61][001018e1][000003d7](05) 68d7030000 push 000003d7
...[00000d66][001018dd][00000d6b](05) e88af6ffff call 000003f5
Halt returned
...[00000d6b][001018e5][00000000](03) 83c404 add esp,+04
...[00000d6e][001018e5][00000000](02) 33c0 xor eax,eax
...[00000d70][001018e9][00000000](02) 8be5 mov esp,ebp
...[00000d72][001018ed][00100000](01) 5d pop ebp
...[00000d73][001018f1][000005a0](01) c3 ret
Number_of_User_Instructions(361)
Number of Instructions Executed(137897)

Kaz Kylheku

unread,
May 7, 2021, 2:39:07 PM5/7/21
to
["Followup-To:" header set to comp.theory.]
I don't understand the purpose of this initializer, given
that Init_res is called.

If omission of the initializer is sufficient for zero initialization
(as normally required by ISO C for a static object) please remove it.

Otherwise use res[NRES] = {{0}};

By the way [4] is my mistake; it was intended to be [NRES]. NRES is 4,
but could change, causing a problem.


> void H_Hat(u32 P)
> {
> if (HaltsProxy(P, P))
> loop: goto loop;
> }
>
> void Init_res()
> {
> u32 P = (u32)H_Hat, I = (u32)H_Hat;
> u32 H = Halts(P, I);
> for (u32 N = 0; N < NRES; N++)
> {
> res[N].P = P;
> res[N].I = I;
> res[N].H = H;
> }
> }

This doesn't make a whole lot of sense. The initialization has no need
to call Halts at all; that should be left to the experiment.

We want the database to be initially empty, not having any knowledge
about any halts results.

Filling the array with *identical* keys makes no sense, and leaves no
room for any other P, I value should that happen.

> u32 HaltsProxy(u32 P, u32 I)
> {
> int i;
> u32 H = Halts(P, I); // call real Halts
> for (i = 0; i < NRES; i++)
> {
> struct HaltResult *r = &res[i];
>
> if (r->P == P && r->I == I)
> {
> // Repeat call for same P, I.
> H = Halts(P, I); // call real Halts

Calling Halts(P, I) more than once in this function does not make sense.

Halts(P, I) was already called at the top, and H holds the result.
Please delete this call to Halts.

> if (r->H != H)
> {
> // Halts has returned a different value
> OutputString("Halt decider is not an algorithm!");
> loop0: goto loop0;
> }
> // Same value; we are done checking.
> break;
> }

> if (i >= NRES)

This statement was originally outside of the loop.

The condition i >= NRES indicates that the loop completed without a
"break". That means that (P, I) was not found in the array, and that the
array contains no more blank space toc reate a new entry for the newly
observed (P, I) value.

NOte that testing (i >= NRES) inside the for loop makes no
sense, because the loop guard assures that the condition is always
false: for (i = 0; i < NRES; i++). See the "i < NRES"? The loop body
does not execute unless i < NRES< therefore i >= NRES is false inside
the loop body.

You've turned a piece of my code that serves a purpose into unreachable
code.

Also, please restore the logic which adds new entries into blank spots in
the array.

{
> // Array has filled up, what? We only call this twice.
> OutputString("Unexpected excess calls to HaltsProxy!");
> loop1: goto loop1;
> }
> }
> return H;
> }

In spite of these problems, I think it look as if the the code should
still catch the situation of Halts being inconsistent.
>
> int main()
> {
> Init_res();
> u32 H = HaltsProxy((u32) H_Hat, (u32) H_Hat);
> Output("Input halts = ", H);
> H_Hat((u32) H_Hat);
> OutputString("Halt returned");

My mistake: please correct to H_Hat returned.

> return 0;
> }

OK, so onto the trace. In the trace we see:

> Input halts = 0

thus Halts(H_Hat, H_Hat) returned 0 when called out of main via
HaltsProxy.

In the trace we also see this output:

> Halt returned

This actually means H_Hat returned, the code being

H_Hat((u32) H_Hat);
OutputString("Halt returned");

Since "Input_Halts = 0" means "H_Hat(H_Hat) does not halt", but
H_Hat(H_Hat) returns, that means it's the wrong halting answer,
doesn't it?

So while we didn't see an inconsistent return value from Halts (which is
good!) the program's behavior appears to support the halting proof,
rather than refute it.

Of course if Halts(H_Hat, H_Hat) consistently returns 0, that
consistency being required, then H_Hat(H_Hat) returns. It obtains the
that 0 from Halts and "behaves opposite" by just returning, making that
the wrong answer.

I specifically did not miss these two pieces of output in your trace:

> Begin Local Halt Decider Simulation at Machine Address:bf5

Firstly, you had previously claimed that the local decider mode was
a mistake and have abandoned it; does Local Halt Decider not refer
to this mode, or is that something else now.

And, more importantly:

> Local Halt Decider: Infinite Recursion Detected Simulation Stopped

Though it claims it has detected infinite recursion and that the simulation has
stopped, the fact is that the traces continue after this diagnostic. The
simuation has not actually stopped!

Moreover, the claim of infinite recursion is difficult to accept given that:

1. Halts((u32) H_Hat, (u32) H_Hat) cheerfully terminated with value 0.

2. H_Hat((u32) H_Hat) returned to subsequent Output statement

I understand you have some talking points around all this, but they don't make
sense, especially in relation to the simplicity of arriving at the conclusion
that the apparatus is simply confirming the proof.

--
TXR Programming Language: http://nongnu.org/txr
Cygnal: Cygwin Native Application Library: http://kylheku.com/cygnal

olcott

unread,
May 7, 2021, 5:13:55 PM5/7/21
to
On 5/7/2021 3:37 PM, Kaz Kylheku wrote:
> On 2021-05-07, olcott <No...@NoWhere.com> wrote:
>> #define NRES 4
>>
>> struct HaltResult
>> {
>> u32 P, I, H;
>> };
>>
>> struct HaltResult res[4] = {{1,1,1},{2,2,2},{3,3,3},{4,4,4}};
>
> It would be good if you would pick up the res[NRES] fix here,
> as well as Output("H_Hat returned") in main.
>
>>
>> void Init_res()
>> {
>> for (u32 N = 0; N < NRES; N++)
>> {
>> res[N].P = 0;
>> res[N].I = 0;
>> res[N].H = 0;
>> }
>> }
>
> Yes, this initialization now meets the intent of the original code.
>
> I think that for the longer term, it would be good to repair your COFF
> loader so that it handles the zero-initialized data which is indicated
> in the COFF file.
>
> Then you can explore whatever C code you want without workarounds
> for zero-initialized statics.
>

Yes as soon as my halt decider is accepted as correct this is first on
the list of enhacements.

>> if (i >= NRES)
>> {
>> // Array has filled up, what? We only call this twice.
>> OutputString("Unexpected excess calls to HaltsProxy!");
>> loop1: goto loop1;
>> }
>
> Nitpick: that should still be restored to its position outside of the
> loop. We never run into this condition either way, since we don't work
> with multiple unique P, I pairs.
>

I only corrected syntax errors in your code.
Your code stipulates that it is inside the loop.

You probably got confused by your formatting conventions. I always match
curly braces on a line by themselves with the same indentation level.

> Otherwise you might as well remove this code; it is unreachable.
>
>> }
>> return H;
>> }
>>

It is not unreachable.

>>
>> void H_Hat4(u32 P)
>
> Seeing you use different names for different H_Hat versions is
> encouraging.
>

Good.

>> int TestHaltsProxy()
>> {
>> Init_res();
>> u32 H = HaltsProxy((u32) H_Hat4, (u32) H_Hat4);
>> Output("Input halts = ", H);
>> H_Hat4((u32) H_Hat4);
>> OutputString("Halt returned");
>
> Please correct to "H_Hat4 returned"; that was my intent.
>

OK

> Your execution trace is essentially the same as before.
>
> The issue is that we see these, in that order:
>
>> Begin Local Halt Decider Simulation at Machine Address:d45
>
> (Halts starts running a nested simulated machine executing H_Hat4(H_Hat4)).
>
>> Local Halt Decider: Infinite Recursion Detected Simulation Stopped
>> ...[00000c88][0010192e][90909090](03) 83c408 add esp,+08
>> ...[00000c8b][0010192e][00000000](03) 8945f4 mov
>
> (outer simulation continues)
>
>> Input halts = 0
>
> (Halts has returned 0 to main.)
>
>> Begin Local Halt Decider Simulation at Machine Address:d45
>
> (another nested simulation: this is due to H_Hat4(H_Hat4) calling Halts!)
>
>> Local Halt Decider: Infinite Recursion Detected Simulation Stopped
>
> (stops again, but surrounding simulation keeps going)
>
>> Halt returned
>
> Oops, H_Hat4(H_Hat4) returns due to getting getting a 0 from Halts.
>
> So the 0 is incorrect: a direct call to H_Hat4(H_Hat4) returns.
>

Halts(H_Hat, H_Hat) is an instance of both of these truisms:

It is true that every computation that would never halt unless its
simulation was stopped is a non-halting computation. Some may disagree
out of ignorance or deception none-the-less it remains a truism.

Every at least partial halt decider that decides to stop simulating its
input on the basis that the execution trace of this input matches a
correct non-halting behavior pattern does decide not halting correctly.

Do you understand that disagreeing with an actual truism is always
necessarily incorrect?

> The "Input halts = 0" result has exactly the meaning that "a direct call
> to H_Hat4(H_Hat4) out of main shall not terminate". Yet that's exactly
> what that call does.

olcott

unread,
May 8, 2021, 12:18:54 PM5/8/21
to
On 5/7/2021 9:12 PM, Ben Bacarisse wrote:
> Richard Damon <Ric...@Damon-Family.org> writes:
>
>> What intuitition is needed. You posted a trace of H_Hat(H_Hat) and it
>> shows that H_Hat(H_Hat) came to a halt.
>>
>> What is your response to that?
>
> I think we finally know:
>
> "the fact that a computation halts does not entail that it is a halting
> computation" Peter Olcott, May 2021.
>
> Presumably that fact that H_Hat(H_Hat) halts does not entail that
> H_Hat(H_Hat) is a halting computation, so you can answer "no" if the
> mood takes you.

On 11/27/2020 9:02 PM, Ben Bacarisse wrote:
> A computation that would not halt if its simulation were not
> halted is indeed a non-halting computation. But a computation that
> would not halt and one that is halted are different computations.

It is true that every computation that would never halt unless its
simulation was stopped is a non-halting computation.

As is shown by the following example computations meeting this criteria
remain non-halting even after they are forced to halt by their halt
deciding simulator thus contradicting Ben's second sentence.

_Infinite_Loop()
[00000aaf](01) 55 push ebp
[00000ab0](02) 8bec mov ebp,esp
[00000ab2](02) ebfe jmp 00000ab2
[00000ab4](01) 5d pop ebp
[00000ab5](01) c3 ret
Size in bytes:(0007) [00000ab5]

// (a) The instruction is a JMP instruction.
// (b) It is jumping upward or to its own address.
// (c) There are no conditional branch instructions inbetween.
// (d) There are no other JMP instructions inbetween (André G. Isaak)

When we apply the above criteria to the above code a program can
definitively decide that it would not halt. When the above code is
simulated its execution trace indicates that it would not halt because
its behavior matches the above criteria.

This remains true even after _Infinite_Loop() is forced to halt because
the halt deciding simulator stopped simulating it. Thus Ben's first
sentence is correct and his second sentence is incorrect because it
contradicts his first sentence.

THIS IS A TRUISM:
It is true that every computation that would never halt unless its
simulation was stopped is a non-halting computation.

The fact that an {infinite loop, infinite recursion, infinitely nested
simulation) was forced to halt when its halt deciding simulator decided
that its behavior matched a pattern of non-halting behavior and stopped
simulating it is the exceptional case where:

On 5/7/2021 9:12 PM, Ben Bacarisse wrote:
> "the fact that a computation halts does not entail that
> it is a halting computation" Peter Olcott, May 2021.
0 new messages