Switch from MM to MMA

[DmxLarchey]

This is a draft PR for switching from MM n to MMA n to put MMA upfront in place of MM.

The list of included reduction so far:

• BSM n halting to MMA (1+n) halting;
• MMA (1+n) halting to MMA (1+n) halting on zero (see remark below);
• MMA n halting to FRACTRAN (regular) halting
  • includes self-loops removal via the syntactic compiler;
  • with a bound on the jump address of the compiled program (as required by @yforster usage elsewhere in the library)
• wrote an alternate self-loops removal for MM n to MM (1+n) also using the syntactic compiler instead of the previous handwritten 1-1 compiler/linker.

Remark: notice than the reduction MMA 0 halting to MMA 0 halting on zero does not hold because the only program in MMA 0 is the empty list which stops immediately and thus cannot always be redirected to the zero state.

[DmxLarchey]

Apparently, we still need to avoid loops in MMA programs. We won't have integers in FRACTRAN programs by encoding MMA instructions but we could still forget about where the DEC instruction is situated which invites troubles:

i: DEC r i

would be encoded by the fractions 1/qs r ; ps (i+1)/ps i hence the reference to i disappears in the first fraction which is ps i / (ps i * qs r).

[DmxLarchey]

The previous commit fails because for the moment I have not decided how to remove self loops in MMA programs. Two options come to mind:

1. try to use the instruction compiler but ATM we miss critical syntactic information about the linked and compiled program;
2. compile every MMA instruction into 5 MMA instructions (uniform length for easy hand written compiler), avoiding the self loops. But, as was already the case for MM, we will have to show the correctness of the hand-written compiler by hand, which is a shame since we already have a correct instruction compiler.

For 1. above, we would need to add (to compiler_t) and establish syntactic properties of the linker and compiler but probably the interface will change since we would likely show equations such as (vulgarized here) if P = L++[i]++R then compiled P is compiled L ++ icomp i ++ compiled R, hence icomp would become a parameter of compiler_t.

[DmxLarchey]

So ideas to remember how to proceed for 1. above.

• define a compiler_synt_t spec that provides the syntactic property of the compiler, enough to implement the actual compiler_t spec, but also enough to capture the actual instructions which occur in the compiled code to be able to show that it is loop free.

• remember that the linker/compiler cannot be handled by local reasoning since these only have global syntactic properties. This means that the compiled code for a sub-program depends on where it is in the global program. Only its length is independent of where it is.

• so the syntactic spec above should express properties of sub-instructions, eg for linker := gc_link P start and Q := (start,gc_code P start);

  • the compiled code of a source instruction is sub-code of the compiled code: if (i,[ρ]) <sc P then (linker i,icomp linker i ρ) <sc Q;
  • if (i,[ρ]) <sc P then linker (1+i) = ilen ρ + linker i

  the above two are already hypotheses in the correctness proof, but we need also

  • each instruction of the compiled code belong to the compiled code of one instruction of the source code: if (j,[µ]) <sc Q then there is (i,[ρ]) <sc P such that (j,[µ]) <sc (linker i,icomp linker i ρ);
  • linker is monotonic, which probably is not true since PC values outside of P (either before or after) get mapped to the end of Q ATM, so the monotonicity property should only hold for PC values inside P : for i,j s.t. code_start P <= i <= j < code_end P we have linker i <= linker j;
  • are these enough to ensure that Q is loop free?

[mrhaandi]

Would it possibly help to have a slightly different compiler to FRACTRAN instead?
E.g. split each state MMA p into two and have a fractran transition p |-> p'.
So instead of p |-> q have p |-> q' |-> q.
A self loop in MMA would then be p |-> p' |-> p with no information loss.

[DmxLarchey]

Would it possibly help to have a slightly different compiler to FRACTRAN instead? E.g. split each state MMA p into two and have a fractran transition p |-> p'. So instead of p |-> q have p |-> q' |-> q. A self loop in MMA would then be p |-> p' |-> p with no information loss.

