Sujet : Re: Proof that DDD specifies non-halting behavior --- point by point
De : F.Zwarts (at) *nospam* HetNet.nl (Fred. Zwarts)
Groupes : comp.theoryDate : 14. Aug 2024, 10:09:40
Autres entêtes
Organisation : A noiseless patient Spider
Message-ID : <v9hs8k$ccps$2@dont-email.me>
References : 1
User-Agent : Mozilla Thunderbird
Op 14.aug.2024 om 02:52 schreef olcott:
void DDD()
{
HHH(DDD);
return;
}
_DDD()
[00002172] 55 push ebp ; housekeeping
[00002173] 8bec mov ebp,esp ; housekeeping
[00002175] 6872210000 push 00002172 ; push DDD
[0000217a] e853f4ffff call 000015d2 ; call HHH(DDD)
[0000217f] 83c404 add esp,+04
[00002182] 5d pop ebp
[00002183] c3 ret
Size in bytes:(0018) [00002183]
Again the same joke? It seems you are short of memory.
A simulation of N instructions of DDD by HHH according to
the semantics of the x86 language is necessarily correct.
It is only a correct start of an incomplete simulation.
A correct simulation of N instructions of DDD by HHH is
sufficient to correctly predict the behavior of an unlimited
simulation.
It is not, since the semantics of the x86 language, used in the direct execution of the same input, shows that DDD halts.
It is clear that HHH aborts its own simulation one cycle to soon. The simulated HHH had only one cycle to go, when aborted. Therefore, the prediction of a non-halting behaviour is premature.
Termination analyzers / halt deciders are only required
to correctly predict the behavior of their inputs.
Exactly. And this is the same input that, when used in direct execution, halts.
Termination analyzers / halt deciders are only required
to correctly predict the behavior of their inputs, thus
the behavior of non-inputs is outside of their domain.
Indeed, so your dreams of a HHH that does not abort and does not halt, is a non-input and is outside the domain.