Re: Incorrect requirements --- Computing the mapping from the input to HHH(DD)

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.
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.
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!
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.