XPost: comp.theory, sci.logic, sci.math

On 11/25/2021 10:35 PM, André G. Isaak wrote:

On 2021-11-25 21:23, olcott wrote:

On 11/25/2021 9:15 PM, André G. Isaak wrote:

Do you not understand the difference between a SPECIFICATION and an
IMPLEMENTATION?

I have been giving you the specification of the halting problem, i.e.
a description of *exactly* which problem a halt decider must solve.
How you go about solving it is the implementation.

The halt decider H(x,y) does not simply take a pair of finite string
inputs and then make a good guess about whether this input reaches its
final state or not.

Nobody ever claimed otherwise. However, it must do this in a way that actually conforms to the specification of the problem given below. That
means that if the input is a description of P(P), it must map to 'halts'.

Halt decider H must derive a formal proof of the behavior of (x,y) based
on the sequence of configurations from x.q0 to x.qn.

You keep accusing people of 'vagueness' for not specifying these steps,
but bear in mind that Linz's H and H_Hat, aren't Turing Machines, they
are *variables* ranging over classes of Turing Machines, and the whole
point of his proof is to show that those classes are *empty*. You can't specify the specific steps involved in a nonexistent computation.

That is why I derived the 100% complete specificity of H/P.
My H/P <is> the (Strachey:1965) T/P

rec routine P
§L:if T[P] go to L
Return §

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

H(P,P) derives its formal proof of the behavior of its input based on
the x86 emulation of the machine code of its input from the start state
of P though N steps of P.

That you expect H to somehow imagine what you mean by the direct
execution of P(P) is ridiculous.

It is a formal proof that already has every single step completely
specified.

You're the one who claims that it actually is possible to create such a program despite the existence of proofs (note the plural) that the
halting function is not computable. So the onus is on you to actually
provide this 'sequence of configurations', not on anyone else.

But so far all you've done is created a program which fails to meet the specification which defines the problem that you purport to have solved
and thus which fails to demonstrate such an algorithm.

André

It must proceed through what is essentially a formal proof of the
behavior of this finite string pair.

This formal proof begins at x.q0 the start state and proceeds
through a sequence of quintuple configurations until N steps of
configurations have been specified.

N is either the final state of x.final or the number of steps required
for H to detect an infinite behavior pattern.

The SPECIFICATION of the problem is that a halt decider takes as its
input a description of a computation and determines whether that
computation, when run independently, halts.

P(P) halts, so by the specification of the problem any halt decider
which is passed a string representing P(P) *must* return true as its
answer. Any "halt decider" which fails to do this fails to implement
the specification.

All your nonsense about what P(P) does "inside H" is just that --
nonsense, because the specification clearly states that the decider
must describe the behaviour of P(P) as an independent computation.

If you don't grasp the distinction between a specification and an
implementation, read the C Standard. It describes the standard
library functions and gives a *specification* of what each function
must do. The actual implementation of these routines varies depending
on your IDE and operating system.

--
Copyright 2021 Pete Olcott

Talent hits a target no one else can hit;
Genius hits a target no one else can see.
Arthur Schopenhauer

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

XPost: comp.theory, sci.logic, sci.math

On 11/25/2021 11:49 PM, André G. Isaak wrote:

On 2021-11-25 22:06, olcott wrote:

On 11/25/2021 10:35 PM, André G. Isaak wrote:

On 2021-11-25 21:23, olcott wrote:

On 11/25/2021 9:15 PM, André G. Isaak wrote:

Do you not understand the difference between a SPECIFICATION and an
IMPLEMENTATION?

I have been giving you the specification of the halting problem,
i.e. a description of *exactly* which problem a halt decider must
solve. How you go about solving it is the implementation.

The halt decider H(x,y) does not simply take a pair of finite string
inputs and then make a good guess about whether this input reaches
its final state or not.

Nobody ever claimed otherwise. However, it must do this in a way that
actually conforms to the specification of the problem given below.
That means that if the input is a description of P(P), it must map to
'halts'.

Halt decider H must derive a formal proof of the behavior of (x,y)
based on the sequence of configurations from x.q0 to x.qn.

No.

