2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему
 
 Обобщённая машина Минского
Сообщение04.11.2019, 18:08 
Заслуженный участник


27/04/09
28128
Машиной (обычной) Минского обычно называют регистровую машину, у которой в регистрах натуральные числа (включая ноль) и две команды — $\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\}$.

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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ 1 сообщение ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group