См мп теорема

В теории вычислимости на 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 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  ( f  x )  ( let  (( y  ( gensym )))  ( list  'лямбда  ( список  y )  ( список  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 .