A halt decider accepts or rejects a computation based on whether it
halts. It doesn't derive a formal proof, anymore than a program which
adds two numbers derives a formal proof. It just returns a sum.

You keep accusing people of 'vagueness' for not specifying these
steps, but bear in mind that Linz's H and H_Hat, aren't Turing
Machines, they are *variables* ranging over classes of Turing
Machines, and the whole point of his proof is to show that those
classes are *empty*. You can't specify the specific steps involved in
a nonexistent computation.

That is why I derived the 100% complete specificity of H/P.
My H/P <is> the (Strachey:1965) T/P

       rec routine P
         §L:if T[P] go to L
           Return §

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

How is Stratchey's code any more 'completely specified' than Linz? He
simply describes what T *does*. He doesn't provide a single line of code describing how it does it. Just as in the Linz proof, his T is a
*variable* ranging over an (empty) class of programs.

H(P,P) derives its formal proof of the behavior of its input based on
the x86 emulation of the machine code of its input from the start
state of P though N steps of P.

That you expect H to somehow imagine what you mean by the direct
execution of P(P) is ridiculous.

What I mean by 'the direct execution of P(P)' is completely unambiguous
and is part of the halting problem's specification. H doesn't have to
imagine anything. YOU, as the programmer, have to ensure that the answer
it gives reflects the behaviour of int main { P(P); } since that is how
the halting problem is DEFINED.

It is a formal proof that already has every single step completely
specified.

Where is this 'formal proof' of which you speak?

The formal proof that I mean is every single step of the behavior of the
input that leads to the last instruction of this input or some kind of repeating cycle.

_H()
[00001a5e](01) 55 push ebp
[00001a5f](02) 8bec mov ebp,esp
[00001a61](03) 8b450c mov eax,[ebp+0c]
[00001a64](01) 50 push eax // push P
[00001a65](03) ff5508 call dword [ebp+08] // call P
[00001a68](03) 83c404 add esp,+04
[00001a6b](05) b801000000 mov eax,00000001
[00001a70](01) 5d pop ebp
[00001a71](01) c3 ret
Size in bytes:(0020) [00001a71]

_P()
[00001a7e](01) 55 push ebp
[00001a7f](02) 8bec mov ebp,esp
[00001a81](03) 8b4508 mov eax,[ebp+08]
[00001a84](01) 50 push eax // push P
[00001a85](03) 8b4d08 mov ecx,[ebp+08]
[00001a88](01) 51 push ecx // push P
[00001a89](05) e8d0ffffff call 00001a5e // call H
[00001a8e](03) 83c408 add esp,+08
[00001a91](05) b801000000 mov eax,00000001
[00001a96](01) 5d pop ebp
[00001a97](01) c3 ret
Size in bytes:(0026) [00001a97]

