Deutsch English Français Italiano |
<b1b9dd419864b78ebd86da1bc1f53bc655340966@i2pn2.org> View for Bookmarking (what is this?) Look up another Usenet article |
Path: ...!weretis.net!feeder9.news.weretis.net!i2pn.org!i2pn2.org!.POSTED!not-for-mail From: Richard Damon <richard@damon-family.org> Newsgroups: comp.theory Subject: Re: Overview of proof that the input to HHH(DDD) specifies non-halting behavior Date: Tue, 13 Aug 2024 22:31:01 -0400 Organization: i2pn2 (i2pn.org) Message-ID: <b1b9dd419864b78ebd86da1bc1f53bc655340966@i2pn2.org> References: <v9edol$3metk$1@dont-email.me> <v9fuim$3uffi$2@dont-email.me> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Wed, 14 Aug 2024 02:31:01 -0000 (UTC) Injection-Info: i2pn2.org; logging-data="2494910"; mail-complaints-to="usenet@i2pn2.org"; posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg"; User-Agent: Mozilla Thunderbird Content-Language: en-US In-Reply-To: <v9fuim$3uffi$2@dont-email.me> X-Spam-Checker-Version: SpamAssassin 4.0.0 Bytes: 4554 Lines: 84 On 8/13/24 11:36 AM, olcott wrote: > On 8/12/2024 8:43 PM, olcott wrote: >> We prove that the simulation is correct. >> Then we prove that this simulation cannot possibly >> reach its final halt state / ever stop running without being aborted. >> The semantics of the x86 language conclusive proves this is true. >> >> Thus when we measure the behavior specified by this finite >> string by DDD correctly simulated/emulated by HHH it specifies >> non-halting behavior. >> >> https://www.researchgate.net/ >> publication/369971402_Simulating_Termination_Analyzer_H_is_Not_Fooled_by_Pathological_Input_D >> > > *ESSENCE OF PROOF OF KEY POINTS* > A simulation of N instructions of DDD by HHH according to > the semantics of the x86 language is stipulated to be correct. Not a valid stipulation, you can not stipulate something to be "correct". If you mean to stipulate a MEANING for corect, then you just locked your self out of using "correct" in the normal meaning, and thus locked you self out of proving anything. Using your "stipulation" of correct, to mean that you are stipulating what will be considered to be a "Correct Simulation" for your previous statement, that make that statement FALSE, because ANY DDD that calls an HHH that will simulate for just N instructions and then return will be HALTING by simple inspection. Yes, the simulation doesn't reach the final state, but partial simulation don't show what happens as a final state of the machine (or if it reaches on). You keep repeating this error, proving that you seem to have a learning disability that prevents you from understanding the true meaning of words. If you want to change your statement to be an actruism, then you need to say something like: "It is true that no partial or complete correct simulaiton of DDD by HHH will ever reach the return instruction of DDD". The key is you need simulation, not DDD to be the subject of the verb reach, so that is what you are actually talking about, and what reaches (or not) the final state. > > A correct simulation of N instructions of DDD by HHH is > sufficient to correctly predict the behavior of an unlimited > simulation. Nope, proven incorrect, as the unlimited simulation of the DDD that calls the HHH that does the partial simulation, and then returns, will see that DDD call the HHH and then the HHH will simulate those N instructions and then returns to the DDD and DDD then reaches it final state. > > Termination analyzers / halt deciders are only required > to correctly predict the behavior of their inputs. Which *IS* the behavior of the program the input represents, BY DEFINITION OF A HALT DECIDER. Also, that means HHH must consider the HHH that DDD calls to be the actual HHH which is there, which is itself, and it can not argue that if it didn't abort, the simulation would go on, as if HHH aobrts, so does the one that DDD calls, and thus that DDD is halting. > > 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. > Which *IS* the behavior of the program the input represents, BY DEFINITION OF A HALT DECIDER. Also, that means HHH must consider the HHH that DDD calls to be the actual HHH which is there, which is itself, and it can not argue that if it didn't abort, the simulation would go on, as if HHH aobrts, so does the one that DDD calls, and thus that DDD is halting.