Smn-теорема

В теорії обчислень s_mn-теорема (англ. s_mn theorem; також відома як лема про трансляцію, теорема параметрів, чи теорема параметризації) — основне досягнення в сфері мов програмування (і, більш загально, Геделівських нумерацій обчислюваних функцій). Вперше була доведена Стівеном Коулом Кліні у 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_{n}^{m}$ m+1 аргументів, яка поводиться таким чином: для кожного Геделівського числа p частково обчислюваної функції з m+n аргументами:

$\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_{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. (1936). General recursive functions of natural numbers. Mathematische Annalen. 112: 727—742. doi:10.1007/BF01565439.