_main()
[00001a9e](01) 55 push ebp
[00001a9f](02) 8bec mov ebp,esp
[00001aa1](05) 687e1a0000 push 00001a7e // push P
[00001aa6](05) 687e1a0000 push 00001a7e // push P
[00001aab](05) e8aeffffff call 00001a5e // call H
[00001ab0](03) 83c408 add esp,+08
[00001ab3](02) 33c0 xor eax,eax
[00001ab5](01) 5d pop ebp
[00001ab6](01) c3 ret
Size in bytes:(0025) [00001ab6]

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= ============= [00001a9e][00102ec8][00000000] 55 push ebp [00001a9f][00102ec8][00000000] 8bec mov ebp,esp [00001aa1][00102ec4][00001a7e] 687e1a0000 push 00001a7e // push P [00001aa6][00102ec0][00001a7e] 687e1a0000 push 00001a7e // push P [00001aab][00102ebc][00001ab0] e8aeffffff call 00001a5e // call H [00001a5e][00102eb8][00102ec8] 55 push ebp [00001a5f][00102eb8][00102ec8] 8bec mov ebp,esp [00001a61][00102eb8][00102ec8] 8b450c mov eax,[ebp+0c] [00001a64][00102eb4][00001a7e] 50 push eax // push P [00001a65][00102eb0][00001a68] ff5508 call dword [ebp+08] // call P [00001a7e][00102eac][00102eb8] 55 push ebp [00001a7f][00102eac][00102eb8] 8bec mov ebp,esp [00001a81][00102eac][00102eb8] 8b4508 mov eax,[ebp+08] [00001a84][00102ea8][00001a7e] 50 push eax // push P [00001a85][00102ea8][00001a7e] 8b4d08 mov ecx,[ebp+08] [00001a88][00102ea4][00001a7e] 51 push ecx // push P [00001a89][00102ea0][00001a8e] e8d0ffffff call 00001a5e // call H [00001a5e][00102e9c][00102eac] 55 push ebp [00001a5f][00102e9c][00102eac] 8bec mov ebp,esp [00001a61][00102e9c][00102eac] 8b450c mov eax,[ebp+0c] [00001a64][00102e98][00001a7e] 50 push eax // push P [00001a65][00102e94][00001a68] ff5508 call dword [ebp+08] // call P [00001a7e][00102e90][00102e9c] 55 push ebp [00001a7f][00102e90][00102e9c] 8bec mov ebp,esp [00001a81][00102e90][00102e9c] 8b4508 mov eax,[ebp+08] [00001a84][00102e8c][00001a7e] 50 push eax // push P [00001a85][00102e8c][00001a7e] 8b4d08 mov ecx,[ebp+08] [00001a88][00102e88][00001a7e] 51 push ecx [00001a89][00102e84][00001a8e] e8d0ffffff call 00001a5e // call H [00001a5e][00102e80][00102e90] 55 push ebp [00001a5f][00102e80][00102e90] 8bec mov ebp,esp [00001a61][00102e80][00102e90] 8b450c mov eax,[ebp+0c] [00001a64][00102e7c][00001a7e] 50 push eax // push P [00001a65][00102e78][00001a68] ff5508 call dword [ebp+08] // call P [00001a7e][00102e74][00102e80] 55 push ebp [00001a7f][00102e74][00102e80] 8bec mov ebp,esp [00001a81][00102e74][00102e80] 8b4508 mov eax,[ebp+08] [00001a84][00102e70][00001a7e] 50 push eax // push P [00001a85][00102e70][00001a7e] 8b4d08 mov ecx,[ebp+08] [00001a88][00102e6c][00001a7e] 51 push ecx // push P [00001a89][00102e68][00001a8e] e8d0ffffff call 00001a5e // call H

A turing machine program consists of a list of 'quintuples', each one of
which is a five-symbol turing machine instruction. For example, the
quintuple 'SCcsm' is executed by the machine if it is in state 'S' and
is reading the symbol 'C' on the tape. In that case, the instruction
causes the machine to make a transition to state 's' and to overwrite
the symbol 'C' on the tape with the symbol 'c'. The last operation it
performs under this instruction is to move the tape reading head one
symbol to the left or right according to whether 'm' is 'l' or 'r'. http://www.lns.mit.edu/~dsw/turing/doc/tm_manual.txt

The input to H(x,y) is a finite string pair where x is a list of
quintuples of Turing machine instructions and y is a finite string.

The formal proof of the behavior of N steps of x applied to y is the
sequence of configurations derived when a UTM is applied to x on input y
for N steps of configurations.

Do you even know what a formal proof is?

I am defining it more broadly as every inference step in sound deduction leading to a true conclusion.

The sequence of configurations of the direct execution or correct
simulation of a computation beginning at its start state through N steps
of configurations is the complete formal proof of the behavior of N
steps of x.

André

--
Copyright 2021 Pete Olcott

Talent hits a target no one else can hit;
Genius hits a target no one else can see.
Arthur Schopenhauer

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

XPost: comp.theory, sci.logic, sci.math

On 11/26/2021 10:46 AM, André G. Isaak wrote:

On 2021-11-26 08:29, olcott wrote:

On 11/25/2021 11:49 PM, André G. Isaak wrote:

Where is this 'formal proof' of which you speak?

The formal proof that I mean is every single step of the behavior of
the input that leads to the last instruction of this input or some
kind of repeating cycle.

<snip pointless trace>

That was a *trace*. A trace is no even remotely a formal proof. It is
simply a trace. You should review what a proof actually looks like.

<snip definition of Turing Machine -- we already know what a TM is>

