Обобщённая машина Минского

[arseniiv]

Машиной (обычной) Минского обычно называют регистровую машину, у которой в регистрах натуральные числа (включая ноль) и две команды — $\operatorname{INC} r\, s$ (инкрементировать значение в $r$ и перейти в состояние $s$) и $\operatorname{JZDEC} r\, s_0 \, s_>$ (попробовать декрементировать значение в $r$, и если это был ноль (и не вышло), перейти в $s_0$, а если вышло, перейти в $s_>$).

По-моему это очень удобный формализм вычислимости, разве что он требует, чтобы мы приняли, что регистр может содержать неограниченные значения; лента машины Тьюринга многим кажется более приземлённой. Ещё кто-то может быть недоволен, что вычислимость сама по себе никак с натуральными числами не связана, и потому якобы ММ — и к примеру рекурсивные функции — хуже, хотя легко представить себе обобщение как ММ, так и рекурсивных функций на любое множество алгебраических типов. Я себе выписывал и то, и то, и это было довольно поучительным опытом (например оператор μ-рекурсии не обобщается натуральным образом, но можно на замену ему предложить куда более гибкий — если мы рассматриваем произвольную кучку типов — оператор поиска в произвольной последовательности $f(a), f(g(a)), f(g(g(a))), \ldots$ произвольного значения).

Сейчас я опишу, до какого определения обобщённой ММ дошёл, а вопрос темы в том, видели ли вы его уже в литературе и как такая машина там называлась. Скорее всего к нему уже давно пришли, просто я не видел, и хотелось бы знать более общеупотребительное название.

Сначала я в точности определю, что здесь понимается под алгебраическими типами, а точнее под отдельным небольшим самодостаточным «миром» алгебраических типов. Он задаётся множествами $L$ названий типов и $C$ конструкторов, сюръекцией $r\colon C\to L$, задающей тип результата конструктора, и функцией $a\colon C\to L^*$, задающей типы аргументов конструктора. Коротко это всё можно записать в виде набора определений вида

$$l_i ::= \ldots\mid c_{ij}\, a(c_{ij}) \mid\ldots,$$

где $r(c_{ij}) = l_i$, например,

$$\begin{aligned} \mathbb N & ::= \mathsf z \mid \mathsf s\,\mathbb N \\ \mathsf{List}_{\mathbb N} & ::= \mathsf{nil} \mid \mathsf{cons}(\mathbb N, \mathsf{List}_{\mathbb N}). \end{aligned}$$

Множество значений $V$ такого «мира» определяется индуктивно вместе с их типами $t\colon V\to L$:
• если $x_1, \ldots, x_n \in V$, $c\in C$, $|a(c)| = n$, $t(x_i) = a(c)_i$, то $a := c(x_1, \ldots, x_n) \in V$ и $t(a) = r(c)$. Для конструктивности, запись $c(x_1, \ldots, x_n)$ обозначает дерево с корнем $c$ и непосредственными поддеревьями $x_1, \ldots, x_n$.

Множество значений типов, описанных примером выше, можно понимать как натуральные числа ($\mathsf z, \mathsf{s\, z}, \mathsf{s\, s\, z}, \ldots$) и конечные кортежи из них ($\mathsf{nil}, \mathsf{cons}(n_1, \mathsf{nil}), \mathsf{cons}(n_1, \mathsf{cons}(n_2, \mathsf{nil})), \ldots$).

Обобщённой ММ для «мира» алгебраических типов $T = (L_T, C_T, r_T, a_T)$ будет набор $(R, t, I, O, S, 0, !, \delta)$, где

$R$ — конечное множество регистров;
$t\colon R\to L_T$ — типы регистров;
$I$ — некоторый кортеж различных входных регистров машины;
$O$ — некоторый кортеж выходных регистров;

(в итоге машина понимается как реализация частичной функции $t(I_1)\times\ldots\times t(I_{|I|})\to t(O_1)\times\ldots\times t(O_{|O|})$)
$S$ — конечное множество состояний машины, включающее начальное состояние $0$ и состояние остановки $!$;
$\delta\colon (S\setminus\{!\})\to K$ — функция перехода, сопоставляющая состояниям выполняемые при нахождении в них команды, множество $K$ которых состоит ровно из элементов такого вида:

• «конструкция» $c\, r_1\ldots r_n\, r\, s$, где

$c\in C_T$, $r_i, r\in R$, $t(r) = r_T(c)$, $t(r_i) = a_T(c)_i$, $s\in S$;
• «деструкция/матчинг» $l\, r\; c_1\colon r_{11}\ldots r_{1n_1}\, s_1\ldots\; c_m\colon r_{m1}\ldots r_{mn_m}\, s_m$, где

$l\in L_T$, $\{c_1,\ldots, c_m\} = r_t^{-1}(l)$, $r, r_{ik}\in R$, $r_{ik}\ne r_{ik'}$ при $k\ne k'$, $t(r) = l$, $t(r_{ik}) = a(c_i)_k$, $n_i = |a(c_i)|$, $s_i\in S$.
(Об их точном смысле см. ниже.)

При выполнении машины мы держим в памяти текущие состояние $s^*\in S$ и значения регистров $v\colon R\to V_T$. Обозначим $v[r\gets x]$ функцию $v'$, отличающуюся от $v$ ровно тем, что $v'(r) = x$.

Выполнение машины $(s^*, v) \overset1{\to} (s', v')$ за один шаг определяется так:
• если $s^*= {!}$, тогда $s' = s$ и $v' = v$;
• если $\delta(s^*) = (c\, r_1\ldots r_n\, r\, s)$, то $s' = s$ и $v' = v[r\gets c(v(r_1), \ldots, v(r_n))]$;
• если $\delta(s^*) = (l\, r\; \ldots c_i\colon \overline{r_i}\, s_i\ldots)$, то положим $k$ таким, что $v(r) = c_k(x_1,\ldots, x_m)$, и тогда $s' = s_k$, $v' = v[r_{k1}\gets x_1]\cdots[r_{km}\gets x_m]$.

Обозначим транзитивное замыкание $\overset1{\to}$ как $\overset{*}\to$. Определим множество результатов работы машины на входах $\bar x = (x_1,\ldots, x_{|I|})$ как $o(\bar x) := \{(v'(O_1),\ldots, v'(O_{|O|}) \mid (0, v) \overset{*}\to (!, v'), v(I_i) = x_i\}$.

Наконец, машина реализует функцию $f\colon t(I_1)\times\ldots\times t(I_{|I|})\to t(O_1)\times\ldots\times t(O_{|O|})$, если для любого набора аргументов $\bar x$ выполняется одно из следующего:
• $f(\bar x)$ не определено и $|o(\bar x)|\ne 1$;
• $f(\bar x) = \bar y$ и $o(\bar x) = \{\bar y\}$.

Всё! Вопрос см. выше.