XPost: comp.theory, sci.logic
On 10/24/2021 12:37 PM, Richard Damon wrote:
On 10/24/21 10:04 AM, olcott wrote:
On 10/24/2021 5:40 AM, Richard Damon wrote:
On 10/23/21 11:29 PM, olcott wrote:
On 10/23/2021 10:19 PM, Richard Damon wrote:
On 10/23/21 10:16 PM, olcott wrote:
On 10/23/2021 8:49 PM, Richard Damon wrote:
On 10/23/21 9:27 PM, olcott wrote:
In order to make my halt decider a pure function it had to have >>>>>>>> a way to look at the inputs to function calls. In order to look >>>>>>>> at the inputs to function calls it had to know how many inputs >>>>>>>> that a function has.
This is DFA analyzes C source code to provide the number of
parameters of each function in the file. The number of
parameters per function is the number of {vt} matches per {fn} >>>>>>>> match.
The only thing that will change with this file is that the halt >>>>>>>> decider will use different halt deciding criteria so that the
halt decider becomes a pure function.
https://www.researchgate.net/publication/351947980_Halting_problem_undecidability_and_infinitely_nested_simulation
In computer programming, a pure function is a function that has >>>>>>>> the following properties:[1][2]
(1) The function return values are identical for identical
arguments (no variation with local static variables, non-local >>>>>>>> variables, mutable reference arguments or input streams).
(2) The function application has no side effects (no mutation of >>>>>>>> local static variables, non-local variables, mutable reference >>>>>>>> arguments or input/output streams).
https://en.wikipedia.org/wiki/Pure_function
//
// Deterministic Finite Automaton (DFA) recognizer
// of C function headers.
// Character Classes
//
EMPTY [0]
ALPHA [ABCDEFGHIJKLMNOPQRSTUVWXYZ_abcdefghijklmnopqrstuvwxyz] >>>>>>>> NUMERIC [0123456789]
WS [0x09,0x0A,0x0D,0x20]
LPAREN [(]
RPAREN [)]
ASTERISK [*]
COMMA [,]
COMMENT [0x2f]
NEWLINE [0x0A]
ASCII [0x20-0x7e]
CONTROL [0x00-0x09,0x0b-0x1f,0x7f]
// Recognized Patterns
//
{et} Empty
{ft} Function_Type
{fn} Function_Name
{vt} Variable_Type
{vn} Variable_Name
{fh} Function_Header
// DFA Definition to recognize C function headers
// begin of function type
<00> WS (00) ALPHA(01) NUMERIC(00) [*](00) [/](12)
<01> WS{ft}(03) ALPHA(01) NUMERIC(01) [*](02)
<02> WS{ft}(03) ALPHA(00) NUMERIC(00) [*](02)
// begin of function name
<03> WS (03) ALPHA(04) NUMERIC(00) [*](00)
<04> WS{fn}(05) ALPHA(04) NUMERIC(04) [*](00) [(]{fn}(06)
<05> WS (05) ALPHA(00) NUMERIC(00) [*](00) [(] (06) >>>>>>>>
// begin of variable type
<06> WS (06) ALPHA(07) NUMERIC(00) [*](00) [)]{fh}(00)
<07> WS{vt}(09) ALPHA(07) NUMERIC(07) [*](08) [)]{fh}(00)
<08> WS{vt}(09) ALPHA(00) NUMERIC(00) [*](08)
// begin of variable name
<09> WS (09) ALPHA(10) NUMERIC(00) [*] (00)
<10> WS{vn}(11) ALPHA(10) NUMERIC(10) [,]{vn}(06) [)]{vn}(00)
<11> WS (11) ALPHA(00) NUMERIC(00) [,] (06) [)] (00) >>>>>>>>
// ignores all "//" comments
<12> WS (00) ALPHA(01) NUMERIC(00) [*](00) [/](13)
<13> CONTROL(13) ASCII(13) [0x0A] (00)
Ok,
Just remember that being a 'Pure Funciton' isn't the actual
requirement, the decider needs to be a Mathematical Computation, >>>>>>> which means that all copies of it, when given the same inputs,
generates the same outputs.
You STILL have the error that you treat H as a 'pure simulator'
when it is not, it is only a 'pure simulatior until' and as such, >>>>>>> the behavior of the copy of H in H^ DOES have an affect on the
behavior of that H^. Remember, a 'Pure Simulator' (aka a UTM)
NEVER stops simulating until the machine it is simulating ends,
even if that takes forever.
void Infinite_Loop()
{
HERE: goto HERE;
}
_Infinite_Loop()
[00000ab0](01) 55 push ebp
[00000ab1](02) 8bec mov ebp,esp
[00000ab3](02) ebfe jmp 00000ab3
[00000ab5](01) 5d pop ebp
[00000ab6](01) c3 ret
Size in bytes:(0007) [00000ab6]
Are you saying that the only way that a simulating halt decider
can correctly decide that the above code will never stop running
is to wait until the end of time?
No. You seem to have a reading comprension problem.
The Simulating Halt Decider is fully allowed to abort the
simulation of the machine it is simulationg.
The only issue is that IF it does so, it can't treat itself as if
it was a UTM/Pure SImulator, and thus the fact that it never saw
the comptation reach a halting state isn't proof of anything.
When a simulating halt decider acts as if it is a pure simulator and
watches the behavior of an infinite loop it can correctly abort the
simulation of this input and report that this input never halts. We
can generalize this simplest case of infinite execution to all other
cases:
All that I am doing is generalizing this same idea. When-so-ever a
simulating halt decider can correctly axiomatically determine that
its input would never halt if it remained a pure simulator then it
can abort the simulation of this input and report that this input
never halts.
When a simulating halt decider correctly axiomatically determines X
then we know that X is necessarily true.
NO!
You are making an INCORRECT generalization.
When-so-ever X is correct about Y then X is not incorrect about Y is
always true.
And if X is not correct about all Y then X is not correct for all Y.
Y is a specific unique instance.
Just because some statement happens to be correct in one case does not
make it correct in all cases.
Just because some statement is correct in one case conclusively proves
that this statement is not incorrect in all cases.
It might be, but that generalization needs
to be PROVEN to be used.
FAIL.
Examples NEVER, by themselves prove a generality.
One single counter-example does correctly refute a general statement.
Linz claims that no H can correctly decide the halt status of ⟨Ĥ⟩ ⟨Ĥ⟩ thus a single H that does correctly decide the halt status of ⟨Ĥ⟩ ⟨Ĥ⟩ refutes Linz.
An example can prove
existance, but not that it is true for all cases.
t is just like claiming that log(a+b+c) is log(a) + log(b) + log(c)
because we have the case that log(1+2+3) = log(1) + log(2) + log(3).
You have made a claim, PROVE IT. Not just a rhetorical argument done
with vague words, but an honest to god actual analytical proof, using
the exact same accepted definitions of all the words. And then go and
prove that setup does meet the conditions required by the proof to
use it.
You say 'axiomatically', but that is just YOUR DISHONEST DOGDE to
insert in a statement that is FALSE.
Now, part of the problem is that you make a number of small errors
that you continue to just ignore and these build up to your false
conclusion.
Your statement would be correct if pronoun usage was correct and the
usage refered to just this one COPY being adjusted, and not the
shared copy being changed, which causes the change to change the
supposed to be fixed algorithm employed by the input being simulated.
We know that for THAT case, H is incorrect, as using an ACTUAL 'Pure
Simulator' to process this input (where H^ still uses the original H
that does abort) shows that H^ WILL HALT, and thus the claim "would
not halt unless H aborts the simulation" is incorrect.
_Infinite_Loop()
[00000ab0](01) 55 push ebp
[00000ab1](02) 8bec mov ebp,esp
[00000ab3](02) ebfe jmp 00000ab3
[00000ab5](01) 5d pop ebp
[00000ab6](01) c3 ret
Size in bytes:(0007) [00000ab6]
It is always the same process. H simulates its input until it
determines that its input would never halt.
Here is what the above simulation looks like:
[00000ab0](01) 55 push ebp
[00000ab1](02) 8bec mov ebp,esp
[00000ab3](02) ebfe jmp 00000ab3
[00000ab3](02) ebfe jmp 00000ab3
[00000ab3](02) ebfe jmp 00000ab3
[00000ab3](02) ebfe jmp 00000ab3
[00000ab3](02) ebfe jmp 00000ab3
[00000ab3](02) ebfe jmp 00000ab3
[00000ab3](02) ebfe jmp 00000ab3
[00000ab3](02) ebfe jmp 00000ab3
[00000ab3](02) ebfe jmp 00000ab3
[00000ab3](02) ebfe jmp 00000ab3
[00000ab3](02) ebfe jmp 00000ab3
[00000ab3](02) ebfe jmp 00000ab3
Can you understand in this simplest possible case that the above is a
non halting behavior pattern?
You keep using this strawman.
I have never said that a simulating halting decider can't abort a
simulation or be able to decide on these simple cases.
Then we can proceed step-by-step increasing the difficulty by minimal increments until we get to H(P,P). The correct halt status of H(P,P) is
based on the correct halt status of infinite recursion.
The problem is that you use a BAD PATTERN to determine that H^ is non-halting. You use a pattern based on UNSOUND logic that gives
incorrect answers for some cases.
If it is true that the infinite simulation of the input to H(P,P) never
reaches its final state then when H stops simulating this input and
reports that this input never halts we know that H has correctly decided
the halt status of its input by semantic tautology.
Even when H aborts the simulation of this input this does not count as
halting because P never reaches its final state.
A simpler version of this same semantic tautology:
If H correctly decides that its input never halts then H is not incorrect.
The simplest version of this same semantic tautology:
If H is correct then H is not incorrect.
--
Copyright 2021 Pete Olcott
"Great spirits have always encountered violent opposition from mediocre
minds." Einstein
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)