The input to H(x,y) is a finite string pair where x is a list of
quintuples of Turing machine instructions and y is a finite string.

The formal proof of the behavior of N steps of x applied to y is the
sequence of configurations derived when a UTM is applied to x on input
y for N steps of configurations.

Do you even know what a formal proof is?

I am defining it more broadly as every inference step in sound
deduction leading to a true conclusion.

You are 'defining' it in a way which bears no resemblance to the actual definition of 'proof'. And a trace does not constitute a 'sound
deduction' either, nor does it include 'inference steps'.

So you are saying the the correct pure simulation of N steps of the
input to H(P,P) by H has no relationship what-so-ever to the actual
behavior of P(P)?

I say that the correct pure simulation of N steps of the input to H(x,y)
is the only correct halt deciding basis that any C/x86/TM halt decider
can possibly have.

There must be some sound deductive reasoning *underlying* an algorithm,
but the algorithm is not the same thing as that reasoning.

And in your case, it clearly doesn't involve sound deductive reasoning
since it gives the *wrong* answer.

H(P, P) is tasked with reporting on whether int main() { P(P); } halts.
That computation does indeed halt. Your H claims otherwise. Therefore it
is wrong.

André

--
Copyright 2021 Pete Olcott

Talent hits a target no one else can hit;
Genius hits a target no one else can see.
Arthur Schopenhauer

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

XPost: comp.theory, sci.logic, sci.math

On 11/26/2021 1:16 PM, André G. Isaak wrote:

On 2021-11-26 11:40, olcott wrote:

On 11/26/2021 10:46 AM, André G. Isaak wrote:

On 2021-11-26 08:29, olcott wrote:

On 11/25/2021 11:49 PM, André G. Isaak wrote:

Where is this 'formal proof' of which you speak?

The formal proof that I mean is every single step of the behavior of
the input that leads to the last instruction of this input or some
kind of repeating cycle.

<snip pointless trace>

That was a *trace*. A trace is no even remotely a formal proof. It is
simply a trace. You should review what a proof actually looks like.

<snip definition of Turing Machine -- we already know what a TM is>

The input to H(x,y) is a finite string pair where x is a list of
quintuples of Turing machine instructions and y is a finite string.

The formal proof of the behavior of N steps of x applied to y is the
sequence of configurations derived when a UTM is applied to x on
input y for N steps of configurations.

Do you even know what a formal proof is?

I am defining it more broadly as every inference step in sound
deduction leading to a true conclusion.

You are 'defining' it in a way which bears no resemblance to the
actual definition of 'proof'. And a trace does not constitute a
'sound deduction' either, nor does it include 'inference steps'.

So you are saying the the correct pure simulation of N steps of the
input to H(P,P) by H has no relationship what-so-ever to the actual
behavior of P(P)?

I say that the correct pure simulation of N steps of the input to
H(x,y) is the only correct halt deciding basis that any C/x86/TM halt
decider can possibly have.

Obviously it is not a 'correct pure simulation' since it gets the wrong answer to the question.

If you do not comprehend that there is a correct pure simulation of N
steps of the input to H(P,P) by H then you are insufficiently
technically competent.

You keep ignoring the specification of the problem.

André

--
Copyright 2021 Pete Olcott

Talent hits a target no one else can hit;
Genius hits a target no one else can see.
Arthur Schopenhauer

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

XPost: comp.theory, sci.logic, sci.math

On 11/28/2021 8:31 AM, André G. Isaak wrote:

On 2021-11-27 23:10, olcott wrote:

On 11/28/2021 12:01 AM, André G. Isaak wrote:

On 2021-11-27 21:49, olcott wrote:

On 11/27/2021 4:43 PM, André G. Isaak wrote:

On 2021-11-27 15:17, olcott wrote:

On 11/27/2021 3:42 PM, André G. Isaak wrote:

On 2021-11-27 14:30, olcott wrote:

On 11/27/2021 3:08 PM, André G. Isaak wrote:

On 2021-11-27 13:12, olcott wrote:

