Sujet : Re: This function proves that only the outermost HHH examines the execution trace
De : mikko.levanto (at) *nospam* iki.fi (Mikko)
Groupes : comp.theoryDate : 28. Jul 2024, 10:23:13
Autres entêtes
Organisation : -
Message-ID : <v852m1$3sfas$1@dont-email.me>
References : 1 2 3 4 5 6 7
User-Agent : Unison/2.2
On 2024-07-27 18:20:19 +0000, olcott said:
On 7/27/2024 1:14 PM, Alan Mackenzie wrote:
olcott <polcott333@gmail.com> wrote:
Stopping running is not the same as halting.
DDD emulated by HHH stops running when its emulation has been aborted.
This is not the same as reaching its ret instruction and terminating
normally (AKA halting).
I think you're wrong, here. All your C programs are a stand in for
turing machines. A turing machine is either running or halted. There is
no third state "aborted".
Until you take the conventional ideas of
(a) UTM
(b) TM Description
(c) Decider
and combine them together to become a simulating partial halt decider.
You also need the conventional ideas of halting and halt decider.
The latter is largely a combination of the conventional ideas of
decider and halting but also involves the conventional of
prediction, so you need that, too.
Although the conventional idea of testing is not relevant to the construction
of a simulating partial halt decider it is helpful to presentation of the
result, especially if your target audience contains software engineers. If
your target audience is mainly mathematicians the convnetional idea of proofs
is more useful because in that case most of your presentation must be proofs.
-- Mikko