См ^м _п теорема - S^m_n theorem

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

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

Подробности

Основная форма теоремы применяется к функциям двух аргументов (Nies 2009, p. 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 ₁ , …, 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}}$

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

Для заданных арностей и для каждой машины Тьюринга арности и для всех возможных значений входных данных существует машина Тьюринга арности , такая что ${\ 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 к = S_ {n} ^ {m} (х, y_ {1}, \ точки, y_ {m})}$

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

Пример

Следующий код 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))

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

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

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

• Клини, SC (1936). «Общерекурсивные функции натуральных чисел» . Mathematische Annalen . 112 (1): 727–742. DOI : 10.1007 / BF01565439 .
• Клини, SC (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 .

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

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