PSR set (pathological self-reference)
H1(P1,P1) Is the above code.
H2(P2,P2) Is the above code where H2 simulates rather than >>>>>>>>>> directly executes its input.
H3(P3,P3) Is the execution of N steps of the input of H1(P1,P1). >>>>>>>>>> H4(P4,P4) Is the simulation of N steps of the input of H2(P2,P2). >>>>>>>>>>
Every Hn(Px,Py) that returns a value returns 1 except for
instances of {H3, H4} that determine whether or not to return >>>>>>>>>> {0,1} on the basis of the behavior of their input.

The correct pure simulation of N steps of the input to H(P,P) >>>>>>>>>> by H is always a correct halt deciding basis where P has
reached its final state or H has correctly detected that P >>>>>>>>>> would never reach its final state.

The point in the sequence of N steps where the execution trace >>>>>>>>>> of the simulation of P shows that P is about to call H(P,P) >>>>>>>>>> again with the same input that H was called with provides
conclusive proof that P would be infinitely recursive unless H >>>>>>>>>> aborted its simulation.
In this H4(P4,P4)==0 computation P4 is dependent on H4
altering the behavior of P4.

When directly executed P(P) calls H(P,P) and the simulated >>>>>>>>>> P(P) reaches the point where it would call H(P,P) with the >>>>>>>>>> same parameters that H was called with H returns 0 to this >>>>>>>>>> directly executed P. In this H1(P4,P4)==1 computation P4 is >>>>>>>>>> independent of H1.

H is a computable function that accepts or rejects inputs in >>>>>>>>>> its domain on the basis that these inputs specify a sequence >>>>>>>>>> of configurations that reach their final state.

But none of your H's can correctly decide halting for its
corresponding P(P).

H1(P4,P4)=1 decides main() { P4(P4); }

But H4(P4, P4) doesn't. The Linz proof demonstrates that no H can >>>>>>> decide the P *derived from* that specific H. Showing that some
*other* H can decide it is irrelevant.

The Linz proof makes the huge mistake that:
main() { P4(P4) } <is>
main() { P4(P4) } calls H4(P4,P4) simulates P4(P4); // this P4

How is this a mistake?

computation that halts
a computation halts whenever it enters a final state (Linz:1990:234)

H1(P4,P4)==1
H4(P4,P4)==0

The actual steps of the actual computations conclusively proves that
the input to H4 never halts(Linz:1990:234) and the input to H1 halts.

Only independent computations halt. "inputs" do not. The input to *both*

The simulation of the input to H1(P4, P4) reaches it final state
proving that its input halts.

The simulation of the input to H4(P4, P4) never reaches it final state
proving that its input halts(Linz:1990:234).

main() { P4(P4); } halts
main() { P4(P4); }
         calls H4(P4,P4); simulates P4(P4); never halts(Linz:1990:234).

The simulation of P4(P4) is not the same thing as the actual computation P4(P4). A halt decider must answer about the *latter*, not the former.

This halt decider cannot possibly be incorrect on any of its aborted simulations:

The correct pure simulation of N steps of the input to H4(X,Y) by H4 is
always a correct halt deciding basis where X has reached its final state
or H4 has correctly detected that X would never reach its final state.

The simulation of the above N steps of P4(P4) by H is identical to the
direct execution of N steps of P4(P4).

computation that halts a computation halts whenever it enters a final
state (Linz:1990:234)

Page 4 of my paper conclusively proves that the actual execution trace
of H(P,P) does give P4 the criteria that is needs to correctly decide
that its simulated input never halts(Linz:1990:234).

Your simulation is not a true simulation since it can be aborted. An
aborted simulation doesn't reach its final state, but it also does not
run forever; therefore you cannot conclude based on this that the
computation being simulated doesn't halt anymore than you can conclude
that it does.

The ACTUAL computation main() {P4(P4);} is the ONLY computation that
matters when it comes to determining the halting status of P4(P4). And
that's what a halt decider, by definition, must answer about.

You don't understand the problem.

André

Halting problem undecidability and infinitely nested simulation V2 https://www.researchgate.net/publication/356105750_Halting_problem_undecidability_and_infinitely_nested_simulation_V2)



--
Copyright 2021 Pete Olcott

Talent hits a target no one else can hit;
Genius hits a target no one else can see.
Arthur Schopenhauer

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)