Smn теорема

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

В теорії обчислень, smn теорема, (також відома як лема про трансляцію, теорема параметрів, чи теорема параметризації) основне досягнення в сфері мов програмування (і, більш загально, Гьоделівських нумерацій обчислюваних функцій). Вперше була доведена Кліні у 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 реалізує s11

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