Generalized Minsky machine
Generalized Minsky machine (GMM for short) is a generalization of Minsky machine conceived (at the least) by User:arseniiv in 2019. In this machine, registers can hold values of (a predefined set of) algebraic types, not just natural numbers.
A GMM corresponding to type definitions
data T1 = C11 typeargs11... | C12 typeargs12... | ... data T2 = C21 typeargs21... | ... ...
(where every type argument is one of Ti) holds values of types T1, T2, … in its registers and can use the following instructions:
- Constructors:
Cij rs... r s.
Read values xs… from the registers rs… and place the valueCij xs...into the register r, then follow to the state s.
- Destructors/matchers:
Ti r (rs1... s1) ... (rsm... sm). (Parentheses are only for convenience. One may call their contents match cases. In case constructors of the types aren’t ordered by default, one can mark these groups with their names; this is also more readable, though less laconic.)
Read the value x from r (it should be of typeTi.) Then in case it equalsCij xs..., place xs… into different registers rsj and then follow to the state sj.
Constructors generalize INC (and CLR which is not usually treated as a primitive), and destructors generalize JZDEC.
There are several approaches for deciding fine details of the semantics not specified above:
- Each register is declared a static type. Only instructions which conform to these declarations are deemed correct and can be used in a machine. As a result, each register can hold only values of the corresponding type, ever. Registers in each match case are statically checked to be distinct, too. This is what User:arseniiv prefers.
- Alternatively, when the type of the value present in the register is not the expected one to read by an instruction, the result is undefined behavior. Also, if one doesn’t want to enforce that the registers in a match case are different, the situation where they aren’t, may be also declared undefined behavior.
Orthogonal to that, there are still unspecified details on handling uninitialized registers. (As types in this setting may have no single natural nullary constructor like ℕ does, we can’t initialize all non-input registers with a default “zero” like in the case of Minsky machines.) So, one may declare reading from a yet-to-be-written non-input register an undefined behavior again. Or one may extend the machine’s definition with initialization expressions for every non-input register.
Examples
For
data Nat = Z | S Nat data List = Nil | Cons Nat List
one will have the following instructions:
Z r s. Place 0 into r and proceed to s.S r1 r s. Take n from r1, place n + 1 into r and proceed to s.Nat r Z(sZ) S(r1 sS). Take n from r. If n = 0, proceed to sZ. If n > 0, place n − 1 into r1 and proceed to sS.Nil r s. Place [] into r and proceed to s.Cons r1 r2 r s. Take n from r1, take ns from r2, place n : ns into r and proceed to s.List r Nil(sNil) Cons(r1 r2 sCons). Take ns from r. If ns = [], proceed to sNil. If ns = n : nt, place n into r1, place nt into r2, and proceed to sCons.
Power
For some type universes, like {Nat, List} above, or just {Nat}, GMMs are obviously Turing-complete: we can easily translate a plain old Minsky machine into one of these as they have Nat.
For other type universes, like those consisting entirely of enums, GMMs are extremely weak: in these cases they allow to implement only functions from a finite set to a finite set, by construction.
Is the universe having infinitely many values equivalent for the corresponding GMM to be TC? Most probably yes, but User:arseniiv have yet to write a rigorous proof. (At least one of the types should then be infinite, and we should be able to treat it like Nat, but mutual recursion in type definitions seems to be tricky case to cover, at least.)
Update 2020-07-02: yes yes it is so. There are in fact constructive algorithm to trim uninhabitable constructors (and uninhabited types), and to construct an isomorphism with Nat when the universe is infinite.