Liste des Groupes | Revenir à c theory |
On 5/7/2024 6:18 AM, Richard Damon wrote:Ok, and I can make an H that simulates its D to the final state.On 5/7/24 3:30 AM, Mikko wrote:This template defines an infinite set of finite string H/D pairs where each D(D) that is simulated by H(D,D) also calls this same H(D,D).On 2024-05-06 18:28:37 +0000, olcott said:>
>On 5/6/2024 11:19 AM, Mikko wrote:>On 2024-05-05 17:02:25 +0000, olcott said:>
>The x86utm operating system: https://github.com/plolcott/x86utm enables>
one C function to execute another C function in debug step mode.
Simulating Termination analyzer H simulates the x86 machine code of its
input (using libx86emu) in debug step mode until it correctly matches a
correct non-halting behavior pattern proving that its input will never
stop running unless aborted.
>
Can D correctly simulated by H terminate normally?
00 int H(ptr x, ptr x) // ptr is pointer to int function
01 int D(ptr x)
02 {
03 int Halt_Status = H(x, x);
04 if (Halt_Status)
05 HERE: goto HERE;
06 return Halt_Status;
07 }
08
09 int main()
10 {
11 H(D,D);
12 }
>
*Execution Trace*
Line 11: main() invokes H(D,D);
>
*keeps repeating* (unless aborted)
Line 03: simulated D(D) invokes simulated H(D,D) that simulates D(D)
>
*Simulation invariant*
D correctly simulated by H cannot possibly reach past its own line 03.
>
The above execution trace proves that (for every H/D pair of the
infinite set of H/D pairs) each D(D) simulated by the H that this D(D)
calls cannot possibly reach past its own line 03.
When you say "every H/D pair" you should specify which set of pairs
you are talking about. As you don't, your words don't mean anything.
>
Every H/D pair in the universe where D(D) is simulated by the
same H(D,D) that D(D) calls. This involves 1 to ∞ steps of D
and also includes zero to ∞ recursive simulations where H
H simulates itself simulating D(D).
"In the universe" is not a set. In typical set theories like ZFC there
is no universal set.
These H/D pairs can be enumerated by the one to ∞ simulated steps of D and involve zero to ∞ recursive simulations of H simulating itself simulating D(D). Every time Lines 1,2,3 are simulated again defines
one more level of recursive simulation.
1st element of H/D pairs 1 step of D is simulated by H
2nd element of H/D pairs 2 steps of D are simulated by H
3rd element of H/D pairs 3 steps of D are simulated by H
4th element of H/D pairs 4 steps of D are simulated by H
this begins the first recursive simulation at line 01
5th element of H/D pairs 5 steps of D are simulated by
next step of the first recursive simulation at line 02
6th element of H/D pairs 6 steps of D are simulated by
last step of the first recursive simulation at line 03
7th element of H/D pairs 7 steps of D are simulated by H
this begins the second recursive simulation at line 01
Can D correctly simulated by H terminate normally?Wrong, I showed two different ways to build an H that will do that.
00 int H(ptr x, ptr x) // ptr is pointer to int function
01 int D(ptr x)
02 {
03 int Halt_Status = H(x, x);
04 if (Halt_Status)
05 HERE: goto HERE;
06 return Halt_Status;
07 }
08
09 int main()
10 {
11 H(D,D);
12 }
*Execution Trace*
Line 11: main() invokes H(D,D);
*keeps repeating* (unless aborted)
Line 01
Line 02
Line 03: simulated D(D) invokes simulated H(D,D) that simulates D(D)
*Simulation invariant*
D correctly simulated by H cannot possibly reach past its own line 03.
The key thing to note is that no D simulated by any H ever reaches
its own line 06 and halts. This means that the input to H(D,D) is
ALWAYS non-halting.
>
No, it shows that he is just thinking of Nieve set theory, you know, the one that was proven broken.
>>>
Usually the best way to introduce a set of pairs is that first two
sets are specified and then a rule that selects some pairs from
the Cartesian product of those two sets.
>
In the current case the first set could be the set programs that
take two input values (possibly of some specific type) and returns
a Boolean value, and the second set could be programs that take
one input value (of the same type as the programs in the first set).
Or whatever best serves your purposes.
>
Les messages affichés proviennent d'usenet.