Теорема Смна

О преобразовании программы путем замены свободных переменных константами

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

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

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

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

Подробности

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

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

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

${\displaystyle \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 можно принять равной . ${\displaystyle S_{1}^{1}}$

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

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

${\displaystyle \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 ; оно обозначается . ${\displaystyle k=S_{n}^{m}(x,y_{1},\dots ,y_{m})}$

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

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

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

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

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

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

${\displaystyle 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.(Это ссылка на теорему в издании «Классической теории рекурсии» Одифредди 1989 года на стр. 131. ) ${\displaystyle 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.

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

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