@mrhaandi ,yes indeed that was a possibility that we discussed early on with @yforster while proving H10, back in late 2018. I think/recall we decided at that time that it was conceptually simpler to stick with the original and simple encoding of Conway and insist that it only worked for self-loop free machines. Indeed, the only idea besides the Gödel coding is that of using the order of fractions to enforce that jumping on a zero counter occurs only when -1 cannot be performed.

This legacy choice also allowed pointing out that notion of self-loop, and split the work in half.

The alternate option you point out, splitting FRACTRAN instructions in half instead and introducing a third idea, displaces the complications into the proof of correctness of the FRACTRAN compiler, but I agree that this is a possibility.

The legacy idea to remove self-loops for MM was to jump to a length 2 cycle since self-loops are zombifying for MM programs. So i: DEC x i is replaced with i: DEC z l2 where z is a fresh and always zero register and l2 is a length 2 cycle looping forever (but free of self-loops), like l2: [ DEC z (l2+1) ; DEC z l2 ]. Hence a one-to-one replacement of MM instructions which gives a trivial linker, greatly simplifying the compiler.

However, for MMA, a self-loop i: DECₐ x i eventually zeroes the register x and then moves on to i+1 (so is semantically equivalent to a would be i: ZEROₐ x).

The idea is then to replace any DECₐ instruction (not just self loops) i: DECₐ x j with

lnk i: [ DECₐ x (3+lnk i) ; INCₐ x ; DECₐ x (5+lnk i) ; INCₐ x ; DECₐ x (lnk j) ]

which has no self-loop but for this we need to show that lnk j is not the same as 4+lnk i. Hence we need syntactic properties of the compiled code which hold in the actual generic compiler, but are not currently available through a well-designed interface.

[DmxLarchey]

Now it remains to establish that the compiler_syntactic interface is enough:

1. to prove that the produced code is self-loop free;
2. to build the compiler_t interface.

[DmxLarchey]

Reminder: do not forget to modify the concrete compilers because now, one needs to establish that instructions are always compiled into at least one instruction in the target language. This property is harmless, trivial to prove and always holds in the current compilers, but the corresponding code proving it should be added.

After considering the pros and cons, even if that "at least length 1 property" can be derived from the other syntactic property and a semantic one, this mixes syntactic and semantic conditions and somehow blocks the separation between the syntactic properties and the semantic properties of the generic compiler.

[DmxLarchey]

Completed the direct reduction from MMA n halting to FRACTRAN (REG) halting.

[mrhaandi]

FYI, I am currently writing an MMA which evaluates a closed L term such that, if the result is an encoded natural number, then this number is extracted into a register. MMAs are really good for this.
The hope is to remove the heavy TM machinery from the proof of L_computable -> TM_computable.
Also, it would be easy to have an MMA_computable -> TM_computable proof, after all MMA is just a variant of a read-only TM; @yforster maybe you would like to help me with this part?

[mrhaandi]

The hope is to remove the heavy TM machinery from the proof of L_computable -> TM_computable.

(FYI) I have now written fast, compact, alternative proofs of L_computable -> MMA_computable and MMA_computable -> TM_computable.
This will make MMA take an even more prominent role (currently working on PR and cleanups).

[DmxLarchey]

The hope is to remove the heavy TM machinery from the proof of L_computable -> TM_computable.

(FYI) I have now written fast, compact, alternative proofs of L_computable -> MMA_computable and MMA_computable -> TM_computable. This will make MMA take an even more prominent role (currently working on PR and cleanups).

@mrhaandi Does this comprises the input-output relation as well as the termination predicate ?

[mrhaandi]

@mrhaandi Does this comprises the input-output relation as well as the termination predicate ?

It follows exactly the definitions of @yforster, so it is about the input/output relations on natural number encodings.
It will be part of the computational equivalence cycle: Models_Equivalent.v and also replace a lot of complexity theoretic machinery, which is not needed for computational equivalence.