Smn-теорема

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

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

Деталі

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

${\phi }_{s(p,x)}\simeq \lambda y.{\phi }_p(x,y).$

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

${\phi }_{s_n^m(p,x_1,\dots ,x_m)}\simeq \lambda y_1,\dots ,y_n.{\phi }_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))

Посилання

• Шаблон:Cite book
• Шаблон:Cite book
• Шаблон:Cite book
• Шаблон:Cite journal