smn theorem

From Wikipedia, the free encyclopedia
Jump to: navigation, search

In computability theory the smn theorem, (also called the translation lemma, parameter theorem, or parameterization theorem) is a basic result about programming languages (and, more generally, Gödel numberings of the computable functions) (Soare 1987, Rogers 1967). It was first proved by Stephen Cole Kleene (Kleene 1943).

In practical terms, the theorem says that for a given programming language and positive integers m and n, there is a particular algorithm that operates on the source code of programs with m + n free variables. This algorithm produces source code that effectively substitutes m given values for the first m free variables in the program and leaves the rest free.

Details[edit]

The basic form of the theorem applies to functions of two arguments (Nies 2009, p. 6). Given a Gödel numbering \varphi of recursive functions, there is a primitive recursive function s of two arguments with the following property: for every Gödel number p of a partial computable function f with two arguments, the expressions \varphi_{s(p,x)}(y) and f(x,y) are defined for the same combinations of natural numbers x and y, and their values are equal for any such combination. In other words, the following extensional equality of functions holds for every x:

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

More generally, for any mn > 0, there exists a primitive recursive function s^m_n of m + 1 arguments that behaves as follows: for every Gödel number p of a partial computable function with m + n arguments, and all values of x1,…,xm:

\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).\,

The function s described above can be taken to be s^1_1.

Example[edit]

The following Lisp code implements s11 for Lisp.

 (defun s11 (f x)
   (let ((y (gensym)))
     (list 'lambda (list y) (list f x y))))

For example, (s11 '(lambda (x y) (+ x y)) 3) evaluates to (lambda (g42) ((lambda (x y) (+ x y)) 3 g42)).

See also[edit]

References[edit]

External links[edit]