С ^м_n теорема

В теории S m вычислимости
о n Теорема , записанная также как « smn-теорема » или « smn-теорема » (также называемая леммой о переводе , теоремой о параметре и теоремой о параметризации ), является основным результатом о языках программирования (и, в более общем смысле, нумерации Гёделя вычислимых функций). ) (Соаре 1987, Роджерс 1967). Впервые это было доказано Стивеном Коулом Клини (1943). Имя См .
n возникает из-за появления буквы S с индексом n и верхним индексом m в исходной формулировке теоремы (см. ниже).

На практике теорема гласит, что для данного языка программирования и натуральных чисел m и n существует определенный алгоритм , который принимает на вход исходный код программы с $m + n$ свободными переменными вместе с m значениями. Этот алгоритм генерирует исходный код, который эффективно заменяет значения первых m свободных переменных, оставляя остальные переменные свободными.

Теорема smn утверждает, что если задана функция двух аргументов $g(x,y)$ которая вычислима , существует полная и вычислимая функция такая, что $\phi _{s}(x)(y)=g(x,y)$ в основном «исправляя» первый аргумент $g$ . Это похоже на частичное применение аргумента к функции. Это обобщено на $m,n$ кортежи для $x,y$ . Другими словами, он обращается к идее «параметризации» или «индексации» вычислимых функций. Это похоже на создание упрощенной версии функции, которая принимает дополнительный параметр (индекс) для имитации поведения более сложной функции.

Функция $s_{m}^{n}$ предназначен для имитации поведения $\phi (x,y)$ при задании соответствующих параметров. По сути, путем выбора правильных значений для $m$ и $n$ , ты можешь сделать $s$ вести себя как для конкретного вычисления. Вместо того, чтобы бороться со сложностью $\phi (x,y)$ , мы можем работать с более простым $s_{m}^{n}$ это отражает суть вычислений.

Подробности

Основная форма теоремы применима к функциям двух аргументов (Нис 2009, стр. 6). Учитывая нумерацию Гёделя $\varphi$ рекурсивных функций существует примитивно-рекурсивная функция s двух аргументов со следующим свойством: для каждого гёделева числа p частично вычислимой функции f с двумя аргументами выражения $\varphi _{s(p,x)}(y)$ и $f(x,y)$ определены для одних и тех же комбинаций натуральных чисел x и y , и их значения равны для любой такой комбинации. Другими словами, имеет место следующее экстенсиональное равенство функций для каждого x :

\varphi _{s(p,x)}\simeq \lambda y.\varphi _{p}(x,y).

В более общем смысле, для любого m , $n > 0$ , существует примитивно-рекурсивная функция $S_{n}^{m}$ из $m + 1$ аргументов, который ведет себя следующим образом: для каждого гёделева числа p частично вычислимой функции с $m + n$ аргументами и всеми значениями x ₁ , …, x _m :

\varphi _{S_{n}^{m}(p,x_{1},\dots ,x_{m})}\simeq \lambda y_{1},\dots ,y_{n}.\varphi _{p}(x_{1},\dots ,x_{m},y_{1},\dots ,y_{n}).

Описанную выше функцию s можно принять в виде $S_{1}^{1}$ .

Официальное заявление

Учитывая арность $m$ и $n$ , для каждой машины Тьюринга ${\text{TM}}_{x}$ арности $m+n$ и для всех возможных значений входных данных $y_{1},\dots ,y_{m}$ , существует машина Тьюринга ${\text{TM}}_{k}$ арности $n$ , такая, что

\forall z_{1},\dots ,z_{n}:{\text{TM}}_{x}(y_{1},\dots ,y_{m},z_{1},\dots ,z_{n})={\text{TM}}_{k}(z_{1},\dots ,z_{n}).

Более того, существует машина Тьюринга $S$ , которая позволяет $k$ вычислять $по x$ и $y$ ; это обозначается $k=S_{n}^{m}(x,y_{1},\dots ,y_{m})$ .

Неофициально $S$ находит машину Тьюринга. ${\text{TM}}_{k}$ это результат жесткого кодирования значений $y$ в ${\text{TM}}_{x}$ . Результат обобщается на любую Тьюринг-полную вычислительную модель.

Это также можно распространить на полные вычислимые функции следующим образом:

Дана полная вычислимая функция $s_{m,n}:\mathbb {N} ^{m+1}\rightarrow \mathbb {N}$ и $m,n\geq 1$ такой, что $\forall {\vec {x}}\in \mathbb {N} ^{m},\forall {\vec {y}}\in \mathbb {N} ^{n}$ , $\forall e\in \mathbb {N}$ :

$\phi _{e}^{m+n}({\vec {x}},{\vec {y}})=\phi _{s_{m,n}{(e,{\vec {x}})}}^{n}({\vec {y}})$

Существует также упрощенная версия той же теоремы (фактически определяемая как « упрощенная smn-теорема », которая в основном использует полную вычислимую функцию в качестве индекса следующим образом:

Позволять $f:\mathbb {N} ^{n+m}\rightarrow \mathbb {N}$ быть вычислимой функцией. Там существует тотально вычислимая функция $s:\mathbb {N} ^{m}\rightarrow \mathbb {N}$ такой, что $\forall x\in \mathbb {N} ^{m}$ , ${\vec {y}}\in \mathbb {N} ^{n}$ :

$f({\vec {x}},{\vec {y}})=\phi _{S({\vec {x}})}^{(n)}({\vec {y}})$

Пример

Следующий код Lisp реализует s ₁₁ для Lisp.

(defun s11 (f x)
  (let ((y (gensym)))
    (list 'lambda (list y) (list f x y))))

Например, (s11 '(lambda (x y) (+ x y)) 3) оценивается как (lambda (g42) ((lambda (x y) (+ x y)) 3 g42)).

См. также

Ссылки

Клини, Южная Каролина (1936). «Общерекурсивные функции натуральных чисел» . Математические Аннален . 112 (1): 727–742. дои : 10.1007/BF01565439 . S2CID 120517999 .
Клини, Южная Каролина (1938). «Об обозначениях порядковых чисел» (PDF) . Журнал символической логики . 3 : 150–155. дои : 10.2307/2267778 . JSTOR 2267778 . S2CID 34314018 . (Это ссылка на стр. 131 «Классической теории рекурсии» Одифредди в издании 1989 года). $S_{n}^{m}$ теорема.)
Нис, А. (2009). Вычислимость и случайность . Оксфордские руководства по логике. Том. 51. Оксфорд: Издательство Оксфордского университета. ISBN 978-0-19-923076-1 . Коллекция 1169.03034 .
Одифредди, П. (1999). Классическая теория рекурсии . Северная Голландия. ISBN 0-444-87295-7 .
Роджерс, Х. (1987) [1967]. Теория рекурсивных функций и эффективная вычислимость . Первое издание MIT в мягкой обложке. ISBN 0-262-68052-1 .
Соаре, Р. (1987). Рекурсивно перечислимые множества и степени . Перспективы математической логики. Спрингер-Верлаг. ISBN 3-540-15299-7 .

Внешние ссылки

Вайсштейн, Эрик В. «Теорема Клини s - m - n » . Математический мир .