Smn-теорема

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

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

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

Деталі

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

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

є лише функцією 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.