| Deutsch English Français Italiano |
|
<1851d842da2521669fdbc201a11119498b81979d@i2pn2.org> View for Bookmarking (what is this?) Look up another Usenet article |
Path: ...!news.misty.com!weretis.net!feeder9.news.weretis.net!news.nk.ca!rocksolid2!i2pn2.org!.POSTED!not-for-mail From: Richard Damon <richard@damon-family.org> Newsgroups: comp.theory Subject: Re: Incorrect requirements --- Computing the mapping from the input to HHH(DD) Date: Tue, 13 May 2025 18:45:06 -0400 Organization: i2pn2 (i2pn.org) Message-ID: <1851d842da2521669fdbc201a11119498b81979d@i2pn2.org> References: <vv97ft$3fg66$1@dont-email.me> <87msbmeo3b.fsf@nosuchdomain.example.com> <vvjcge$27753$2@dont-email.me> <vvjeqf$28555$1@dont-email.me> <vvjffg$28g5i$1@dont-email.me> <875xiaejzg.fsf@nosuchdomain.example.com> <vvjgt1$28g5i$5@dont-email.me> <87jz6qczja.fsf@nosuchdomain.example.com> <vvjotc$28g5i$12@dont-email.me> <vvnh9u$3hd96$1@raubtier-asyl.eternal-september.org> <vvno4e$3in62$2@dont-email.me> <vvo71c$rlt$1@news.muc.de> <PlNTP.270466$lZjd.128570@fx05.ams4> <vvochv$15td$2@news.muc.de> <vvodn5$3na6l$3@dont-email.me> <1276edeb9893085c59b02bbbd59fe2c64011736b@i2pn2.org> <vvqk4s$gldn$12@dont-email.me> <vvqln4$g8ck$5@dont-email.me> <vvrftj$ndkg$1@dont-email.me> <vvrima$nejb$3@dont-email.me> <vvua3t$1hm37$1@dont-email.me> <cd36dcf87daefa9ae472cc426d57704c2baa4292@i2pn2.org> <10000hl$1v330$1@dont-email.me> <1000c4g$21dtc$2@dont-email.me> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Wed, 14 May 2025 00:58:38 -0000 (UTC) Injection-Info: i2pn2.org; logging-data="251915"; mail-complaints-to="usenet@i2pn2.org"; posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg"; User-Agent: Mozilla Thunderbird X-Spam-Checker-Version: SpamAssassin 4.0.0 In-Reply-To: <1000c4g$21dtc$2@dont-email.me> Content-Language: en-US Bytes: 6678 Lines: 111 On 5/13/25 5:04 PM, olcott wrote: > On 5/13/2025 12:46 PM, Mike Terry wrote: >> On 13/05/2025 10:01, joes wrote: >>> Am Tue, 13 May 2025 03:17:32 +0100 schrieb Mike Terry: >>> >>>> When his HHH simulates DD, it spots a pattern in the simulation >>>> which PO >>>> calls his "infinite recursive simulation" pattern. PO believes that >>>> this pattern "specifies non halting behaviour" but it does not, as it >>>> can match for both halting and non-halting computations. Anyhow, PO >>>> has >>>> coded HHH to abort and return non-halting if it sees that pattern. He >>>> really really really believes that pattern "specifies non halting", >>>> despite observing with his own eyes DD halting when called directly! >>>> The rest of his arguments are just attempts to justify why HHH is >>>> "correct" to decide non-halting, despite DD halting. They generally >>>> amount to something like "during simulation my HHH detected non-halting >>>> behaviour, so it is correct to decide non-halting". >>> >>> Can you remind me how it matches halting computations? IIRC it looks >>> for invocations of the same function (across simulation levels, mind) >>> without conditional statements inbetween. Or is the impossibility of >>> recursive simulation the only reason for false positives? >>> >> >> Recursive simulation is not itself the problem. If we set aside some >> design errors like the use of mutable global data to communicate >> across simulation levels (making simulations follow a different code >> path to directly executed code), then in principle PO's x86utm could >> handle nested simulation in an ok way, at least for the purposes PO >> needs. His x86utm itself does cater for simulating a simulation of a >> simulation and so on, at the instruction level. >> > > Thanks for clearing that up. Everyone else > simply baselessly argued the opposite not > even knowing that they had no basis. Yes, x86utm does it right. Your decider do it wrong by turning on and off the trace, and mixing up traces at different levels of simulation, The "simulation" of the input should be ALWAYS the result of the outer level of simulation. It might include "notes", clearly marked, of the wider sematnic meaning of what the sequence of code performed, but the simulaiton is only the outer level simulation. > >> Your description of the matching process is pretty much right - I'll >> need to check in halt7.c ... >> >> Right, so the matching process goes like this: >> >> - simulated instructions (from all simulation levels) are added to a >> global trace table, but ONLY IF THEY ARE FROM DD, i.e. their address >> puts them physically inside C function DD. >> Trace entries from HHH and routines called from HHH are discarded. >> >> - when a call instruction is simulated the trace table is scanned >> backwards >> looking for a "matching" entry: that is, another call from the same >> address, and to the same target address. >> >> - if one is found, a check is made for whether there were any >> conditional >> branch instructions in the trace table between the matching calls >> [remember, the trace table only includes instructions inside C >> function DD] >> >> - if no conditional branches were encountered, the simulation is aborted >> with message "Infinite Recursion Detected Simulation Stopped\n\n", >> and the simulating HHH decides non-halting. >> >> - if no match is found, simulation continues as normal. >> > > That is all exactly correct. > >> The global trace table does not record the simulation level for an >> entry, so the matching process is agnostic when it comes to simulation >> levels. Also note there are many conditional branch instructions in >> HHH which would prevent matches occuring if we were to include HHH >> instructions in the examined trace! >> > > Yes that is true. The program-under-test is not the test-program. > When HHH is reporting on the behavior of the finite string of x86 > machine code specified by DD, HHH correctly reports that its input > DD cannot possibly reach its own final halt state. > > The input being decided by HHH(DD) includes DD > calling its own emulator in recursive simulation. > > The input being decided by HHH1(DD) DOES NOT INCLUDE > DD calling its own emulator in recursive simulation. > > Everyone here thinks that they can simply ignore > that entirely on the basis that this issue was never > raised in any textbooks. > >> For completeness, there is also a similar looking test relating to >> unconditional branches (jmp and the likes) aimed at detecting loops >> rather than recursion. This test does not match for input DD. >> >> >> Regards, >> Mike. >> > >