S^м_п теорема - Smn theorem - Wikipedia

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

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

Подробности

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

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

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

${\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}}$.

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

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

${\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}).}$

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

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

Пример

Следующее Лисп код реализует s₁₁ для Лиспа.

 (defun s11 (ж Икс)   (позволять ((у (генсим)))     (список лямбда (список у) (список ж Икс у))))

Например, (s11 '(лямбда (Икс у) (+ Икс у)) 3) оценивает (лямбда (g42) ((лямбда (Икс у) (+ Икс у)) 3 g42)).

Смотрите также

• Каррирование
• Теорема Клини о рекурсии
• Частичная оценка

Рекомендации

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

внешняя ссылка

• Вайсштейн, Эрик В. "Клини" s-м-п Теорема ". MathWorld.