Теорема Smn
-
Теорема sm mn
- Теорема sm mn утверждает, что для заданного языка программирования и натуральных чисел m и n существует алгоритм, который заменяет значения первых m свободных переменных в исходном коде программы.
- Теорема была доказана Стивеном Коулом Клини в 1943 году.
-
Формулировка теоремы
- Теорема утверждает, что для функции g(x, y) существует полная и вычислимая функция s(x), такая что s(x)(y) = g(x, y).
- Функция s(x) имитирует поведение g(x, y) при задании соответствующих параметров.
-
Обобщение теоремы
- Теорема обобщается на функции с m + n аргументами.
- Для каждого числа Геделя p и частично вычислимой функции f с m + n аргументами существует примитивная рекурсивная функция S(n, m), такая что S(n, m)(x, y) = f(x, y) для всех x и y.
-
Официальное заявление
- Для каждой машины Тьюринга арности m + n и всех возможных значений входных данных y1, …, ym существует машина Тьюринга k, такая что k = S(n, m)(x, y1, …, ym).
- Неофициально, S находит машину Тьюринга k путем жесткого кодирования значений y в машине Тьюринга x.
-
Упрощенная версия теоремы
- Существует упрощенная версия теоремы, использующая полную вычислимую функцию s(x) в качестве индекса.
- Для каждой вычислимой функции f: Nn + m → N существует полная вычислимая функция s: Nm → N, такая что f(x, y) = ϕS(x)(n)(y).
-
Пример реализации
- Приведен лисп-код, реализующий s11 для Lisp.