Smn теорема

В теорії обчислень, s_mn теорема, (також відома як лема про трансляцію, теорема параметрів, чи теорема параметризації) основне досягнення в сфері мов програмування (і, більш загально, Гьоделівських нумерацій обчислюваних функцій). Вперше була доведена Кліні у 1943.

На практиці, теорема означає, що для заданої мови програмування та додатніх цілих m та n, існує певний алгоритм який оперує кодом програм з m+n вільними змінними. Цей алгоритм ефективно прив'язує m даних значень до перших m вільних змінних в програмі, і залишає інші вільними.

Деталі

Найпростішою формою до якої застосовна теорема є функція двох аргументів. Маючи дану Гьоделівську нумерацію $\varphi$ рекурсивних функцій, існує, примітивно-рекурсивна функція s двох аргументів з такою властивістю: для кожного номера p часткової обчислюваної функції f з двома аргументами, $\varphi_{s(p,x)}(y)$ та $f(x,y)$ визначені для однакових комбінацій x-ів та y-ків однакові для тих комбінацій. Іншими словами, наступна зовнішня рівність функцій зберігається:

$\varphi_{s(p,x)} \simeq \lambda y.\varphi_p(x,y).\,$

Щоб узагальнити теорему, виберіть схему для кодування n чисел як одне число, так що оригінальні числа можуть витягуватись примітивно рекурсивними функціями. Наприклад, одна може чергувати біти чисел. Тоді для будь-яких m, n > 0, існує примітивно рекурсивна функція $s^m_n$ m+1 аргументів яка поводиться таким чином: для кожного Гьоделівського числа p частково обчислюваної функції з m+n аргументами:

$\varphi_{s^{m}_{n}(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^1_1$ є лише функцією s що вже була описана.

Приклад

Наступний код Lisp реалізує s₁₁

(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)).

Посилання

• Використано матеріали зі статті в англійській Вікіпедії.
• Odifreddi, P. (1999). Classical Recursion Theory. North-Holland. ISBN 0-444-87295-7. 
• Rogers, H. (1987) [1967]. The Theory of Recursive Functions and Effective Computability. First MIT press paperback edition. ISBN 0-262-68052-1. 
• Soare, R. (1987). Recursively enumerable sets and degrees. Perspectives in Mathematical Logic. Springer-Verlag. ISBN 3-540-15299-7. 
• Kleene, S. C. General recursive functions of natural numbers // Mathematische Annalen. — Т. 112. — (1936) С. 727–742. DOI:10.1007/BF01565439.