# 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 T_{1}= C_{11}typeargs_{11}... | C_{12}typeargs_{12}... | ... data T_{2}= C_{21}typeargs_{21}... | ... ...

(where every type argument is one of `T`

) holds values of types _{i}`T`

, _{1}`T`

, … in its registers and can use the following instructions:
_{2}

- Constructors:
`C`

._{ij}*rs*...*r**s*

Read values*xs*… from the registers*rs*… and place the value`C`

into the register_{ij}*xs*...*r*, then follow to the state*s*.

- Destructors/matchers:
`T`

. (Parentheses are only for convenience. One may call their contents_{i}*r*(*rs*_{1}...*s*_{1}) ... (*rs*_{m}...*s*_{m})*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 type`T`

.) Then in case it equals_{i}`C`

, place_{ij}*xs*...*xs*… into*different*registers*rs*_{j}and then follow to the state*s*_{j}.

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`

. Place 0 into*r**s**r*and proceed to*s*.`S`

. Take*r*_{1}*r**s**n*from*r*_{1}, place*n*+ 1 into*r*and proceed to*s*.`Nat`

. Take*r*Z(*s*_{Z}) S(*r*_{1}*s*_{S})*n*from*r*. If*n*= 0, proceed to*s*_{Z}. If*n*> 0, place*n*− 1 into*r*_{1}and proceed to*s*_{S}.`Nil`

. Place [] into*r**s**r*and proceed to*s*.`Cons`

. Take*r*_{1}*r*_{2}*r**s**n*from*r*_{1}, take*ns*from*r*_{2}, place*n*:*ns*into*r*and proceed to*s*.`List`

. Take*r*Nil(*s*_{Nil}) Cons(*r*_{1}*r*_{2}*s*_{Cons})*ns*from*r*. If*ns*= [], proceed to*s*_{Nil}. If*ns*=*n*:*nt*, place*n*into*r*_{1}, place*nt*into*r*_{2}, and proceed to*s*_{Cons}.

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