Superfluous Minsky Machine Models

[mrhaandi]

We currently have

• MM 2 two-counter Minsky machines
• MM2 two-counter (alternative) Minsky machines
• MMA 2 two-counter (alternative) Minsky machines
• CM2 two-counter (alternative) Minsky machines

Much of the above is redundant, including infrastructure and proofs.

My personal preference is to get rid of MM 2 and CM2.
The roles of remaining of MM2 (easy to reduce from) and MMA n (easy to reduce to) are justified.

[DmxLarchey]

Hi @mrhaandi,

What is MM 2 ? Is this the instance of MM nwith n := 2? Because I do not see it anywhere in the code. Removing the general MM n would be more problematic because it described and used in the CPP'19 paper. CM2 derives from MM2 which itself derives from MMA 2 (in terms of reductions).

[mrhaandi]

What is MM 2 ? Is this the instance of MM n with n := 2?

Yes.

problematic because it described and used in the CPP'19 paper.

Isn't it linked to the specific tag/branch? If so, then the paper remains correct.

[DmxLarchey]

@mrhaandi Do you suggest completely suppressing the semantics of MM where the conditional jump occurs on the 0 case (as opposed to the 1+n case) ?

[mrhaandi]

Do you suggest completely suppressing the semantics of MM where the conditional jump occurs on the 0 case (as opposed to the 1+n case) ?

Yes. Currently, I see no benefit (besides pointing out decidability of the two counter case) of this model.
Minsky himself confusingly states that two counters suffice for universality of some not precisely stated model, which then is not exactly MM 2.
Working with students and explaining the library to other people the overall issue led to quite some confusion.

[mrhaandi]

Also, I am looking to fully replace CM2 by MM2 in proofs, to logically deduplicate the library.

[mrhaandi]

Also, I am looking to fully replace CM2 by MM2 in proofs, to logically deduplicate the library.

I put in the effort to replace CM2 by MM2 in reductions (for negative results such as semi-unification). The only annoyance is that instruction counting starts from 1 and not 0, so there are more cases than before.

Interestingly, it is not straightforward to formulate uniform mortality for MM2 because there is no notion of a number of steps until termination.

[DmxLarchey]

Yes. Currently, I see no benefit (besides pointing out decidability of the two counter case) of this model.

Well I do find very interesting the subtlety that a slight semantic change impacts the number of registers needed for undec. And the decidability proof for MM 2 you did implement is far from trivial. However, I do agree that MM n should perhaps not be put upfront and that MMA n would be better suited.

Here are the places where MM n is used that I know of because I did contribute to them:

1. a BSM to MM reduction (CPP 19);
2. removal of self-loops in MM (FSCD 19);
3. a reduction from self-loop free MM to FRACTRAN (FSCD 2019, that one initially by @yforster);
4. a compiler from MuRec to MMe (which is like MM n but with nat indexed registers instead of Fin n indexed ones);
5. a compressor from MMe to MM n (fom some n).

Also @yforster did modify the upfront semantic presentation on MM n in MinskyMachines/MM.v so I guess he did that for a use case but I do not immediately remember which one.

Here is my assessment on switching from MM n to MMA n in all of those:

• I suspect 1 to be easy but perhaps a bit long;
• 2 might not be needed for MMA because they do not contain self loops;
• 3 could be easy as well.
• 4 might be longer: that compiler was a PITA from my recollection.
• I guess 5 would be easy. I just consists in computing a global bound m on the number of used nat indexed registers and projecting them injectively on Fin m.

Minsky himself confusingly states that two counters suffice for universality of some not precisely stated model, which then is not exactly MM 2. Working with students and explaining the library to other people the overall issue led to quite some confusion.

I agree it can be confusing but it is also interesting (see above). @mrhaandi do you agree on keeping MM n (maybe renaming it?) by putting MMA n upfront in place of MM n?

I would like the input of @yforster on this issue since it may impact some of his code as well.

[yforster]

I agree it can be confusing but it is also interesting (see above). @mrhaandi do you agree on keeping MM n (maybe renaming it?) by putting MMA n upfront in place of MM n?

I think it makes sense to let MMA be the central, exposed notion (maybe renamed into something entirely new like MCM (Minsky Counter Machines, unfortunately just CM is already taken), but keep MM internally to ease proofs. We don't want to delete it entirely, otherwise we can't keep Andrej's surprising MM 2 decidability proof around.

The only reason I changed MinskyMachines/MM.v was to align its semantics with the other central models, via a big-step evaluation relation. The sss framework is still used a lot, but reviewers don't have to understand it and can survey a more or less standalone definition, which is equivalent to the sss semantics.

[mrhaandi]

I think it makes sense to let MMA be the central, exposed notion (maybe renamed into something entirely new like MCM (Minsky Counter Machines, unfortunately just CM is already taken), but keep MM internally to ease proofs. We don't want to delete it entirely, otherwise we can't keep Andrej's surprising MM 2 decidability proof around.

I currently work on replacing CM entirely by MMA 2, so potentially the name will be free starting from 8.16.
Already, there is a self-contained
https://github.com/uds-psl/coq-library-undecidability/blob/coq-8.15/theories/MinskyMachines/Deciders/MPM2_HALT_dec.v
I use MPM for Minsky's Program Machines explicitly to refer to the exact book definition, which has the instruction set

Inductive Instruction : Set :=
  | halt : Instruction
  | zero : bool -> Instruction
  | inc : bool -> Instruction
  | dec : bool -> nat -> Instruction.

So maybe making MPM2_dec a top-level thing is good to have the important observation and for future reference in papers.

[DmxLarchey]

I did open up the draft PR #161 to see where replacing MM with MMA leads us.

[mrhaandi]

I now fully replaced CM2 by MM2 in negative and positive results. Since there is a recent paper Certified Decision Procedures for Two-Counter Machines which points to the 8.15 branch, I will wait with a PR for 8.16. The changes currently reside in less-CM2.

[mrhaandi]

PR #169 now completely replaces CM2 by MM2.

[DmxLarchey]

In draft PR #161, removing self-loops from MMA programs is still required, but for more subtle reasons than was the case for MM where self-loops rendered the corresponding FRACTRAN program always non-terminating. In case of MMA, this is not the case anymore but still, a MMA self-loop naively compîled to FRACTRAN produce instructions/fractions that forget about their location in the source code, and hence might preempt instructions from other locations.

The removal of self-loops from MMA is simple in principle and would ideally be obtained using the generic compiler, avoiding reproducing a correctness proof of the compiled code. Unfortunately, this is how it was done for with MM where the compiler removing self-loops was simpler (one instruction replaced by one instruction, hence a trivial linker).

As a consequence, the following issue with the generic compiler did not occur to me:

• the generic compiler gathers enough semantic information for correctness;
• but ATM, we do not gather enough syntactic information about the compiled code to be able to show that it is free of self-loops.

TBC

[DmxLarchey]

PR #169 now completely replaces CM2 by MM2.

#169 does not seem to pass the CI at the moment. Also, I am unable to comment there. No idea why.

[DmxLarchey]

I did complete the self-loops removal for MMA using the syntactic compiler and the MMA n to FRACTRAN reduction in draft PR #161. Missing so far:

• the MuRec to MMAe compiler where registers are indexed by nat instead of pos n/Fin.t n;
• and the corresponding compressor (a priori easy to transfer).
• MM to FRACTRAN compiler was also used by @yforster to implement more subtle reductions that required extra properties which I did not transfer so far (eg bounds on the space of PC values).